CS Talk
Alex Ozdemir
Host: Ruzica Piskac
If you would like to meet with Alex, please let Ruzica know.
Title: CirC: Unifying Compilers for SNARKs, SMT, and More [Oakland’22]
Authors: Alex Ozdemir, Fraser Brown, Riad S. Wahby
Abstract:
We present CirC (“SIR-see”): a compiler infrastructure that aims to support zero-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
* …
Presenter:
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.
Paper link: https://eprint.iacr.org/2020/1586