Resolving the conflict between generality and plausibility in verified computation
Proceedings of the ACM European Conference on Computer Systems (EuroSys) 2013.
View
PDF or BibTeX.
areas
Security
abstract
The area of proof-based verified 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 verification, we develop a protocol that achieves the
efficiency 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 efficiently, can yield a particularly
efficient 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 verified computation are questions in secure systems.