[curves] Distribution-ready optimized code

[Peter Schwabe]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 173 bytes
Desc: Digital signature
URL: <http://moderncrypto.org/mail-archive/curves/attachments/20150401/d00cd6f0/attachment.sig>