[curves] Distribution-ready optimized code
peter at cryptojedi.org
Tue Mar 31 19:32:16 PDT 2015
Trevor Perrin <trevp at trevp.net> wrote:
> On Thu, Mar 19, 2015 at 11:36 AM, Samuel Neves <sneves at dei.uc.pt> wrote:
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 173 bytes
Desc: Digital signature
More information about the Curves