Security protocols, such as TLS, Kerberos, and WireGuard, are not only complex in their implementations -- often involving nontrivial optimizations for maximal performance -- but are also complex in their designs, requiring significant proof effort to verify their cryptographic security guarantees. Thus, to confidently rely on these protocols for security-critical tasks, we need to ensure that these protocols are simultaneously running correctly and implement secure designs.
To address this need, we introduce Owl, a new programming language for developing security protocols. Using Owl, developers express their protocols using a novel mix of refinement and information flow types; in turn, all well-typed programs are guaranteed to be secure. Indeed, Owl, for the first time, simultaneously guarantees computational soundness against PPT attackers, a high degree of proof automation, and type-based abstractions for modular protocol developments.
This talk will introduce our work on Owl, including our new proof techniques for guaranteeing the existence of cryptographic reductions via type systems, and our ongoing work to extract verified, high-performance Rust code from Owl protocols using the Verus toolchain.
18 сен 2024
