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
signature.asc
Description: Digital signature
_______________________________________________ Curves mailing list [email protected] https://moderncrypto.org/mailman/listinfo/curves
