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