Cryptographic security protocols, such as TLS or WireGuard, form the foundation of a secure Internet, and yet modern implementations still rely on testing and manual audits for security and correctness. We aim to replace these ad hoc efforts with strong mathematical guarantees, using a combination of type-checking, proof-producing compilation, and automated formal verification. A key theme of our work is a focus on scaling verification to complex, real-world protocols, while ensuring state-of-the-art performance for the resulting implementations.

In the talk, we will describe our novel use of information flow and refinement types for modular, computationally-sound protocol proofs, as well techniques to compile high-level protocol descriptions into high-performance implementations that are provably correct and secure, even against basic digital side channels. These implementations rely, in turn, on newly developed tools for creating high-performance, verifiably correct and secure versions of: serializers and parsers in Rust, customizable x.509 certificate validation libraries, and cryptographic primitives. We will present a variety of case studies showing that our verified protocol implementations interoperate with existing implementations, and that their performance matches unverified industrial baselines on end-to-end benchmarks.