Tahina Ramananandro > Research > Everest >

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider

Jonathan Protzenko (RiSE: Research in Software Engineering, Microsoft Research, Redmond, WA, USA)
Bryan Parno (Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA; Electrical and Computer Engineering Department, Carnegie Mellon University)
Aymeric Fromherz (CMU)
Chris Hawblitzel (Systems Research Group, Microsoft Research, Redmond, WA, USA)
Marina Polubelova (Prosecco, INRIA, Paris, France)
Karthikeyan Bhargavan (Prosecco)
Benjamin Beurdouche (Prosecco)
Joonwon Choi (Programming Principles and Tools, Microsoft Research, Cambridge, United Kingdom; CSAIL, MIT, Cambridge, MA, USA)
Antoine Delignat-Lavaud (Programming Principles and Tools)
Cédric Fournet (Programming Principles and Tools)
Natalia Kulatova (Prosecco)
Tahina Ramananandro (RiSE)
Aseem Rastogi (Microsoft Research, Bengaluru, Karnataka, India)
Nikhil Swamy (RiSE)
Christoph Wintersteiger (Programming Principles and Tools)
Santiago Zanella-Béguelin (Programming Principles and Tools)

IEEE S&P 2020 (41st IEEE Symposium on Security and Privacy, a.k.a. "Oakland")

We present EverCrypt: a comprehensive collection of verified, high-performance cryptographic functionalities available via a carefully designed API. The API provably supports agility (choosing between multiple algorithms for the same functionality) and multiplexing (choosing between multiple implementations of the same algorithm). Through abstraction and zero-cost generic programming, we show how agility can simplify verification without sacrificing performance, and we demonstrate how C and assembly can be composed and verified against shared specifications. We substantiate the effectiveness of these techniques with new verified implementations (including hashes, Curve25519, and AES-GCM) whose performance matches or exceeds the best unverified implementations. We validate the API design with two high-performance verified case studies built atop EverCrypt, resulting in line-rate performance for a secure network protocol and a Merkle-tree library, used in a production blockchain, that supports 2.7 million insertions/sec. Altogether, EverCrypt consists of over 124K verified lines of specs, code, and proofs, and it produces over 29K lines of C and 14K lines of assembly code.