Pequin: An end-to-end toolchain for verifiable computation, SNARKs, and probabilistic proofs
Pequin is a toolchain to verifiably execute programs expressed in (a
large subset of) the C programming language. There are two parties: a
prover and verifier. Using Pequin, the prover can convince the
verifier that it executed a given computation according to the program
expressed by the verifier. More generally, using Pequin, the prover can
convince the verifier of the truth of some assertion, without the
verifier having to manually check every line of the proof of that
Pequin consists of a front-end and a back-end. The front-end takes C
programs and transforms them to a set of arithmetic constraints, in
such a way that the constraints are satisfiable if and only if the
purported output (which will be produced by the prover, and which is
represented by variables in the constraints) is what the original
program would have produced. The back-end is a probabilistic proof
protocol by which the prover convinces the verifier that the constraints
are indeed satisfiable (if they are); if the constraints are not
satisfiable, the verifier is not fooled, except with vanishingly low
The specific back-end in Pequin is a zk-SNARK (zero-knowledge succinct
non-interactive argument of knowledge). Pequin uses SCIPR Lab's
libsnark, which is an
optimized implementation of the back-end of
itself a refinement and implementation of
Pequin is a result of several years of research in the Pepper
project, done at NYU and UT Austin.
Pepper has brought to bear powerful techniques from
complexity theory and cryptography: probabilistically checkable proofs
(PCPs), efficient arguments, interactive proofs (IPs) etc.
Pepper's research results include
reducing the computational costs of a PCP-based efficient argument by
over 20 orders of magnitude (in base 10!), and extending verifiability to
representative uses of cloud computing (MapReduce jobs, simple
database queries, computations involving private databases, etc.).
These results and others are published in peer-reviewed scientific
Pepper itself has code;
the goal of Pequin in particular is to be easier to use, and more composable. Development is ongoing. Please open issues or
submit pull requests! (This source code is released under a BSD-style
license. See LICENSE for more details.)
What's coming next?
- Incorporating other back-ends
- Improving documentation and usability of this codebase is ongoing.
Installation and first steps
This codebase depends on several external libraries. Installation
scripts are provided for a few common linux distros. For example,
on Ubuntu 14.04 or Debian Jessie,
will install some packages from apt repositories and compile our
snapshots of some third-party dependencies. (You will be
prompted to enter your password to install the apt packages as
./install_buffet.shwill build the patched Clang/LLVM libraries for
Buffet's C-to-C compiler, needed for running computations with
data-dependent loops and control flow.
Once everything is set up, you're ready to run some verifiable
computations! Please see GETTINGSTARTED.md for a quick overview of the process.
Please contact email@example.com for any questions and comments. We are happy to work with you to adapt this technology into your application.