Write a Blog >>

Elliptic curve cryptography (ECC) is at the heart of some of the workhorse algorithms in TLS 1.3 and other important protocols. You may be shocked to hear that, for the modular big-integer arithmetic behind this kind of algorithm, expert implementers often write new assembly code from scratch for each new large prime modulus! The constant-factor performance win is so big that it makes sense to invest in that kind of specialization, compared to using, say, a standard bignum library based on dynamic allocation. But could we do the specialization automatically and save human engineers the trouble?

I will present Fiat Cryptography, a work-in-progress Coq library that can generate fast ECC code automatically from short descriptions of implementation strategies. While a particular run may spit out thousands of lines of low-level code, we also generate proofs of equivalence to the uncontroversial whiteboard-level math behind elliptic curves. The library’s architecture combines traditional manual proofs of data abstraction, generation of specialized code via partial evaluation, and some compiler verification. For curve 25519, the “hello world” of elliptic curves with a conveniently straightforward prime modulus, we are able to get within about 20% of the performance of the best known C implementation.

Thu 22 Jun
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: Academic crypto projects; industry perspective on formal-methods integrationDSW at Vertex WS216
Chair(s): Zhong ShaoYale University
10:30 - 11:00
Correct-by-Construction Generation of Fast Code for Elliptic Curves
Adam ChlipalaMassachusetts Institute of Technology, USA
11:00 - 11:30
Introduction to verification using the VST
Lennart BeringerPrinceton University
11:30 - 12:10
Using formal tools to develop high-assurance software for autonomous ground vehicles
Aleksey NoginHRL Laboratories, LLC