The Last Mile: High-Assurance and High-Speed Cryptographic Implementations

Abstract

We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as hand-written assembly. We illustrate our approach using Chacha20-Poly1305, one of the mandatory ciphersuites in TLS 1.3.
We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which allows for proofs of functional correctness and equivalence checking. These infrastructures allow programmers to develop efficient and verified implementations by “game hopping”, starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking.
To do this, we extended the Jasmin compiler to verify that the source program is safe (e.g. no out-of-bound array accesses), using a automated static analyzer. Moreover, we automatically infer sufficient conditions under which the program memory accesses are safe (the memory calling contract).