I study topics related to formal methods, cryptography, and distributed systems.

A full list of papers can be found here.

Read below for project summaries.

Efficient Storage for Verifiable Computation

The circuit for updating an RSA accumulator. We show how to implement it within a SNARK.

Cryptographers have shown that you can certify the correct execution of a program using proofs that (a) are verifiable in constant time and (b) keep the inputs to the program hidden. These systems are called zk-SNARKs (Zero Knowledge Succinct Non-Interactive Arguments of Knowledge) and they power crypto-currencies like Zcash.

A pervasive but tough problem for these systems is how to manipulate persistent memory. Traditionally these systems have summarized that memory with a hash tree, and proven that the program updates it correctly. We argue that there’s a better way, using RSA Accumulators.

Using Modern Proofs of Unsatisifability for Bit-Vectors

Modern SAT solvers produce complex proofs of unsatisfiability. Modern bit-vector solvers translate bit-vector queries into SAT queries. To make full use of modern SAT solvers, the bit-vector solver must be able to translate the unsatisfiability proofs back into the language of bit-vectors. We explore three ways of doing this, exploring the trade-off between transaction-time and proof-check-time.

Clustering Phylogeny Reconciliations

A pair of related phylogenies and two reconciliations.

Within genomics, researchers study phylogenies: the evolutionary trees that represent the genetic history of a family of species.

When two families share a close relationship (e.g., fig trees and fig-wasps), their evolutionary histories should be related, and it is useful to reconcile them: i.e. to line them up with a minimal number of disagreements.

There are fast algorithms for finding good reconciliations, but it turns out that there are often exponentially many good reconciliations, so examining all of them isn’t reasonable.

My collaborators and I studied the metric space of good reconciliations and showed how classic clustering algorithms could be run in this space. Our algorithms require time polynomial in the phylogeny size, even when there are exponentially many good reconciliations.