Resolving the conflict between generality and plausibility in verified computation
The area of proof-based veriﬁed computation (outsourced computation built atop probabilistically checkable proofs and cryptographic machinery) has lately seen renewed interest. Although recent work has made great strides in reducing the overhead of naive applications of the theory, these schemes still cannot be considered practical. A core issue is that the work for the server is immense, in general; it is practical only for hand-compiled computations that can be expressed in special forms. This paper addresses that problem. Provided one is willing to batch veriﬁcation, we develop a protocol that achieves the efﬁciency of the best manually constructed protocols in the literature yet applies to most computations. We show that Quadratic Arithmetic Programs, a new formalism for representing computations efﬁciently, can yield a particularly efﬁcient PCP that integrates easily into the core protocols, resulting in a server whose work is roughly linear in the running time of the computation. We implement this protocol in the context of a system, called Zaatar, that includes a compiler and a GPU implementation. Zaatar is almost usable for real problemsówithout special-purpose tailoring. We argue that many (but not all) of the next research questions in veriﬁed computation are questions in secure systems.