"Verifying the correctness of remote executions: from theoretical
possibility to near practicality"

Abstract:

How can a machine specify a computation to another one and then, without
executing the computation, check that the remote machine carried it out
correctly? And how can this be done without assumptions about the
performer (replication, etc.) or restrictions on the computation? This
is a classic problem in systems security, and is relevant in multiple
contexts: cloud computing, an untrusted hardware supply chain, etc. For
decades, it has been known that this problem can be solved in theory,
using probabilistically checkable proofs (PCPs) coupled with
cryptographic tools. The rub was practicality: if implemented naively,
the theory would be astronomically more expensive than simply executing
the computation locally.

Over the last several years, a number of projects have brought this
theory to near practicality. In this emerging area of _proof-based
verifiable computation_, the pace of progress has been rapid, and there
have been many encouraging developments: factors-of-a-trillion speedups,
compilers that transform from high-level programs to executables that
implement the protocol entities, and sophisticated implementations.

I will discuss the general area and my group's efforts in refining
theory and building systems. A notable recent result is our Buffet
system. Buffet has very good expressivity (it handles almost the entire
C programming language as well as setups such as remote MapReduce jobs,
database queries, etc.) and achieves the best performance in the area by
multiple orders of magnitude. I will also cover the remaining obstacles
to practicality in this research area; my hope is to communicate
cautious optimism, with the emphasis on cautious.

----

Michael Walfish is an associate professor in the CS department in the
Courant Institute at New York University (NYU), which he joined in 2014.
Prior to that, he was an assistant professor at The University of Texas
at Austin. His research interests are in systems, security, and
networking.  His honors include an Air Force Young Investigator Award,
an NSF CAREER Award, a Sloan Research Fellowship, a Teaching Excellence
Award from the UT College of Natural Sciences, the Intel Early Career
Faculty Honor Program, and the UT Society for Teaching Excellence. He
received his B.A. from Harvard and his Ph.D. from MIT, both in Computer
Science.