My goal is to make private and 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) have the potential to allow non-experts to easily build systems with strong privacy and security guarantees.
Volatile and Persistent Memory for zkSNARK via Algebraic Interactive Proofs
We improve zkSNARKs for different kinds of RAM via a new intermediate
representation: algebraic interactive proofs.
[preprint]
Efficient Proofs of Possession for Legacy Signatures
We improve zkSNARKs
for standardized and widely deploy signature schemes:
RSA, ECDSA, and Ed25519.
zkPi: Zero-Knowledge Proofs for Lean Theorems
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
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
We propose an SMT-LIB standard for finite fields.
[paper]
Generating and Exploiting Automated Reasoning Proof Certificates
We make the case for automatically constructible and checkable proofs of
correctness.
[paper]
Bounded Verification for Finite-Field-Blasting (in a Compiler for Zero Knowledge Proofs)
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
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
Leveraging CirC, we build a high-performance compiler to hybrid
multi-party computations using an combination of graph partitioning and
integer-linear programming.
[preprint]
Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
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
cvc5: A Versatile and Industrial-Strength SMT Solver
Flexible Proof Production in an Industrial-Strength SMT Solver
We present the design of cvc5’s proof system.
[paper]
R2E2: low-latency path tracing of terabyte-scale scenes using thousands of cloud CPUs
We build a massively
parallel ray-tracer
for massive scenes
using serverless executors.
[code]
Efficient Functional Commitments: How to Commit to a Private Function
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
SAT Solving in the Serverless Cloud
High-level high-speed high-assurance crypto
We explore the design of high-level programming languages
for cryptography.
Parallelization Techniques for Verifying Neural Networks
We explore parallelization techniques and heuristics for
verifying properties of small neural networks.
[paper]
Scaling Verifiable Computation Using Efficient Set Accumulators
DRAT-based Bit-Vector Proofs in CVC4
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
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]