I study topics related to formal methods, cryptography, and distributed systems.
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 a clever integrating 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]