Principles of Programming Seminar

— 4:30pm

Location:
In Person - Newell-Simon 3305

Speaker:
JOSHUA GANCHER, Postdoctoral Fellow, Computer Science Department, Carnegie Mellon University
https://gancher.dev/

Owl: Compositional Verification of Security Protocols via an Information-Flow Type System

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 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 probabilistic, polynomial time 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.

—

Joshua Gancher is a postdoctoral fellow at Carnegie Mellon University, working with Bryan Parno. He obtained his Ph.D. from Cornell University, advised by Elaine Shi and Greg Morrisett. His research is about using formal methods and programming language techniques to secure the designs and implementations of cryptographic protocols.