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

Explore a comprehensive presentation on EverCrypt, a fast, verified, and cross-platform cryptographic provider. Delve into the challenges of modern cryptography, including the trade-offs between speed and security. Learn about EverCrypt's innovative approach to combining verified implementations with high performance, its carefully designed API supporting algorithm agility and implementation multiplexing, and the use of abstraction and zero-cost generic programming. Discover how EverCrypt integrates C and assembly code while maintaining shared specifications and verification. Examine new verified implementations of cryptographic algorithms, including hashes, Curve25519, and AES-GCM, that match or exceed the performance of unverified alternatives. Investigate real-world applications of EverCrypt through case studies, including a secure network protocol and a high-performance Merkle-tree library used in blockchain technology. Gain insights into EverCrypt's extensive codebase, comprising over 124,000 verified lines of specifications, code, and proofs, which generate more than 29,000 lines of C and 14,000 lines of assembly code.

Intro
Modern Crypto Providers are Fast
Modern Crypto Providers are Insecure
Verified Crypto: Some Assembly Required
EverCrypt is Comprehensive
Modern API Design
Generic Interop: C Assembly
Lifting specifications over calling conventions
EverCrypt Performance
Performance: SHA-256
Performance: AEAD
Example: Merkle trees
Performance: Merkle tree
EverCrypt Summary