OwlC: Compiling Security Protocols to Verified, Secure...
summary
OwlC compiles Owl protocol specifications into side‑channel‑resistant Rust libraries and mechanically verifies their fidelity to an itrees specification using the Varys verifier; it enforces effect-only I/O with ghost linear permission tokens and allows compiler-checked declassification from the Owl cryptographic analysis. The pipeline produces interoperable drop‑in WireGuard and HPKE libraries, matches WireGuard Go performance in end‑to‑end benchmarks, and reports a maximum measured overhead of 6% overhead while avoiding explicit and implicit secret leaks.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 1:58Protocol design to code
- 4:03Preventing information leakage
- 6:50Blocking side-channel attacks
- 9:23Compiler pipeline and verification
- 10:24WireGuard case study
- 12:54Conclusion
related talks
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
39mKeynote: Towards High-Assurance Cryptographic Software
12mAutomated Synthesis of Verified Firewalls
09mFormally Secure Hardware with Rust
21mSecuring Verified IO Programs Against Unverified Code in F*
01h 04mSoftware Verification meets Real-World Cryptography
12mHardware Verification of Timing Side Channel Freedom in the Spectre Era
30mA Case Study in Language-Based Security: Building an I/O Library for Wyvern