FYI... It looks like an interesting tool, and the timing is good since
we are expanding curve support.

---------- Forwarded message ----------
From:  <travis+ml-rbcryptogra...@subspacefield.org>
Date: Mon, Jan 18, 2016 at 6:23 PM
Subject: [cryptography] gfverif, djb's ECC bugfinder
To: cryptogra...@randombit.net

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
cryptogra...@randombit.net
http://lists.randombit.net/mailman/listinfo/cryptography

-- 
-- 
You received this message because you are subscribed to the "Crypto++ Users" 
Google Group.
To unsubscribe, send an email to cryptopp-users-unsubscr...@googlegroups.com.
More information about Crypto++ and this group is available at 
http://www.cryptopp.com.
--- 
You received this message because you are subscribed to the Google Groups 
"Crypto++ Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to cryptopp-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Reply via email to