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