EECS Special Seminar: Joshua Gancher - New Techniques for Secure-by-Construction Cryptography
Speaker
Joshua Gancher
Carnegie Mellon University
Host
Professor Adam Chlipala
EECS
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.
********
Join Zoom Meeting
https://mit.zoom.us/j/91089942246
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.
********
Join Zoom Meeting
https://mit.zoom.us/j/91089942246