International Association
for Cryptologic Research

Recent work on proof-based verifiable computation has resulted in built

systems that employ tools from complexity theory and cryptography to

address a basic problem in systems security: allowing a local computer

to outsource the execution of a program while providing the local

computer with a guarantee of integrity and the remote computer with a

guarantee of privacy. However, support for programs that use RAM and

complicated control flow has been problematic. State of the art systems

restrict the use of these constructs (e.g., requiring static loop

bounds), incur sizable overhead on every step to support these

constructs, or pay tremendous costs when the constructs are invoked.

This paper describes Buffet, a built system that solves these problems

by providing inexpensive \"a la carte\" RAM and dynamic control flow

constructs. Buffet composes an elegant prior approach to RAM with a

novel adaptation of techniques from the compiler community. The result

is a system that allows the programmer to express programs in an

expansive subset of C (disallowing only \"goto\" and function pointers),

can handle essentially any example in the verifiable computation

literature, and achieves the best performance in the area by multiple

orders of magnitude.