| Title | : | Owl: Bringing Verified Cryptographic Protocols to Practice |
| Speaker | : | Pratap Singh (Carnegie Mellon University) |
| Details | : | Tue, 13 Jan, 2026 11:00 AM @ SSB 334 |
| Abstract: | : | Cryptographic security protocols, such as TLS or WireGuard, form the foundation of a secure Internet, but vulnerabilities are discovered in them with alarming frequency. Formal verification promises a foundational solution to this problem, with significant prior work on mechanizing cryptographic proofs of high-level protocol designs, and more recent work on verifying particular implementations of single protocols against higher-level specifications. In this talk, I will discuss our work on Owl, a verifier and secure compiler for cryptographic protocols. Owl's verifier uses a novel combination of information-flow and refinement types to prove security in the computational model, enabling greater modularity and automation than prior computational tools. Owl's compiler translates well-typed protocols into performant, interoperable, side-channel-resistant Rust libraries that are automatically verified to be correct. With Owl, developers can define and prove security for their protocols in an intuitive, high-level language, and obtain for free a drop-in executable implementation with formal guarantees of correctness and security. We evaluate Owl using a range of case studies. We verify the core logic of 14 protocols, including SSH and Kerberos. We additionally develop two large-scale, interoperable case studies for WireGuard and Hybrid Public-Key Encryption (HPKE), yielding verified implementations that interoperate with, and match the performance of, existing industrial baselines on end-to-end benchmarks. |
