Adam Chlipala
2018-07-15 14:04:13 UTC
I'm writing to share a bit of progress in real-world use of Coq, which I
hope will be helpful to anyone who needs to make a case for the value of
the Coq system or specific uses of it. Much more detail is found in our
upcoming paper on the project
<http://adam.chlipala.net/papers/FiatCryptoSP19/>.
Background: cryptography is an interesting area for algorithmic
challenges because we need crucial operations to be fast for legitimate
participants and slow for bad guys who don't know the right secrets.Â
Some of the most widely used algorithms are quite challenging to
implement efficiently on commodity processors. Elliptic curves are one
of the most popular approaches to public-key crypto today, and practice
there has been to rewrite the code from scratch in assembly (or C, if
we're lucky), not just for every interestingly different hardware
family, but also for every different set of numeric parameters. Yes, it
really has been traditional to rewrite the code from scratch when you
change the one large prime number used as modulus of arithmetic.
With our Fiat Cryptography project, we show how the important algorithms
can be written as Gallina programs, such that their partial evaluation
to specific parameters gives us performance-competitive low-level code.Â
And, of course, we prove the crypto algorithms and the compilation
phases in Coq.
This code-generation pipeline is now used for Google's BoringSSL
library, to generate the finite-field arithmetic for the two most widely
used elliptic curves, P-256 and Curve25519. BoringSSL is used in a few
high-profile places, most notably the Chrome browser. As a result, a
back-of-the-envelope market-share calculation suggests that about half
of all HTTPS connections from browsers worldwide now use our
correct-by-construction field arithmetic, generated and proved with
Coq. Probably many of you saw the earlier news about inclusion in
Firefox of handwritten code verified with F*
<https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/>,
which handles some of the same parts of TLS; so formal verification is
really making some inroads in this area, where security bugs are
genuinely scary.
Most of the work on this project was done by the student team members,
all of whom have spent some time working on it at Google by now.Â
Following the author order from the paper: they are Andres Erbsen
<https://andres.systems/>, Jade Philipoom
<https://github.com/jadephilipoom>, Jason Gross
<http://people.csail.mit.edu/jgross/>, Robert Sloan <https://blog.modt.io/>.
hope will be helpful to anyone who needs to make a case for the value of
the Coq system or specific uses of it. Much more detail is found in our
upcoming paper on the project
<http://adam.chlipala.net/papers/FiatCryptoSP19/>.
Background: cryptography is an interesting area for algorithmic
challenges because we need crucial operations to be fast for legitimate
participants and slow for bad guys who don't know the right secrets.Â
Some of the most widely used algorithms are quite challenging to
implement efficiently on commodity processors. Elliptic curves are one
of the most popular approaches to public-key crypto today, and practice
there has been to rewrite the code from scratch in assembly (or C, if
we're lucky), not just for every interestingly different hardware
family, but also for every different set of numeric parameters. Yes, it
really has been traditional to rewrite the code from scratch when you
change the one large prime number used as modulus of arithmetic.
With our Fiat Cryptography project, we show how the important algorithms
can be written as Gallina programs, such that their partial evaluation
to specific parameters gives us performance-competitive low-level code.Â
And, of course, we prove the crypto algorithms and the compilation
phases in Coq.
This code-generation pipeline is now used for Google's BoringSSL
library, to generate the finite-field arithmetic for the two most widely
used elliptic curves, P-256 and Curve25519. BoringSSL is used in a few
high-profile places, most notably the Chrome browser. As a result, a
back-of-the-envelope market-share calculation suggests that about half
of all HTTPS connections from browsers worldwide now use our
correct-by-construction field arithmetic, generated and proved with
Coq. Probably many of you saw the earlier news about inclusion in
Firefox of handwritten code verified with F*
<https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/>,
which handles some of the same parts of TLS; so formal verification is
really making some inroads in this area, where security bugs are
genuinely scary.
Most of the work on this project was done by the student team members,
all of whom have spent some time working on it at Google by now.Â
Following the author order from the paper: they are Andres Erbsen
<https://andres.systems/>, Jade Philipoom
<https://github.com/jadephilipoom>, Jason Gross
<http://people.csail.mit.edu/jgross/>, Robert Sloan <https://blog.modt.io/>.