Toward practical and unconditional verification of remote computations
This paper revisits a classic question: how can a machine specify a computation to another one and then, without executing the computation, check that the other machine carried it out correctly? We want a scheme that (a) has practical performance, (b) is simple to implement, and (c) provides unconditional guarantees. Of these goals, (a) and (b) contrast with the way this question is handled in the theory literature and (c) contrasts with current systems approaches. Our approach is to revisit the theory of interactive proofs and probabilistically checkable proofs (PCPs) and attempt to reduce it to practice. We do so by identifying a strand of theory that can lead to a practical solution and then applying several refinements that reduce the costs by over 12 orders of magnitude. Our resulting prototype meets goals (a)--(c) but only over a limited domain. In this partial success, the prototype provides a concrete foundation for our position: that PCP-based verifiable computation can be a systems problem, not just a theory problem. In its shortcomings, the prototype illustrates how much research remains, a gap that we hope to close with the help of the community's expertise.