Introduction
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:
- Unconditional. As mentioned above, the client should not have to make any assumptions about the server.
- General-purpose. The system should not be specialized to a particular family of functions.
- 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?
What is our approach?
We turn to argument systems. An argument system is an interactive protocol with two actors, a prover and a verifier, and efficient argument systems have been based on PCPs. The purpose of the interaction between the prover and the verifier is for the verifier to commit the prover to a particular PCP, thereby forcing the prover to act like a fixed proof. In other words, efficient argument systems are a way of coopting the server to "front" a PCP.
The most promising (that is, most likely to yield a practical implementation) efficient argument system that we know of is due to Ishai, Kushilevitz, and Ostrovsky, in this paper (also available here). Our work has focused on trying to make this argument system practical.
What is PEPPER?
PEPPER is a built system that refines the protocol of Ishai et al. PEPPER shrinks program encoding (via a concise representation that generalizes arithmetic circuits), reduces the cost of commitment (via a stronger and streamlined commitment primitive), and amortizes the verifier's costs (via batching). Furthermore, PEPPER can use tailored PCP encodings for certain classes of problems, resulting in a protocol in which the prover's total work is (in complexity theoretic terms) the same as executing the computation. As server overhead has been an issue in previous PCP schemes, this tailored PCP encoding is a key innovation in PEPPER.
We have proved the soundness of these refinements. The result is a constant-round protocol that reduces the running time by a factor of 1020 over a naive implementation of the protocol of Ishai et al. The system is (arguably) practical in some cases. Our conclusion so far is that, as a tool for building secure systems, PCPs and argument systems are not a lost cause.