[curves] Distribution-ready optimized code

[Tony Arcieri]

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 <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 [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
> Curves at moderncrypto.org
> https://moderncrypto.org/mailman/listinfo/curves
>
>


-- 
Tony Arcieri
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/curves/attachments/20150331/0ebed277/attachment.html>