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

Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cedric Fournet; Natalia Kulatova; Tahina Ramananandro; Aseem Rastogi; Nikhil Swamy; Christoph Wintersteiger; Santiago Zanella-Beguelin

Paper 2019/757

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

Jonathan Protzenko

Bryan Parno

Aymeric Fromherz

Chris Hawblitzel

Marina Polubelova

Karthikeyan Bhargavan

Benjamin Beurdouche

Joonwon Choi

Antoine Delignat-Lavaud

Cedric Fournet

Natalia Kulatova

Tahina Ramananandro

Aseem Rastogi

Nikhil Swamy

Christoph Wintersteiger

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 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.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Published elsewhere. Proceedings of the IEEE Symposium on Security and Privacy, 2020
DOI: 10.1109/SP40000.2020.00114
Keywords: verification secret-key cryptography elliptic 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

BibTeX

@misc{cryptoeprint:2019/757,
      author = {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 Natalia Kulatova and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Christoph Wintersteiger and Santiago Zanella-Beguelin},
      title = {{EverCrypt}: A Fast, Verified, Cross-Platform Cryptographic Provider},
      howpublished = {Cryptology {ePrint} Archive, Paper 2019/757},
      year = {2019},
      doi = {10.1109/SP40000.2020.00114},
      url = {https://eprint.iacr.org/2019/757}
}