Paper 2013/507
SNARKs for C: Verifying Program Executions Succinctly and in Zero Knowledge
Eli BenSasson, Alessandro Chiesa, Daniel Genkin, Eran Tromer, and Madars Virza
Abstract
An argument system for NP is a proof system that allows efficient verification of NP statements, given proofs produced by an untrusted yet computationallybounded prover. Such a system is noninteractive and publiclyverifiable if, after a trusted party publishes a proving key and a verification key, anyone can use the proving key to generate noninteractive proofs for adaptivelychosen NP statements, and proofs can be verified by anyone by using the verification key. We present an implementation of a publiclyverifiable noninteractive argument system for NP. The system, moreover, is a zeroknowledge proofofknowledge. It directly proves correct executions of programs on TinyRAM, a randomaccess machine tailored for efficient verification of nondeterministic computations. Given a program $P$ and time bound T, the system allows for proving correct execution of $P$, on any input $x$, for up to T steps, after a onetime setup requiring $\tilde{O}(P T)$ cryptographic operations. An honest prover requires $\tilde{O}(P \cdot T)$ cryptographic operations to generate such a proof, while proof verification can be performed with only $O(x)$ cryptographic operations. This system can be used to prove the correct execution of C programs, using our TinyRAM port of the GCC compiler. This yields a zeroknowledge Succinct Noninteractive ARgument of Knowledge (zkSNARK) for program executions in the preprocessing model  a powerful solution for delegating NP computations, with several features not achieved by previouslyimplemented primitives. Our approach builds on recent theoretical progress in the area. We present efficiency improvements and implementations of two main ingredients: * Given a C program, we produce a circuit whose satisfiability encodes the correctness of execution of the program. Leveraging nondeterminism, the generated circuit's size is merely quasilinear in the size of the computation. In particular, we efficiently handle arbitrary and datadependent loops, control flow, and memory accesses. This is in contrast with existing ``circuit generators'', which in the general case produce circuits of quadratic size. * Given a linear PCP for verifying satisfiability of circuits, we produce a corresponding SNARK. We construct such a linear PCP (which, moreover, is zeroknowledge and very efficient) by building on and improving on recent work on quadratic arithmetic programs.
Note: Revised for clarity, especially Section 3 and Appendix E.
Metadata
 Available format(s)
 Category
 Cryptographic protocols
 Publication info
 A major revision of an IACR publication in CRYPTO 2013
 Keywords
 computationallysound proofssuccinct argumentszeroknowledgedelegation of computation
 Contact author(s)
 tromer @ cs tau ac il
 History
 20131007: revised
 20130817: received
 See all versions
 Short URL
 https://ia.cr/2013/507
 License

CC BY
BibTeX
@misc{cryptoeprint:2013/507, author = {Eli BenSasson and Alessandro Chiesa and Daniel Genkin and Eran Tromer and Madars Virza}, title = {{SNARKs} for C: Verifying Program Executions Succinctly and in Zero Knowledge}, howpublished = {Cryptology ePrint Archive, Paper 2013/507}, year = {2013}, note = {\url{https://eprint.iacr.org/2013/507}}, url = {https://eprint.iacr.org/2013/507} }