[PriSC'25] Keynote: Bringing Verified Cryptographic Protocols to Practice

Keynote: Bringing Verified Cryptographic Protocols to Practice (Video, PriSC 2025) Bryan Parno (Carnegie Mellon University) Abstract: 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. Presentation at the PriSC 2025 workshop, January 19, 2025, https://popl25.sigplan.org/home/prisc-2025 Sponsored by ACM SIGPLAN