PEPPER: Toward practical verified computation

Our project is investigating ways of making verified computation practical. By verified computation, we mean a system that implements the following picture:

The motivation is the rise of third-party computing: increasingly, computation is provided by an entity other than the actual "consumer" of the computation. Examples include cloud computing, volunteer computing (in which a central project computer outsources to volunteers' computers, which play the role of servers in the above picture), peer-to-peer computing, and more.

In this environment, many things can go wrong; the litany includes software bugs, hardware defects, misconfigurations, operator error, malicious insiders, and far more. Thus, we don't want to assume that the server is implemented correctly, or that its failure modes are known, or that it has trusted hardware, or that it uses replication, or how many replicas it has, or whether those replicas can fail, etc.

The properties that we desire from the system are as follows:

1. Unconditional. As mentioned above, the client should ideally not have to make any assumptions about the server.
2. General-purpose. The system should not be specialized to a particular family of functions.
3. Practical, or at least conceivably so.

Previous work in the area of verifying remote computations has not met all three of these properties (our publications below give detail).

Our approach is to apply the theory of Probabilistically Checkable Proofs (PCPs) and two closely related constructs: argument systems and interactive proofs. PCPs have several central roles in complexity theory. In one of those roles, PCPs demonstrate that it is possible (in theory) to check a mathematical proof by investigating only a few bits of that proof. In our context, this implies that the picture above has a solution, one that is unconditional and general-purpose. However, PCPs, as described in the literature, have not been remotely practical (for instance, it would take trillions of years for the server to produce a proof). This leads to the question: can we incorporate PCPs into a built system?

So far, we have been able to come close.

Our line of work on Pepper, Ginger, and Zaatar has instantiated an argument system (an interactive protocol that assumes a computationally bounded prover) due to Ishai, Kushilevitz, and Ostrovsky (CCC 2007), in this paper (also available here). Through theoretical and practical refinements, we have reduced the cost of this argument system by roughly 20 orders of magnitude (a factor of 10²⁰).

In another strand of work, Allspice, we have built on an interactive proof system due to Goldwasser, Kalai, and Rothblum (STOC 2008), and refined and implemented by Cormode, Mitzenmacher, and Thaler (ITCS 2012). One of the chief advantages of this line of work is that it avoids expensive cryptographic operations.

One might wonder: which protocol is "best"? Our experience has been that it depends on the computation. Accordingly, we have built a compiler that takes as input a high-level programming language and performs static analysis to compile to the optimal verified computation protocol for that computation.