Formalizing Soundness Proofs of Linear PCP SNARKs

Formalizing Soundness Proofs of Linear PCP SNARKs

Speakers: Bolton Bailey; Andrew Miller

Conference: USENIX Security '24

YouTube: https://www.youtube.com/watch?v=BXWmFEeKbJI

Overview

This talk, presented by Bolton Bailey and co-authored with Andrew Miller, addresses a critical challenge in modern cryptography: the formal verification of soundness proofs for Succinct Non-interactive ARguments of Knowledge (SNARKs). Specifically, the work focuses on Linear Probabilistically Checkable Proof (PCP) SNARKs, a class of cryptographic primitives vital for applications requiring compact and verifiable computation, such as blockchain technologies. The core contribution is the successful formalization and computer-aided verification of the soundness property for six prominent linear PCP SNARKs, including the widely used Groth16.

The significance of this research stems from the inherent complexity and subtlety of SNARK soundness proofs. Unlike other cryptographic properties, soundness is notoriously difficult to prove manually, often leading to hidden errors—a problem highlighted by past vulnerabilities in implementations like the Zcash cryptocurrency. By employing the Lean theorem prover, a powerful formal verification tool, Bailey and Miller aim to provide a higher degree of assurance in the security claims of these complex cryptographic systems. This work not only enhances the trustworthiness of foundational SNARK protocols but also demonstrates a robust methodology for applying formal methods to the challenging domain of cryptographic proof systems, bridging the gap between theoretical mathematical proofs and verifiable computational guarantees.

Background

▶ Watch: Introduction to SNARKs and their key features (0:00)

SNARKs are cryptographic primitives that enable a prover to convince a verifier that a certain computation was performed correctly, without revealing the prover's private inputs and with a proof of remarkably small size. They are defined by three critical properties:

1. Completeness: An honest prover, given valid inputs, can always generate a proof that an honest verifier will accept.
2. Zero-Knowledge: The proof reveals nothing about the prover's private inputs beyond the fact that the computation is valid.
3. Soundness: An adversarial prover cannot generate a false proof that an honest verifier will accept. This is the property that this research primarily addresses.

Soundness is often considered the most challenging of these properties to prove. Its complexity arises from the intricate mathematical justifications involved, the vast space of potential adversaries, and the composition of various cryptographic components. Historical incidents, such as errors discovered in the SNARK used by Zcash, underscore the practical importance of rigorously proving soundness. Traditional methods like fuzzing are ineffective for this property due to the infinite space of possible adversarial strategies.

The SNARKs examined in this work are Linear PCP SNARKs, which operate within the Algebraic Group Model (AGM). In this model, proof messages are constructed from elements of a finite field, but these elements are then encrypted into elliptic curve groups. Specifically, three types of groups are typically involved: G1, G2, and a target group GT. The allowed operations on these encrypted elements are restricted:

• Standard elliptic curve operations: Addition of elements within the same group and scalar multiplication by constants.
• Pairing operations: A crucial bilinear map, denoted as e(G1_element, G2_element), which takes an element from G1 and an element from G2, multiplies them in a cryptographic sense, and produces a result in the target group GT. The security of the scheme critically depends on the assumption that no other operations are possible on these encrypted field elements.

The protocol for a linear PCP SNARK unfolds in several stages:

1. Trusted Setup: A trusted third party generates a Structured Reference String (SRS). This involves sampling random field elements and encrypting them into the elliptic curve groups. Once generated, the SRS is distributed to both the prover and the verifier, and the trusted third party is no longer needed (ideally, their secret parameters are securely discarded).
2. Prover's Role: The prover, possessing a program represented as an arithmetic circuit and potentially private inputs, performs linear combinations of the SRS elements. These combinations are used to construct the proof, Pi.
3. Verifier's Role: The verifier receives the proof Pi from the prover. They then perform their own set of elliptic curve group operations and pairing operations using Pi and the SRS. The verifier's final step is to check for specific equalities between computed values. If all checks pass, the verifier accepts the proof as valid.

A fundamental insight underpinning this formalization effort is that throughout the entire protocol, all encrypted values—whether passed between parties or computed internally—can be represented as multivariable polynomials of the initial random field elements sampled during the trusted setup. Consequently, the statement of the soundness property for these SNARKs can be reformulated as a statement asserting that "some multivariable polynomial identities imply some other multivariable polynomial identity." This transformation is key because problems of this nature can be systematically addressed using Gröbner basis methods, providing a pathway for automated, formal verification.

Key Findings

▶ Watch: Linear PCP SNARK structure and cryptographic model (3:20)

The central achievement of this research is the successful formalization and computer-aided verification of the soundness property for a significant set of linear PCP SNARKs. Utilizing the Lean theorem prover, the project formally proved the soundness of six distinct SNARK constructions. This includes:

• Early Literature SNARKs: The work covered foundational schemes such as the GGPR SNARK and the Pinocchio SNARK, which were instrumental in the early development of SNARK technology.
• Groth16 Variants: A major focus was on the Groth16 SNARK, one of the most widely adopted and efficient SNARK constructions currently in use. The team verified several variants, including a Type 3 version that utilizes specific Type 3 pairings with different restrictions on interactions between the G1 and G2 elliptic curves.

A notable finding during the verification process was the differential effort required for different SNARKs. While the initial formalization of Groth16 proved to be the most challenging, demanding "quite a bit of casework" and taking considerably longer to complete the computer-checked proof, subsequent variants became "relatively easy" to verify once the core framework was established. This suggests that the methodology developed is robust and adaptable, allowing for efficient extension to similar SNARK designs once a foundational proof is in place. The successful application of Gröbner basis methods within a formal verification environment for these complex cryptographic primitives represents a significant step forward in ensuring their security guarantees.

Technical Deep Dive

▶ Watch: Step-by-step linear PCP SNARK protocol overview (4:30)

The technical core of this work lies in translating the cryptographic soundness problem into a formal system amenable to automated proof, specifically using the Lean theorem prover and leveraging Gröbner basis methods. The overall strategy involves representing the SNARK protocol's operations as polynomial equations and then using Lean to demonstrate that the verifier's acceptance conditions (polynomial identities) necessarily imply the prover's adherence to the protocol's mathematical rules (another polynomial identity).

Let's illustrate this with a simplified "toy SNARK" example, as presented in the talk, to understand the formalization process:

Consider a hypothetical SNARK where the Structured Reference String (SRS) consists of four random field elements, alpha, beta, gamma, delta, encrypted into the elliptic curve groups.

• The prover is supposed to compute and return an element P_pi in G1, which is a*alpha + b*beta for some secret a and b.
• The verifier computes Q_check in G2, which is c*alpha + d*beta.
• The verifier then performs a pairing check: e(P_pi, Q_check) == e(e*alpha, beta). This implies e(a*alpha + b*beta, c*alpha + d*beta) == e(e*alpha, beta).
• The goal for soundness is to prove that if this check passes, then it must be the case that a*d = e OR b*c = e.

The steps within the Lean theorem prover proceed as follows:

1. Loading Assumptions and Goal: The first step is to encode the verifier's check as a polynomial identity within Lean. Using the bilinearity of the pairing e, the check e(a*alpha + b*beta, c*alpha + d*beta) == e(e*alpha, beta) can be expanded.

• The left-hand side (LHS) expands to a*c*(alpha*alpha) + a*d*(alpha*beta) + b*c*(beta*alpha) + b*d*(beta*beta).
• The right-hand side (RHS) is e*(alpha*beta).
• Since alpha*beta is equivalent to beta*alpha, the LHS simplifies to a*c*alpha^2 + (a*d + b*c)alphabeta + b*d*beta^2.
• The initial polynomial equation to load into Lean is thus:

a*c*alpha^2 + (a*d + b*c)alphabeta + b*d*beta^2 == e*alpha*beta

1. Normalization and Coefficient Comparison: For two polynomials to be equal for all possible random values of alpha and beta (which is implied by the verifier's check passing), their coefficients for each monomial must be identical. This is a crucial step in Gröbner basis methods.

• Comparing coefficients for alpha^2: a*c = 0
• Comparing coefficients for alpha*beta: a*d + b*c = e
• Comparing coefficients for beta^2: b*d = 0

These three equations form the set of hypotheses derived from the verifier's check. The goal remains to prove that these hypotheses imply a*d = e OR b*c = e.

1. Recursive Casework and Simplification: This is where the power of the theorem prover and Gröbner basis techniques become evident.

• From the equation a*c = 0, Lean can deduce that either a = 0 or c = 0. This splits the proof into two distinct cases.

• Case 1: Assume a = 0
• Substitute a = 0 into the hypotheses:
• 0*c = 0 (trivial)
• 0*d + b*c = e which simplifies to b*c = e
• b*d = 0
• In this case, we have directly derived b*c = e from the hypotheses. Since our goal is a*d = e OR b*c = e, having b*c = e satisfies the goal for this case.

• Case 2: Assume c = 0
• Substitute c = 0 into the hypotheses:
• a*0 = 0 (trivial)
• a*d + b*0 = e which simplifies to a*d = e
• b*d = 0
• Similarly, in this case, we have directly derived a*d = e from the hypotheses. This also satisfies the goal for this case.

Since both possible cases (a=0 or c=0) lead to the desired conclusion (a*d=e OR b*c=e), the theorem is formally proven.

The actual SNARKs are more complex than this toy example. They involve Laurent polynomials, which permit negative exponents (e.g., alpha^-1), and formal sums of terms. However, the underlying principle of translating cryptographic operations into polynomial identities, comparing coefficients, and performing systematic casework remains the same. The use of Gröbner basis methods provides the algorithmic framework to manage these complex polynomial systems within the theorem prover.

A significant challenge highlighted by the speaker was the "fragility" of the underlying proof system itself. The Lean theorem prover is an actively developed project, with a major transition from Lean 3 to Lean 4 occurring during the project's timeline. This required continuous adaptation and maintenance of the formalized proofs, underscoring the dynamic nature of working with cutting-edge formal verification tools. Despite these hurdles, the successful verification of Groth16 and other SNARKs demonstrates the immense potential of this approach for cryptographic assurance.

Demo / Proof of Concept

▶ Watch: Soundness as polynomial identities; Groebner basis methods (6:00)

While the talk did not feature a live software demonstration in the traditional sense of running an exploit or a cryptographic protocol, the core "proof of concept" was the successful formalization and computer-aided verification of the SNARK soundness proofs themselves. The speaker effectively demonstrated this by walking through the detailed logical steps within the Lean theorem prover for the simplified "toy SNARK" example.

This walkthrough served as a pedagogical demonstration of how the Lean environment is used to:

1. Encode cryptographic assumptions: Representing the verifier's equality checks as multivariable polynomial identities.
2. Apply algebraic transformations: Showing how Lean applies properties like the distributive law and the bilinearity of pairings to expand and normalize these polynomial expressions.
3. Perform coefficient comparison: Illustrating how the theorem prover equates coefficients of like terms across polynomial identities to derive a set of simpler, foundational equations.
4. Execute systematic casework: Demonstrating how Lean recursively splits the proof into disjunctive cases (e.g., a=0 or c=0) and simplifies the problem within each case until the desired soundness condition is met.

This step-by-step exposition, although presented via slides and logical derivation rather than interactive code execution, vividly conveyed the rigor and automation afforded by the formal verification process. It underscored that the "proof of concept" is not merely a theoretical claim but a meticulously constructed and machine-checked logical artifact, confirming the soundness of the SNARKs under the specified cryptographic model.

Defensive Implications

▶ Watch: Walkthrough of a basic SNARK example begins (7:00)

The formalization of SNARK soundness proofs has profound implications for defenders, particularly those involved in designing, implementing, or auditing cryptographic systems that rely on SNARKs.

1. Enhanced Assurance for Critical Primitives: SNARKs are increasingly becoming foundational components for privacy-preserving computations, verifiable computation in blockchains, and other sensitive applications. Given their complexity and the history of subtle errors in manual proofs (e.g., Zcash), formal verification provides an unprecedented level of assurance in their security guarantees. Defenders can have higher confidence that the SNARKs verified by this methodology are mathematically sound against adversarial provers.

1. Robust Methodology for Future SNARKs: This work establishes a clear and robust methodology for formally proving the soundness of linear PCP SNARKs within the Algebraic Group Model. This framework, leveraging Lean and Gröbner basis methods, can be adapted and extended to new SNARK constructions or variants. For security architects and researchers, this offers a powerful toolset to proactively verify the integrity of novel SNARK designs before deployment.

1. Identification of Implicit Assumptions: The process of formalization forces explicit articulation of all assumptions. This can help uncover implicit assumptions in manual proofs that might otherwise go unnoticed. For instance, the reliance on the Algebraic Group Model, where adversaries are restricted to algebraic operations, is made explicit, guiding implementers and auditors on the exact security model under which the SNARK is proven sound.

1. Mitigation of Human Error: Manual cryptographic proofs, especially for complex systems like SNARKs, are highly susceptible to human error. Formal verification eliminates this risk by requiring a machine-checkable proof. This is particularly valuable for soundness, where the adversary space is vast and difficult to reason about exhaustively without computational assistance.

1. Importance of Trusted Setup: While the focus is on soundness, the work implicitly highlights the critical role of the trusted setup in linear PCP SNARKs. The security of the entire scheme hinges on the initial random field elements being sampled correctly and the secret parameters being securely discarded. Defenders must therefore pay rigorous attention to the security and auditability of trusted setup ceremonies.

1. Guidance for Auditing and Review: For auditors and security researchers evaluating SNARK-based systems, this work provides a deeper understanding of the underlying mathematical structure and the precise conditions that constitute soundness. It equips them with the knowledge to scrutinize existing SNARK implementations and their proofs more effectively, even if they are not directly using formal verification tools themselves.

Key Takeaways

• SNARK Soundness is Critical and Complex: The soundness property of SNARKs, ensuring no adversarial prover can forge a valid proof, is exceptionally difficult to prove manually due to intricate mathematics, a vast adversary space, and past errors in real-world deployments.
• Formal Verification Provides Robust Assurance: Using theorem provers like Lean offers a powerful, computer-aided approach to formally verify SNARK soundness, significantly increasing confidence in their cryptographic security guarantees.
• Polynomial Identities are Key: The core insight is that SNARK operations and soundness conditions can be translated into statements about multivariable polynomial identities, allowing algebraic methods to be applied.
• Gröbner Basis Methods are Effective: Mathematical tools like Gröbner basis methods are well-suited for solving systems of polynomial equations, providing the algorithmic backbone for formalizing SNARK soundness proofs.
• Six Linear PCP SNARKs Verified: The project successfully formalized and verified the soundness of six prominent linear PCP SNARKs, including foundational schemes like GGPR and Pinocchio, and crucial variants of Groth16 (e.g., Type 3).
• Challenges and Future of Formal Methods: While active development of tools like Lean (e.g., Lean 3 to Lean 4 transition) presents challenges, the success of this work demonstrates the immense potential and growing maturity of formal verification for securing complex cryptographic primitives.

About the Speaker(s)

Bolton Bailey was the primary presenter of this work, detailing the process and findings of formalizing soundness proofs for linear PCP SNARKs using the Lean theorem prover. His presentation highlighted the technical intricacies and the practical challenges encountered during the project.

Andrew Miller is credited as a co-author of the work. While not explicitly stated in the transcript, Andrew Miller is a known figure in the blockchain and cryptocurrency space, often involved in research related to cryptographic protocols and their security.