My goal is to make secure systems as easy to build as insecure ones.

Towards this goal, I use cryptography, compilers, and automated reasoning to improve programmable cryptosystems. Programmable cryptosystems (such as zero-knowledge proofs, multi-party computation, and homomorphic encryption) are powerful tools for building systems with strong privacy and security guarantees—without cryptographic or security expertise.

zkPi: Zero-Knowledge Proofs for Lean Theorems
Evan Laufer, Alex Ozdemir, Dan Boneh
[CCS ‘24]
We build the first zero-knowledge, succinct proofs for Lean theorems. One potential application is safety proofs for proprietary software. [preprint]
Split Gröbner Bases for Satisfiability Modulo Finite Fields
Alex Ozdemir, Shankara Pailoora, Alp Bassa, Kostas Ferles, Clark Barrett, Işıl Dillig
[CAV ‘24]
We improve an SMT solver for finite fields by splitting up the Gröbner basis it uses. [preprint]
An SMT-LIB Theory of Finite Fields
Thomas Hader, Alex Ozdemir
[SMT ‘24]
We propose an SMT-LIB standard for finite fields.
Generating and Exploiting Automated Reasoning Proof Certificates
Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
[CACM ‘23]
We make the case for automatically constructible and checkable proofs of program correctness. [paper]
Bounded Verification for Finite-Field-Blasting (in a Compiler for Zero Knowledge Proofs)
Alex Ozdemir, Riad Wahby, Fraser Brown, Clark Barrett
[CAV ‘23]
We explore automatic verification for a finite-field blaster: a key component of compilers for zero-knowledge proofs. Along the way, we find 4 bugs in an existing finite-field blaster. [preprint]
Satisfiability Modulo Finite Fields
Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark Barrett
[CAV ‘23]
We build finite-field reasoning into an SMT solver. This is a key tool for automated cryptographic verification. [preprint]
Silph: A Framework for Scalable and Accurate Generation of Hybrid MPC Protocols
Edward Chen, Jinhao Zhu, Alex Ozdemir, Riad S. Wahby, Fraser Brown, Wenting Zheng
[Oakland ‘23]
Leveraging CirC, we build a high-performance compiler to hybrid multi-party computations using a clever integrating of graph partitioning and integer-linear programming. [preprint]
Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark Barrett
[FMCAD ‘22]
We study producing a single refutation for an unsatisfiable formula solved with divide-and-conquer parallelism. [preprint]
Collaborative zk-SNARKs: Zero-Knowledge Proofs for Distributed Secrets
Alex Ozdemir, Dan Boneh
[USENIX Security ‘22]
We define Collaborative zk-SNARKs: zero knowledge proofs about distributed secrets. Surprisingly, they are nearly as efficient as conventional zk-SNARKs: (which only support one party’s secrets). [code] [preprint]
cvc5: A Versatile and Industrial-Strength SMT Solver
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar
[TACAS ‘22]
We present the design of cvc5, the latest in the series of “CVC” SMT solvers. Best tool paper [code] [paper]
Flexible Proof Production in an Industrial-Strength SMT Solver
Haniel Barbosa, Hanna Lachnitt, Andrew Reynolds, Gereon Kremer, Alex Ozdemir, Aina Niemetz, Andres Nötzli, Scott Viteri, Mathias Preiner, Arjun Viswanathan, Clark Barrett, Yoni Zohar, Cesare Tinelli
[IJCAR ‘22]
We present the design of cvc5’s proof system. [paper]
R2E2: low-latency path tracing of terabyte-scale scenes using thousands of cloud CPUs
Sadjad Fouladi, Brennan Shacklett, Fait Poms, Arjun Arora, Alex Ozdemir, Deepti Raghavan, Pat Hanrahan, Kayvon Fatahalian, Keith Winstein
We build a massively parallel ray-tracer for massive scenes using serverless executors. [code]
Efficient Functional Commitments: How to Commit to a Private Function
Dan Boneh, Wilson Nguyen, Alex Ozdemir
In submission
We allow the evaluator of a secret function to prove that they are evaluating that function uniformly. The might be applicable to credit scores or bail decisions. [preprint]
CirC: Unifying Compilers for SNARKs, SMT, and More
Alex Ozdemir, Fraser Brown, Riad Wahby
[Oakland ‘22]
We define and develop a compiler infrastructure from high-level languages to zero-knowledge proofs, SMT formulae, and other existentially quantified circuits. [code] [preprint]
SAT Solving in the Serverless Cloud
Alex Ozdemir*, Haoze Wu*, Clark Barrett
[FMCAD ‘21]
We develop a parallel divide-and-conquer SAT solver compatible with serverless executors. Along the way, we build a new interface to gg, which has since been upstreamed. [paper]
High-level high-speed high-assurance crypto
Jonathan Cogan, Fraser Brown, Alex Ozdemir, Riad S. Wahby
[PriSC ‘21]
We explore the design of high-level programming languages for cryptography.
Parallelization Techniques for Verifying Neural Networks
Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, Clark Barrett
[FMCAD ‘20]
We explore parallelization techniques and heuristics for verifying properties of small neural networks. [paper]
Scaling Verifiable Computation Using Efficient Set Accumulators
Alex Ozdemir, Riad Wahby, Barry Whitehat, Dan Boneh
[USENIX Security ‘20]
We show that, in a zkSNARK, RSA accumulators provide better storage than Merkle trees for sufficiently many accesses to a sufficiently large memory. Along the way we design new hash functions and analyze consistency semantics for batched operations. [code] [paper] [slides]
DRAT-based Bit-Vector Proofs in CVC4
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark Barrett
[SAT ‘19]
We experiment with a variety of techniques for integrating the DRAT proofs of a SAT solver into an SMT bit-vector solver. [paper]
Clustering the Space of Maximum Parsimony Reconciliations in the Duplication-Transfer-Loss Model
Alex Ozdemir, Michael Sheely, Daniel Bork, Ricson Cheng, Reyna Hulett, Jean Sung, Jincheng Wang, Ran Libeskind-Hadas
[ALCOB ‘17]
We build clustering and evaluation algorithms for joint evolutionary histories (cophylogenies). These algorithms run in time sub-linear in the size of the sets that they cluster. [paper]