Fiat Cryptography: Automatic Correct-by-Construction Generation of Low-Level Cryptographic Code

Опубликовано 16 января 2018, 3:59

Some of the most widely used cryptographic protocols, including TLS, depend on fast execution of modular big-number arithmetic. Cryptographic primitives are coded by an elite set of implementation experts, and most programmers are shocked to learn that performance-competitive implementations are rewritten from scratch for each new prime-number modulus and each significantly different hardware architecture. In the Fiat Cryptography project, we show for the first time that an automatic compiler can produce this modulus-specialized code, via formalized versions of the number-theoretic optimizations that had previously only been applied by hand. Through experiments for a wide range of moduli, compiled for 64-bit x86 and 32-bit ARM processors, we demonstrate typical speedups vs. an off-the-shelf big-integer library in the neighborhood of 5X, sometimes going up to 10X. As a bonus, our compiler is implemented in the Coq proof assistant and generates proofs of functional correctness. These combined benefits of rigorous correctness/security guarantees and labor-saving were enough to convince the Google Chrome team to adopt our compiler for parts of their TLS implementation in the BoringSSL library. The project is joint work with Andres Erbsen, Jade Philipoom, Jason Gross, and Robert Sloan. 

See more at microsoft.com/en-us/research/v...