EverCrypt: A Fast, Veriﬁed, Cross-Platform Cryptographic Provider - Protzenko, Jonathan; Parno, Bryan; Fromherz, Aymeric; Hawblitzel, Chris; Polubelova, Marina; Bhargavan, Karthikeyan; Beurdouche, Benjamin; Choi, Joonwon; Delignat-Lavaud, Antoine; Fournet, Cédric; Kulatova, Natalia; Ramananandro, Tahina; et al. (IEEE Symposium on Security and Privacy, 2020)
We present EverCrypt: a comprehensive collection of veriﬁed, 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 veriﬁcation without sacriﬁcing performance, and we demonstrate how C and assembly can be composed and veriﬁed against shared speciﬁcations. We substantiate the effectiveness of these techniques with new veriﬁed implementations (including hashes, Curve25519, and AES-GCM) whose performance matches or exceeds the best unveriﬁed implementations. We validate the API design with two high-performance veriﬁed 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 veriﬁed lines of specs, code, and proofs, and it produces over 29K lines of C and 14K lines of assembly code.