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.

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.

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

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.

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.

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.

Giraffe builds on the Verifiable ASICs model introduced by Zebra. Giraffe removes Zebra's requirement that a trusted entity supply the verifier with an endless stream of precomputations. In doing so, it charges for all protocol costs and makes outsourcing with probabilistic proofs worthwhile for the first time.

Giraffe includes a new probabilistic proof for data-parallel computations that refines the protocol of Thaler13 to give asymptotically optimal prover cost; this is of independent interest. Giraffe also develops a design template that automatically produces optimized hardware designs for a wide range of computations and circuit technologies. It combines this template with program analysis and compiler techniques that extend the Verifiable ASICs model to a wider range of computations. Compared to Zebra, Giraffe handles computations that are 500× larger, and it can automatically outsource parts of programs that are not worthwhile to outsource in full.