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? The applications of such a primitive include cloud computing (a computationally limited device offloads processing to the cloud [11] but does not assume the cloud’s correctness [12]); volunteer computing (some 30 projects use the BOINC [1] software platform to leverage volunteers’ spare cycles, but some “volunteers” return wrong answers [2]); and high-assurance computing (a machine may be remotely deployed and subject to physical tampering).