Security Seminar: Alex Ozdemir on “CirC: Unifying Compilers for SNARKs, SMT, and More”, Friday Feb. 11th at 11 AM PT
February 11, 2022
Title: CirC: Unifying Compilers for SNARKs, SMT, and More
Speaker: Alex Ozdemir (Stanford)
Time: Fri Feb 11 at 11AM
Zoom link: https://berkeley.zoom.us
In-person location: Soda 465H
Abstract: We present CirC (“SIR-see”): a compiler infrastructure that aims to supportzero-knowledge proof systems, multi-party computations, fully homomorphic encryption, constraint solving, and optimization. We observe that these seemingly disparate cryptosystems and verification problems share a common model of computation. This model is characterized by being state-free, non-uniform, and non-deterministic—we call it the *existentially quantified circuit (EQC)*. The common model admits a shared compiler infrastructure (CirC) for compiling different high-level languages to different circuit representations used by these systems.
We show:
(1) CirC makes it easy to build new compilers for these systems
* e.g., we reproduce and improve on a 28k LOC compiler in 700 LOC.
(2) CirC’s compilers perform well (by leveraging shared optimizations)
(3) CirC enables “cross-overs” in which different back-end systems are combined in the service of a shared optimization
* SMT+ZKP = zero-knowledge bug bounties
* SMT+X = SMT assisted optimization
* …
This is joint work with Fraser Brown and Riad S. Wahby.
Bio: Alex Ozdemir is a Phd student at Stanford, studying cryptography and formal methods. Lately, he’s been investigating how cryptographic proof systems can be made more useful, sometimes by using techniques from formal methods and programming languages.