http://gfverif.cryptojedi.org/
(Humorous logo of Evariste Galois and a checkmark elided) Cryptographic software needs to be correct: even a tiny bug can have disastrous consequences for security, as illustrated by Brumley, Barbosa, Page, and Vercauteren exploiting an ECDH carry bug in OpenSSL 0.9.8g. Standard software-testing techniques catch many bugs but did not prevent, e.g., further OpenSSL carry bugs announced in January 2015 (initial analysis: too expensive to exploit) and December 2015 (initial analysis: exploitable by well-equipped attackers). The goal of gfverif is to integrate highly automated proofs of correctness into the ECC software-development process. These proofs can be compromised by bugs in gfverif, but eliminating those bugs is a relatively small one-time task. Correct proofs will eliminate all ECC software bugs, including the low-probability carry bugs that slip past testing. Of course, bug-free software can be compromised by hardware bugs and compiler bugs, but separate projects are underway to eliminate those bugs. ... We have proven the correctness of a reference implementation of X25519 elliptic-curve scalar multiplication. The implementation is, except for a few minor tweaks, the preexisting "ref10" implementation in C. Correctness means that, under plausible assumptions regarding the behavior of the C compiler, the implementation computes exactly the function specified by a concise high-level description of X25519. ... gfverif focuses on finite-field computations. This is slightly broader than ECC (for example, it can handle HECC and can probably handle NTRU) but it isn't all of core crypto. On the other hand, it's a significant chunk of core crypto. etc. -- http://www.subspacefield.org/~travis/ | if spammer then j...@subspacefield.org "Computer crime, the glamor crime of the 1970s, will become in the 1980s one of the greatest sources of preventable business loss." John M. Carroll, "Computer Security", first edition cover flap, 1977 _______________________________________________ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
