Making proof-based verified computation almost practical

Seminar: Departmental | December 5 | 12-1 p.m. | 310 Soda Hall

Speaker/Performer: Michael Walfish, University of Texas, Austin

Sponsor: Electrical Engineering and Computer Sciences (EECS)

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? And how can this be done without assumptions about the performer (replication, trusted hardware, etc.) or restrictions on the computation? This is the problem of _verified computation_, and it is motivated by the cloud and other third-party computing models. It has long been known that (1) this problem can be solved in theory using probabilistically checkable proofs (PCPs) coupled with cryptographic tools, and (2) the performance of these solutions is wildly impractical (trillions of CPU-years or more to verify simple computations).

I will describe a project at UT Austin that challenges the second piece of this folklore. We have developed an interactive protocol that begins with an efficient argument [IKO CCC ´07] and incorporates new theoretical work to improve performance by 20+ orders of magnitude. In addition, we have broadened the computational model from Boolean circuits to a general-purpose model. We have fully implemented the system, accelerated it with GPUs, and developed a compiler that transforms computations expressed in a high-level language to
executables that implement the protocol entities.

The resulting system, while not quite ready for the big leagues, is close enough to practicality to suggest that in the near future, PCPs could be a real tool for building actual systems.

Talk will be based on these papers and ongoing work:
http://www.cs.utexas.edu/~mwalfish/papers/ginger-usec12.pdf
http://www.cs.utexas.edu/~mwalfish/papers/pepper-ndss12.pdf

Event Contact: alig@cs.berkeley.edu