Resolving the conflict between generality and plausibility in verified computation

Srinath Setty, Benjamin Braun, Victor Vu, Andrew J. Blumberg, Bryan Parno, Michael Walfish

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 8th ACM European Conference on Computer Systems, EuroSys 2013
Pages71-84
Number of pages14
DOIs
StatePublished - 2013
Event8th ACM European Conference on Computer Systems, EuroSys 2013 - Prague, Czech Republic
Duration: Apr 15 2013Apr 17 2013

Other

Other8th ACM European Conference on Computer Systems, EuroSys 2013
CountryCzech Republic
CityPrague
Period4/15/134/17/13

Fingerprint

Network protocols
Servers
Machinery
Graphics processing unit

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Cite this

Setty, S., Braun, B., Vu, V., Blumberg, A. J., Parno, B., & Walfish, M. (2013). Resolving the conflict between generality and plausibility in verified computation. In Proceedings of the 8th ACM European Conference on Computer Systems, EuroSys 2013 (pp. 71-84) https://doi.org/10.1145/2465351.2465359

Resolving the conflict between generality and plausibility in verified computation. / Setty, Srinath; Braun, Benjamin; Vu, Victor; Blumberg, Andrew J.; Parno, Bryan; Walfish, Michael.

Proceedings of the 8th ACM European Conference on Computer Systems, EuroSys 2013. 2013. p. 71-84.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Setty, S, Braun, B, Vu, V, Blumberg, AJ, Parno, B & Walfish, M 2013, Resolving the conflict between generality and plausibility in verified computation. in Proceedings of the 8th ACM European Conference on Computer Systems, EuroSys 2013. pp. 71-84, 8th ACM European Conference on Computer Systems, EuroSys 2013, Prague, Czech Republic, 4/15/13. https://doi.org/10.1145/2465351.2465359
Setty S, Braun B, Vu V, Blumberg AJ, Parno B, Walfish M. Resolving the conflict between generality and plausibility in verified computation. In Proceedings of the 8th ACM European Conference on Computer Systems, EuroSys 2013. 2013. p. 71-84 https://doi.org/10.1145/2465351.2465359
Setty, Srinath ; Braun, Benjamin ; Vu, Victor ; Blumberg, Andrew J. ; Parno, Bryan ; Walfish, Michael. / Resolving the conflict between generality and plausibility in verified computation. Proceedings of the 8th ACM European Conference on Computer Systems, EuroSys 2013. 2013. pp. 71-84
@inproceedings{66eb100bc89643e890cd23d85b51d5b4,
title = "Resolving the conflict between generality and plausibility in verified computation",
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.",
author = "Srinath Setty and Benjamin Braun and Victor Vu and Blumberg, {Andrew J.} and Bryan Parno and Michael Walfish",
year = "2013",
doi = "10.1145/2465351.2465359",
language = "English (US)",
isbn = "9781450319942",
pages = "71--84",
booktitle = "Proceedings of the 8th ACM European Conference on Computer Systems, EuroSys 2013",

}

TY - GEN

T1 - Resolving the conflict between generality and plausibility in verified computation

AU - Setty, Srinath

AU - Braun, Benjamin

AU - Vu, Victor

AU - Blumberg, Andrew J.

AU - Parno, Bryan

AU - Walfish, Michael

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84877694382&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84877694382&partnerID=8YFLogxK

U2 - 10.1145/2465351.2465359

DO - 10.1145/2465351.2465359

M3 - Conference contribution

SN - 9781450319942

SP - 71

EP - 84

BT - Proceedings of the 8th ACM European Conference on Computer Systems, EuroSys 2013

ER -