Bringing Verified Cryptographic Protocols to Practice

Explore a keynote presentation from Carnegie Mellon University's Bryan Parno at PriSC 2025 workshop that addresses the critical challenge of bringing verified cryptographic protocols into practical implementation. Learn how researchers aim to replace traditional testing and manual audits with strong mathematical guarantees through type-checking, proof-producing compilation, and automated formal verification. Discover innovative approaches using information flow and refinement types for modular, computationally-sound protocol proofs, along with techniques to compile high-level protocol descriptions into high-performance implementations that are provably correct and secure against basic digital side channels. The talk showcases newly developed tools for creating verifiably correct and secure versions of serializers and parsers in Rust, customizable x.509 certificate validation libraries, and cryptographic primitives. Through various case studies, see how these verified protocol implementations successfully interoperate with existing implementations while matching the performance of unverified industrial baselines on end-to-end benchmarks.