CS Talk - Joshua Gancher

Event time: 
Monday, February 26, 2024 - 4:00pm
AKW 200 See map
51 Prospect Street
New Haven, CT 06511
Event description: 

CS Talk
Joshua Gancher

Host: Fan Zhang

Title: New Techniques for Secure-by-Construction Cryptography


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. 


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.