CS Talk
Joshua Gancher
Host: Fan Zhang
Title: New Techniques for Secure-by-Construction Cryptography
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 new tools and techniques for bringing cryptographic
protocol verification to scale. First, I will present Owl, a new type system
for proving security protocols such as TLS and WireGuard secure in an automated
and modular way; 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.