Paper 2019/757
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
Jonathan Protzenko and Bryan Parno and Aymeric Fromherz and Chris Hawblitzel and Marina Polubelova and Karthikeyan Bhargavan and Benjamin Beurdouche and Joonwon Choi and Antoine Delignat-Lavaud and Cedric Fournet and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Christoph Wintersteiger and Santiago Zanella-Beguelin
Abstract
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 a combination of 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.5+ million insertions/sec. Altogether, EverCrypt consists of over 100K verified lines of specs, code, and proofs, and it produces over 45K lines of C and assembly code.
Metadata
- Available format(s)
- Category
- Implementation
- Publication info
- Preprint. MINOR revision.
- Keywords
- verificationsecret-key cryptographyelliptic curves
- Contact author(s)
- parno @ cmu edu
- History
- 2022-09-25: last of 2 revisions
- 2019-07-02: received
- See all versions
- Short URL
- https://ia.cr/2019/757
- License
-
CC BY