{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/87953"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/87953","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"SNARKs for C : verifying program executions succinctly and in zero knowledge","abstract":"We present a proof system that allows efficient verification of NP statements, given proofs produced by an untrusted yet computationally-bounded prover. Our system is publicly verifiable: after a trusted third-party has generated a proving key and a verification key, anyone can use the proving key to generate non-interactive proofs for adaptively-chosen NP statements, and the proofs can be verified by anyone using the verification key. Moreover, our system is statistically zero-knowledge and the generated public parameters are reusable. The NP-complete language we choose is the correct execution of programs on TinyRAM, a minimalistic (nondeterministic) random-access machine that we design. Together with TinyRAM port of gcc compiler this achieves the first practical realization of a zero-knowledge Succinct Non-interactive ARgument of Knowledge (zk-SNARK) for program executions, in the preprocessing model. This cryptographic primitive is a powerful solution for delegating N P computations, and enjoys many features not achieved by primitives implemented in prior works, most importantly, succinct verification and support for arbitrary computations. Our approach builds on recent theoretical work in the area of outsourced verified computation. We present efficiency improvements and implementations of the two main ingredients: 1. A transformation that, given as input a C program, outputs a circuit whose satisfiability encodes the correct execution of the program. We leverage nondeterminism to make the generated circuit's size merely quasilinear in the size of the computation; in particular, we efficiently handle arbitrary loops, control flow, and random-memory accesses. This is in contrast with existing \"circuit compilers\", which produce circuits of quadratic size. 2. A transformation that, given as input a linear PCP for verifying satisfiability of circuits, outputs a corresponding SNARK. Furthermore, by building on recent work about quadratic span programs, using suitable choices of finite field and FFT algorithms, we give a very efficient implementation of a zero-knowledge linear PCP: linear-time query generation and quasilinear-time prover.","abstract_html":"We present a proof system that allows efficient verification of NP statements, given proofs produced by an untrusted yet computationally-bounded prover. Our system is publicly verifiable: after a trusted third-party has generated a proving key and a verification key, anyone can use the proving key to generate non-interactive proofs for adaptively-chosen NP statements, and the proofs can be verified by anyone using the verification key. Moreover, our system is statistically zero-knowledge and the generated public parameters are reusable. The NP-complete language we choose is the correct execution of programs on TinyRAM, a minimalistic (nondeterministic) random-access machine that we design. Together with TinyRAM port of gcc compiler this achieves the first practical realization of a zero-knowledge Succinct Non-interactive ARgument of Knowledge (zk-SNARK) for program executions, in the preprocessing model. This cryptographic primitive is a powerful solution for delegating N P computations, and enjoys many features not achieved by primitives implemented in prior works, most importantly, succinct verification and support for arbitrary computations. Our approach builds on recent theoretical work in the area of outsourced verified computation. We present efficiency improvements and implementations of the two main ingredients: 1. A transformation that, given as input a C program, outputs a circuit whose satisfiability encodes the correct execution of the program. We leverage nondeterminism to make the generated circuit's size merely quasilinear in the size of the computation; in particular, we efficiently handle arbitrary loops, control flow, and random-memory accesses. This is in contrast with existing "circuit compilers", which produce circuits of quadratic size. 2. A transformation that, given as input a linear PCP for verifying satisfiability of circuits, outputs a corresponding SNARK. Furthermore, by building on recent work about quadratic span programs, using suitable choices of finite field and FFT algorithms, we give a very efficient implementation of a zero-knowledge linear PCP: linear-time query generation and quasilinear-time prover.","abstract_has_math":false,"creators":["Virza, Madars"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.","school":null,"contributors":[],"advisors":["Ronald L. Rivest and Eli Ben-Sasson."],"committee_chairs":[],"committee_members":[],"year":2014,"date_issued":"2014","date_published":"2014","updated_at":"2026-07-22T22:21:52Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/87953","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Ronald L. Rivest and Eli Ben-Sasson."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Virza, Madars"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2014-06-13T22:35:57Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2014-06-13T22:35:57Z"]},{"key":"dc:date.issued","label":"Date","values":["2014"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/87953"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis: S.M., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2014.","Cataloged from PDF version of thesis.","Includes bibliographical references (pages 69-72)."]},{"key":"dc:description.abstract","label":"Abstract","values":["We present a proof system that allows efficient verification of NP statements, given proofs produced by an untrusted yet computationally-bounded prover. Our system is publicly verifiable: after a trusted third-party has generated a proving key and a verification key, anyone can use the proving key to generate non-interactive proofs for adaptively-chosen NP statements, and the proofs can be verified by anyone using the verification key. Moreover, our system is statistically zero-knowledge and the generated public parameters are reusable. The NP-complete language we choose is the correct execution of programs on TinyRAM, a minimalistic (nondeterministic) random-access machine that we design. Together with TinyRAM port of gcc compiler this achieves the first practical realization of a zero-knowledge Succinct Non-interactive ARgument of Knowledge (zk-SNARK) for program executions, in the preprocessing model. This cryptographic primitive is a powerful solution for delegating N P computations, and enjoys many features not achieved by primitives implemented in prior works, most importantly, succinct verification and support for arbitrary computations. Our approach builds on recent theoretical work in the area of outsourced verified computation. We present efficiency improvements and implementations of the two main ingredients: 1. A transformation that, given as input a C program, outputs a circuit whose satisfiability encodes the correct execution of the program. We leverage nondeterminism to make the generated circuit's size merely quasilinear in the size of the computation; in particular, we efficiently handle arbitrary loops, control flow, and random-memory accesses. This is in contrast with existing \"circuit compilers\", which produce circuits of quadratic size. 2. A transformation that, given as input a linear PCP for verifying satisfiability of circuits, outputs a corresponding SNARK. Furthermore, by building on recent work about quadratic span programs, using suitable choices of finite field and FFT algorithms, we give a very efficient implementation of a zero-knowledge linear PCP: linear-time query generation and quasilinear-time prover."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["S.M."]},{"key":"dc:title","label":"Title","values":["SNARKs for C : verifying program executions succinctly and in zero knowledge"]}]}],"canonical_facts":{"dc:contributor.advisor":["Ronald L. Rivest and Eli Ben-Sasson."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Virza, Madars"],"dc:date.accessioned":["2014-06-13T22:35:57Z"],"dc:date.available":["2014-06-13T22:35:57Z"],"dc:date.issued":["2014"],"dc:description":["Thesis: S.M., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2014.","Cataloged from PDF version of thesis.","Includes bibliographical references (pages 69-72)."],"dc:description.abstract":["We present a proof system that allows efficient verification of NP statements, given proofs produced by an untrusted yet computationally-bounded prover. Our system is publicly verifiable: after a trusted third-party has generated a proving key and a verification key, anyone can use the proving key to generate non-interactive proofs for adaptively-chosen NP statements, and the proofs can be verified by anyone using the verification key. Moreover, our system is statistically zero-knowledge and the generated public parameters are reusable. The NP-complete language we choose is the correct execution of programs on TinyRAM, a minimalistic (nondeterministic) random-access machine that we design. Together with TinyRAM port of gcc compiler this achieves the first practical realization of a zero-knowledge Succinct Non-interactive ARgument of Knowledge (zk-SNARK) for program executions, in the preprocessing model. This cryptographic primitive is a powerful solution for delegating N P computations, and enjoys many features not achieved by primitives implemented in prior works, most importantly, succinct verification and support for arbitrary computations. Our approach builds on recent theoretical work in the area of outsourced verified computation. We present efficiency improvements and implementations of the two main ingredients: 1. A transformation that, given as input a C program, outputs a circuit whose satisfiability encodes the correct execution of the program. We leverage nondeterminism to make the generated circuit's size merely quasilinear in the size of the computation; in particular, we efficiently handle arbitrary loops, control flow, and random-memory accesses. This is in contrast with existing \"circuit compilers\", which produce circuits of quadratic size. 2. A transformation that, given as input a linear PCP for verifying satisfiability of circuits, outputs a corresponding SNARK. Furthermore, by building on recent work about quadratic span programs, using suitable choices of finite field and FFT algorithms, we give a very efficient implementation of a zero-knowledge linear PCP: linear-time query generation and quasilinear-time prover."],"dc:description.degree":["S.M."],"dc:identifier.uri":["http://hdl.handle.net/1721.1/87953"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["SNARKs for C : verifying program executions succinctly and in zero knowledge"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:21:52Z"}