Efficient RAM and Control Flow in Verifiable Outsourced Computation
Download: Paper (PDF)
Date: 7 Feb 2015
Document Type: Briefing Papers
Additional Documents: Slides
Associated Event: NDSS Symposium 2015
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 either 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 builds on an elegant prior approach to RAM combined 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.