<div dir="ltr">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:<div><br></div><div><a href="https://github.com/klutzy/nadeko">https://github.com/klutzy/nadeko</a><br></div><div><br></div><div>This lets you write what otherwise looks like ordinary Rust code, but in a way that's actually applicable to cryptographic implementations.</div><div><br></div><div>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.</div><div><br></div><div>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"</div><div><br></div><div>Seems better than Perl scripts? ;)</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Mar 31, 2015 at 7:32 PM, Peter Schwabe <span dir="ltr"><<a href="mailto:peter@cryptojedi.org" target="_blank">peter@cryptojedi.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">Trevor Perrin <<a href="mailto:trevp@trevp.net">trevp@trevp.net</a>> wrote:<br>
> On Thu, Mar 19, 2015 at 11:36 AM, Samuel Neves <<a href="mailto:sneves@dei.uc.pt">sneves@dei.uc.pt</a>> wrote:<br>
<br>
</span>Dear all,<br>
<span class=""><br>
> I don't know that anyone's doing much formal validation of ECC<br>
> codebases yet, but it seems like a potential good idea.  If the input<br>
> source is a Perl script any formal validation tools would need to<br>
> understand Perl (not likely) or would need to understand asm, and be<br>
> re-run on every output flavor...<br>
<br>
</span>Well, in our CCS paper [1] we did formal verification of ECC in<br>
hand-optimized assembly. We worked on qhasm [2] level, which (aside from<br>
the fact that qhasm is in alpha state for a long time already and the<br>
language is not formally defined) might be a suitable alternative:<br>
verification tools can understand qhasm; qhasm can translate to<br>
different assembly dialects and (once the qhasm syntax and semantics are<br>
formally defined) it should be feasible to formally verify the<br>
translation process from qhasm to assembly.<br>
<br>
Best regards,<br>
<br>
Peter<br>
<br>
<br>
[1] <a href="http://cryptojedi.org/papers/#verify25519" target="_blank">http://cryptojedi.org/papers/#verify25519</a><br>
[2] <a href="http://cr.yp.to/qhasm.html" target="_blank">http://cr.yp.to/qhasm.html</a><br>
<br>_______________________________________________<br>
Curves mailing list<br>
<a href="mailto:Curves@moderncrypto.org">Curves@moderncrypto.org</a><br>
<a href="https://moderncrypto.org/mailman/listinfo/curves" target="_blank">https://moderncrypto.org/mailman/listinfo/curves</a><br>
<br></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature">Tony Arcieri<br></div>
</div>