Joshua Gancher – New Techniques for Secure-by-Construction Cryptography
Grier Room B
Abstract
We rely on cryptographic protocols every day to secure our digital lives. Since these protocols are so important, developers invest a huge amount of energy into making sure that they are themselves secure; nevertheless, critical vulnerabilities still happen. To end the cycle of security vulnerabilities and patches, I advocate for using formal verification: machine-checkable, mathematically precise proofs for security and correctness. In this talk, I will describe my work bringing cryptographic protocol verification to scale. First, I will present Owl, a new type system that delivers automated and modular security proofs for protocols such as TLS and WireGuard; next, I will present IPDL, which presents a compositional, equational logic for security proofs of distributed cryptography such as Secure Multi-Party Computation. Finally, I will conclude by describing my vision for a next-generation ecosystem of secure software.
Bio
Joshua Gancher is a postdoctoral fellow at Carnegie Mellon University, working at the intersection of Programming Languages and Cryptography to give formal guarantees to secure systems. His work appears in venues including POPL, PLDI, IEEE S&P, and CCS.
Details
- Date: Tuesday, March 5
- Time: 10:00 am - 11:00 am
- Category: EECS Seminar
- Location: Grier Room B
Host
- Professor Adam Chlipala
- Email: adamc@csail.mit.edu