OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries

Pratap Singh, Joshua Gancher, Bryan Parno

This article delves into **OwlC**, a groundbreaking compiler presented at USENIX Security that addresses a critical gap in the security of cryptographic protocols. While high-level designs of protocols like TLS and WireGuard have long benefited from formal verification, their real-world implementations often remain susceptible to vulnerabilities due to a lack of rigorous, automated security guarantees. OwlC bridges this divide by automatically generating verified, high-performance, and side-channel-resistant Rust libraries directly from high-level protocol specifications written in the Owl language.

AI review

This is foundational work. OwlC is the first fully automated compiler that takes a high-level protocol spec and spits out verified, side-channel-resistant, performant Rust—and they proved it on WireGuard and HPKE with numbers that match or beat industrial baselines. The gap between 'we verified the design' and 'we verified the implementation' has been a festering wound in this field for decades. They actually closed it.