Efficient zkSNARKs Without Trusted Setup: Spartan Overview
Spartan is a family of zkSNARKs that offer efficient and general-purpose zero-knowledge proofs without the need for a trusted setup. These zkSNARKs allow for proving the correctness of cloud services, ensuring transaction privacy, and more, with applications in cloud computing and blockchain technology. Unlike previous approaches, Spartan achieves sub-linear verification times and supports arbitrary circuits without compromising succinctness.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Spartan Efficient and general-purpose zkSNARKs without trusted setup Srinath Setty Microsoft Research https://github.com/Microsoft/Spartan
What is a zkSNARK? Argument of Knowledge Prove the knowledge of a secret witness w such that C(x,w) = 1 Prover Verifier Zero-knowledge hides w Applications in practice: Proving the correct operation of cloud services Offload blockchain processing to the cloud Transaction privacy Non-interactive Succinct | | is sub-linear in |C| Verifier runs in time sub-linear in |C|
Many approaches to build zkSNARKs PCPs + Merkle trees [Kilian92, Micali94] A breakthrough result: [GGPR13] building on [IKO07, Groth10, Lipmaa12] Supports arbitrary circuits Near-optimal asymptotics with good constants Prover: O (|C| log |C|) Proof size: O (1) Verifier: O (|x| + |y|) Requires a per-circuit trusted setup where the trapdoor used must be kept secret
Recent focus: zkSNARKs without trusted setup Several schemes: Ligero, Hyrax, STARK, Bulletproofs, Aurora Some of these achieve better performance than GGPR-derived schemes Prior works can support arbitrary circuits or a succinct verifier, not both Succinct verifier Arbitrary circuits Aurora Hyrax layered, parallel circuits Spartan (this work) Ligero A sequence of repeated sub-circuits STARK Bulletproofs
Challenges with achieving succinct verification 1. Arbitrary circuits have no structure 2. The verifier must know what statement is being proven! (1) + (2) Verification must be at least O(|C|) The Spartan verifier preprocesses circuits withoutsecret trapdoors The verifier retains a commitment to circuit computation commitment Preprocessing incurs O(|C|) costs, but is amortized The amortization is similar to that of [GGPR13]
Spartan: A family of zkSNARKs without trusted setup Supports arbitrary circuits, specifically R1CS A new recipe for constructing zkSNARKs The sum-check protocol Polynomial commitments Computation commitments Four new zkSNARKs (using different polynomial commitments) Verification and proof sizes: O(log2n) to O( ?) Prover: O(n) to O(n log n) A Rust implementation of a member of the family (~8,000 SLOC) Fastest prover. Fastest verifier; shortest proof sizes (except for Bulletproofs) for n 220 constraints
Spartan unifies different strands of theory (Short PCPs) With [Kilian92, Micali94]: Concretely inefficient Requires uniform circuits for sub-linear verification Short PCPs of [BFLS91] Merkle trees zkSNARKs With Spartan: Short PCPs of [BFLS91] Polynomial commitments Concretely efficient Supports arbitrary circuits zkSNARKs Computation commitments
Spartan unifies different strands of theory (MIPs) With [BC12]: Concretely inefficient Designated verifier FHE-based compiler MIPs zkSNARKs of [BTVW14] With Spartan: MIPs Polynomial commitments of [BTVW14] Concretely efficient Publicly verifiable zkSNARKs Computation commitments
Spartan unifies different strands of theory (IPs) With [Zhang et al. 17, Wahby et al. 2018]: Doubly- efficient IPs of GKR08 Low-depth circuits Uniform circuits Polynomial commitments zkSNARKs With Spartan: Doubly- efficient IPs of GKR08 Polynomial commitments Arbitrary circuits (no depth or structure limitations) zkSNARKs Computation commitments
Rest of this talk Overview of Spartan Experimental results
Spartans base: The sum-check protocol[LFKN90] A proof system for proving statements of the form i.e., sum-check instances (G is a multivariate polynomial over a finite field): ? = ?1, ,?? {0,1}?(?1, ,??) The proof system does not require a trusted setup It can be made zero-knowledge and non-interactive with existing compilers What is missing? We need an efficient reduction from R1CS statements to sum-check instances The proof system is not succinct (both proof sizes and verification times) The verifier must evaluate G at a random point in its domain (?1, ,??)
Rank-1 constraint satisfiability (R1CS) Given three public matrices A, B, C over a finite field ?, does there exist a secret witness z such that: ?? ?? = ?? ? ( is entry-wise product) An NP-complete problem that generalizes arithmetic circuit satisfiability Implicit in [GGPR13], but made explicit by subsequent works There exist many compiler toolchains from high-level programs (C, Java, Rust, etc.) of interest to R1CS since the early 2010s Ginger, Pinocchio, Pantry, Buffet, Geppetto, xJsnark, etc.
Encoding R1CS instances as sum-check instances Given three public matrices A, B, C over a finite field ?, does there exist a secret witness z such that: ?? ?? = ?? ? View A, B, C, and z as functions (s = logm and m is matrix dimension) A, B, C: {0,1}s x {0,1}s ? and z: {0,1}s ? We prove: ?? ?? = ?? iff (except small soundness error): eq(x, ) = 1 if x = , 0 otherwise 0 = ? {0,1}??? ?, ?(?) ? ?,? ? ? ? 0,1? ? ?,? ?(?) ? 0,1? ? ?,? ?(?) ? ? = ? {0,1}? ?(x, ?) = A(x, ?) for ?,? {0,1}?
Recap: What is missing with the sum-check protocol? We need a reduction from R1CS statements to sum-check instances 0 = ? {0,1}??? ?, ?(?) ? ?,? ? ? ? 0,1? ? ?,? ?(?) ? 0,1? ? ?,? ?(?) ? ? = ? {0,1}? (See the paper for how to apply the sum-check protocol on double sums.) The protocol is not succinct (both proof sizes and verification times). The verifier must evaluate four multilinear polynomials: ? ?? The first one depends on the prover s witness ? ??,??, ? ??,??, ? ??,?? The last three depend only on the statement
Evaluating ? ?? succinctly (for the verifier) Idea: Employ an extractable polynomial commitment scheme (we assume background on polynomial commitments) Prover Verifier: Commit(pp, ?) (before the sum-check protocol) [Run the sum-check protocol] Prover Verifier: ? ??, (a proof of correct evaluation) Verifier: Verify using the commitment and use the supplied ? ?? to evaluate G There are many polynomial commitments without trusted setup (see the paper) | | and the cost to verify are succinct (i.e., sub-linear in |z|)
Evaluating ? ??,??, ? ??,??,? ??,?? succinctly Computation commitment Idea: Employ a polynomial commitment scheme In a preprocessing phase, the verifier computes: ?????? ??, ? ,?????? ??, ? ,??????(??, ?) Prover Verifier: Commit(pp, ?) (before the sum-check protocol) [Run the sum-check protocol] Prover Verifier: ? ??,?? ? ??,??, ? ??,??, ? ??,?? , ??,??,?? Verifier: Verify proofs against commitments and evaluate G using the supplied evaluations
This almost works, but ?, ?, ? are sparse polynomials. That is, A, B, C are sparse matrices In practice, the number of non-zero entries is n = O(m) But, the total number of entries is O(m2) 5 2 0 0 0 1 0 0 0 Existing commitment schemes incur O(m2) costs (for creating commitments and producing evaluation proofs) Prover is quadratic in the statement size (Theoretically efficient, but not in practice)
Our solution: SPARK PolyCommit for multilinear polynomials PolyCommit for sparse multilinear polynomials SPARK compiler (1) Commitments: commit to dense representations 0 8 0 0 5 0 0 0 0 9 0 0 col val row 0 1 1 1 0 2 5 8 9 Each polynomial size = O(n), #non-zero entries (2) Polynomial evaluation (see the paper for details): An O(n)-sized uniform circuit (employs offline memory checking techniques) A tailored zkSNARK where the verifier incurs sub-linear costs
Spartans techniques in a nutshell R1CS instance An argument of knowledge Existing compilers Sum-check instance Theorem 5.1 NIZKs Theorem 4.1 PolyCommit for multilinear polynomials PolyCommit for sparse multilinear polynomials SPARK compiler Computation commitments zkSNARKs for R1CS
Rest of this talk Overview of Spartan Experimental results
Implementation Implement SpartanDL is secure under DLOG in the RO model 8,000 lines of Rust, with many optimizations (see the paper) Open source: https://github.com/Microsoft/Spartan
Experimental evaluation Metrics:(1) prover s time, (2) verifier s time, and (3) proof sizes Testbed: A Microsoft Surface Laptop 3, with Intel i7 and 16 GB RAM Baselines: Groth16, the state-of-the-art zkSNARK with trusted setup based on [GGPR13] Ligero Hyrax Aurora Fractal (achieves sub-linear verification using computation commitments) Incur linear-time costs for arbitrary circuits
Provers costs (one CPU core) 10000 SpartanNIZK SpartanSNARK Groth16 Ligero Hyrax Aurora Fractal 1000 Prover s time (seconds) 100 10 1 0.1 15 16 17 18 19 20 log(number of constraints) SpartanSNARK is 36x faster than Fractal and 2x faster than Groth16 SpartanNIZK is 24 152x faster than Ligero, Hyrax, and Aurora
Proof sizes 100000 SpartanNIZK SpartanSNARK Hyrax Ligero Aurora Fractal 10000 Proof sizes (KB) 1000 100 10 1 15 16 17 18 19 20 log(number of constraints) Groth16 (not depicted) produces shortest proofs (128 bytes) SpartanSNARK s proofs are 23x smaller than Fractal SpartanNIZK offers 1.2 416x smaller proofs than Ligero, Hyrax, and Aurora
Verifiers cost (one CPU core) 1000000 SpartanNIZK SpartanSNARK Hyrax Fractal Ligero Aurora 100000 Verifier s time (ms) 10000 1000 100 10 1 15 16 17 18 19 20 log(number of constraints) Groth16 (not depicted) features the fastest verifier (~3ms) SpartanSNARK is 3.6x faster than Fractal SpartanNIZK offers 22 363x faster than Ligero, Hyrax, and Aurora SpartanSNARK beats SpartanNIZK at roughly 217 constraints
Summary Spartan is a new family of zkSNARKs without trusted setup First to achieve sub-linear verification costs for arbitrary circuits Features schemes with a linear-time prover Introduces new techniques: Computation commitments to preprocess NP statements without trapdoors SPARK compiler to transform polynomial commitments to handle sparse multilinear polynomials efficiently A compact encoding of R1CS instances as sum-check instances Concrete implementation in Rust and evaluation up to 220 constraints. Among transparent schemes: Fastest prover and verifier Shortest proof sizes (except for Bulletproofs)
