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