[curves] Distribution-ready optimized code
bascule at gmail.com
Tue Mar 31 19:47:25 PDT 2015
Not really formally verified or applicable to other languages, but the
Nadeko library for Rust uses a syntax extension (i.e. macros) to transform
a subset of Rust into "constant time" x86-64 assembly:
This lets you write what otherwise looks like ordinary Rust code, but in a
way that's actually applicable to cryptographic implementations.
I guess the nice thing about Rust is if you do use it to make a library, it
has no mandatory runtime/GC/any of that, uses C calling conventions, and
should be easy to integrate into practically any other language that
supports a C ABI/FFI of some sort.
You also get all of the type safety you ordinarily would with Rust, but
with a backend that skips LLVM and instead uses a completely asm
macro-based "crypto compiler"
Seems better than Perl scripts? ;)
On Tue, Mar 31, 2015 at 7:32 PM, Peter Schwabe <peter at cryptojedi.org> wrote:
> Trevor Perrin <trevp at trevp.net> wrote:
> > On Thu, Mar 19, 2015 at 11:36 AM, Samuel Neves <sneves at dei.uc.pt> wrote:
> Dear all,
> > I don't know that anyone's doing much formal validation of ECC
> > codebases yet, but it seems like a potential good idea. If the input
> > source is a Perl script any formal validation tools would need to
> > understand Perl (not likely) or would need to understand asm, and be
> > re-run on every output flavor...
> Well, in our CCS paper  we did formal verification of ECC in
> hand-optimized assembly. We worked on qhasm  level, which (aside from
> the fact that qhasm is in alpha state for a long time already and the
> language is not formally defined) might be a suitable alternative:
> verification tools can understand qhasm; qhasm can translate to
> different assembly dialects and (once the qhasm syntax and semantics are
> formally defined) it should be feasible to formally verify the
> translation process from qhasm to assembly.
> Best regards,
>  http://cryptojedi.org/papers/#verify25519
>  http://cr.yp.to/qhasm.html
> Curves mailing list
> Curves at moderncrypto.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Curves