### Built systems under the Pepper project

In the descriptions below, the *prover* is the
entity that performs a computation. The
*verifier* checks a proof (produced by the
prover) that the computation was performed
correctly.

**Pepper**

Pepper is the first system to challenge the folklore that
PCP-derived machinery is impractical. Pepper implements an efficient argument system based on a
protocol of Ishai et al., CCC 2007, and incorporates new
theoretical work to improve performance by 20 orders of magnitude.
Pepper is implemented and experimentally evaluated, and is arguably
practical for some computations and in some regimes.

S. Setty, R. McPherson, A. J.
Blumberg, and M. Walfish, “Making argument
systems for outsourced computation practical
(sometimes)”, Network & Distributed
System Security Symposium (NDSS), February 2012.
[pdf]

**Ginger**

Ginger is based on Pepper. It slashes query costs via
further refinements. In addition, Ginger broadens the
computational model to include (primitive) floating-point
fractions, inequality comparisons, logical operations, and
conditional control flow. Ginger also includes a parallel
GPU-based implementation, and a compiler that transforms
computations expressed in a high-level language to
executables that implement the protocol entities.

S. Setty, V. Vu, N. Panpalia,
B. Braun, A. J. Blumberg, and M. Walfish,
“Taking proof-based verified computation a
few steps closer to practicality”, USENIX
Security Symposium, August 2012. [pdf (corrected)]

**Zaatar**

Zaatar addresses a limitation in Ginger, namely that
avoiding immense work for the prover requires
computation-specific tailoring of the protocols. Zaatar is
built on our observation that the QAPs of Gennaro et al., EUROCRYPT 2013
yield a linear PCP that works with the
Ginger/Pepper/IKO framework and is (relatively) efficient for the prover.
The consequence is a prover whose total work is not much
more than linear in the running time of the computation (and
does not require special-purpose tailoring).

S. Setty, B. Braun, V. Vu, A.
J. Blumberg, B. Parno, and M. Walfish,
“Resolving the conflict between generality
and plausibility in verified computation”,
ACM European Conference on Computer Systems
(EuroSys), April 2013. [pdf]

**Allspice**

Allspice addresses a key
limitation of prior work for verifying computations: either it
relies on cryptography, which carries an expense (as with Zaatar,
Ginger, Pepper, and IKO), or else it applies to a restricted class
of computations (as with work by Cormode et al., ITCS 2012, which
builds on an interactive proof system of Goldwasser et al., STOC
2008). Allspice optimizes the non-cryptographic
protocols and extends them to a much larger class of computations.
Allspice also uses static analysis to compile an input program to
the best verification machinery for that program.

V. Vu, S. Setty, A. J. Blumberg, and M. Walfish,
“A hybrid architecture for interactive
verifiable computation”, IEEE Symposium on
Security and Privacy (Oakland), May 2013. [pdf]

**Pantry**

Pantry extends
verifiable computation to handle

*stateful*computations: those that work over RAM, or computations for which the verifier does not have the full input. Pantry composes techniques from untrusted storage with existing verifiable computation machinery: the verifier’s explicit input includes a*digest*of the full input or state, and the prover is obliged to compute over state that matches the digest. The result is to extend verifiability to real applications of cloud computing (MapReduce jobs, queries against remote databases, applications for which the prover’s state is hidden, etc.). Besides the gain in expressiveness, Pantry improves performance: by not handling inputs, the verifier saves CPU and network costs.
B. Braun, A. J. Feldman, Z. Ren, S. Setty, A. J.
Blumberg, and M. Walfish, “Verifying
computations with state”, ACM Symposium on
Operating Systems Principles (SOSP), November
2013. [pdf]