Crypto Seminar - John Kolesar

— 1:00pm

Location:
In Person and Virtual - ET - Blelloch-Skees Conference Room, Gates Hillman 8115 and Zoom

Speaker:
JOHN KOLESAR, Ph.D. Student, Department of Computer Science, Yale University
https://johnckolesar.github.io/

Zero-Knowledge Proofs for SMT Theorems and Regular Expression Equivalence

Zero-knowledge (ZK) protocols allow software developers to provide proofs of their programs' correctness to other parties without revealing the programs themselves.  Most prior work in the domain of ZK verification has focused on the encoding of witnesses for satisfiability proofs, but the task of encoding proof trees for demonstrating that a formula is unsatisfiable has received comparatively little attention.  We introduce ZKSMT, the first zero-knowledge protocol designed for encoding unsatisfiability proofs generated by SMT solvers.  We design a virtual machine (VM) structure for proofs that enables the prover to hide the structure of a proof while still manipulating complex ASTs for terms and formulas.  We use ZKSMT to validate SMT proofs involving equality with uninterpreted functions (EUF) and linear integer arithmetic (LIA).  In terms of performance, ZKSMT achieves a three-order-of-magnitude improvement over general-purpose ZK protocols. 

Along with SMT proof validation, we tackle another novel problem for ZK proofs:  the problem of checking whether two regular expressions are equivalent.  We introduce Crepe, the first ZK protocol for encoding regular expression equivalence proofs.  For the proofs that Crepe validates, we introduce a new custom calculus of proof rules based on regular expression derivatives and coinduction.  We prove the calculus sound and complete, and we provide a decision procedure for generating proofs in our format.  We test our proof generator on a suite of thousands of equivalent regular expression pairs, and we test Crepe on the proofs that we generate.  The proof generator scales effectively, and Crepe itself can validate large equivalence proofs in only a few seconds each. 

— 

John Kolesar is a fifth-year Ph.D. student in computer science at Yale University advised by Ruzica Piskac.  His dissertation research combines automated program verification and zero-knowledge proofs.  His other research interests include functional programming, symbolic execution, automatic program repair, and software-defined networking.  He has held research intern positions at both Microsoft and Amazon Web Services.  Before coming to Yale, he earned a bachelor's degree at Cornell, where he did research work with Nate Foster. 

In Person and Zoom Participation.  See announcement.

Event Website:
https://sites.google.com/view/crypto-seminar/home

Add event to Google
Add event to iCal