The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.

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*, 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, Jade Philipoom, Jason Gross, Robert Sloan.