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:
https://github.com/klutzy/nadeko 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 <[email protected]> wrote: > Trevor Perrin <[email protected]> wrote: > > On Thu, Mar 19, 2015 at 11:36 AM, Samuel Neves <[email protected]> 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 [1] we did formal verification of ECC in > hand-optimized assembly. We worked on qhasm [2] 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, > > Peter > > > [1] http://cryptojedi.org/papers/#verify25519 > [2] http://cr.yp.to/qhasm.html > > _______________________________________________ > Curves mailing list > [email protected] > https://moderncrypto.org/mailman/listinfo/curves > > -- Tony Arcieri
_______________________________________________ Curves mailing list [email protected] https://moderncrypto.org/mailman/listinfo/curves
