OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries
Pratap Singh
34th USENIX Security Symposium (USENIX Security '25) · Day 2 · Crypto 3: Formal Methods and Private Computation
Cryptographic protocols form the bedrock of digital security, underpinning everything from secure web traffic (TLS) to private messaging (Signal) and secure network access (WireGuard). Despite their critical importance, implementations of these protocols have been plagued by a persistent stream of vulnerabilities, some leading to catastrophic financial and data losses. While significant academic effort has focused on formally proving the cryptographic soundness of protocol designs, a substantial gap often remains between these theoretical proofs and the security of the actual code deployed in production environments. This talk addresses precisely this disparity, highlighting how even a perfectly designed protocol can be rendered insecure by flaws in its implementation.
AI review
OwlC is legitimate, technically dense research that attacks a real and persistent problem — the gap between formally verified protocol designs and their inevitably buggy implementations. The combination of interaction trees for effect specification, ghost linear permission tokens for enforcement, and a cryptography-guided declassification mechanism is a genuinely novel stack, and the WireGuard case study with only 6% overhead closes the 'too slow to matter' escape hatch that kills most formal methods work.