### 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]

**Buffet**

Buffet eliminates what was
a problematic cost-programmability tradeoff in this research area. Prior
to Buffet, there were two approaches to program representation. One
approach, due to Ben-Sasson et al., Usenix
Security 2014, offered excellent programmability (the full C
programming language) but substantial overhead. Another approach
(embodied by Pantry, Pinocchio,
and Zaatar) offered much lower overhead but could not handle
data-dependent control flow. Buffet takes Pantry as a base and applies
static program analysis (including loop flattening) together with an
adaptation of BCTV's elegant
representation of RAM. Buffet can handle essentially any example in
the verifiable computation literature (it supports an expansive subset
of C, disallowing only goto and function pointers) and achieves the
best performance in the area by multiple orders of magnitude.

R. S. Wahby, S. Setty, Z. Ren, A. J. Blumberg, and M. Walfish, "Efficient RAM and control
flow in verifiable outsourced computation."
Network & Distributed System Security Symposium,
NDSS
2015, February 2015. [pdf]

A slightly longer version is available as Cryptology ePrint 2014/674.

A slightly longer version is available as Cryptology ePrint 2014/674.

**Zebra**

Zebra instantiates a new model
for building trustworthy chips, called Verifiable ASICs.
This model uses a high-performance chip from an untrusted (and possibly malicious)
hardware vendor to accelerate the computation of a low-performance
chip supplied by a trusted vendor, while retaining the latter's trustworthiness.
To instantiate the model, Zebra builds on the interactive proofs of
GKR,
CMT,
and Allspice.
Zebra demonstrates that, for a class of real computations, the Verifiable ASICs approach
reduces costs and improves performance compared to chips built solely by a trusted
manufacturer.

R. S. Wahby, M. Howald, S. Garg, a. shelat, and M. Walfish, "Verifiable ASICs."
IEEE Symposium on Security and Privacy (Oakland), May 2016.
[pdf]

An extended version is available as Cryptology ePrint 2015/1243.

*(Distinguished student paper award.)*An extended version is available as Cryptology ePrint 2015/1243.