Crafting certified elliptic curve cryptography implementations in Coq

Elliptic curve cryptography has become a de-facto standard for protecting the privacy and integrity of internet communications. To minimize the operational cost and enable near-universal adoption, increasingly sophisticated implementation techniques have been developed. While the complete specification of an elliptic curve cryptosystem (in terms of middle school mathematics) fits on the back of a napkin, the fast implementations span thousands of lines of low-level code and are only intelligible to a small group of experts. However, the complexity of the code makes it prone to bugs, which have rendered well-designed security systems completely ineffective. I describe a principled approach for writing crypto code simultaneously with machine-checkable functional correctness proofs that compose into an end-to-end certificate tying highly optimized C code to the simplest specification used for verification so far. Despite using template-based synthesis for creating low-level code, this workflow offers good control over performance: I was able to match the fastest C implementation of X25519 to within 1% of arithmetic instructions per inner loop and 7% of overall execution time. While the development method itself relies heavily on a proof assistant such as Coq and most techniques are explained through code snippets, every Coq feature is introduced and motivated when it is first used to accommodate a non-Coq-savvy reader.

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2017

Author dc:creator

• Erbsen, Andres

Advisor dc:contributor.advisor

• Adam Chlipala.

• Electrical Engineering and Computer Science.

Statement dc:rights

• MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/112843

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/112843