ZKProof Verified Verifiers

What’s “Verified Verifiers”?

This working group will formally establish the validity of a zero-knowledge proof, by ensuring correctness of the cryptographic software that runs the verification step of the ZKP protocol, by use of formal verification of that software. ☺

Objectives

Select and endorse a specific verifier for a chosen Zero-Knowledge Proof (ZKP) scheme.
Rigorously define all properties of the chosen verifier at the highest level of detail.
Conduct a comprehensive formal verification process on an implementation of the scheme.

The ZKProof.org Steering Committee is focused on:

Producing concrete formal verification outcomes and artifacts
Establishing a replicable process for formal verification that can serve as a reference for future ZKP schemes

This Working Group aims to deliver results within 12 months of kick-off, setting a new standard for trust and reliability in ZKP implementations.

Presentations

ZKProof & EF Workshop
Formal Verification of ZKP Zurich, October 21st 2024

This focused workshop is a collaborative effort between ZKProof and the Ethereum Foundation’s FV-zkEVM team. It aims to advance the practice of formal verification within zero-knowledge-proof systems. Attendees will engage in deep technical discussions, participate in collaborative problem-solving sessions, and contribute to strategic roadmaps for future research and implementation.

Sessions Overview:

Vilhelm’s presentation on zkWasm verification methodology, which provided interesting lessons for zkEVM work.
Julian’s talk and demo about his work with Denis on doing verification of cryptography using EasyCrypt, useful for the Groth16 verified verifier.
then Marco’s CLAP framework presentation, showing how simple optimizations beat hand-crafted results while keeping assurances.
and finally the roadmap discussions for both the zkEVM verification and Verified Verifier efforts.

Key Themes that emerged:

Start verification during design phase – you get cost/time savings when formal methods inform development rather than validate it.
Separate circuit construction from optimization and the idea of witness generators as specifications which allows cleaner composition.
Verification approaches by layers – the low/middle/high spec pattern works well and gives reusable FV work.
Testing alone isn’t sufficient for critical systems – formal methods caught critical bugs that fuzzing missed.
Documentation of optimization rationale is crucial – much time spent reverse-engineering design decisions.
Build maintainable verification frameworks – MathLib’s success shows a model for the way forward.
Industry needs different guarantees than academia – clear caveats about what’s verified.
Current learning resources are inadequate – need better onboarding for engineers.

Open Questions:

How do we bridge the gap between cryptographic papers and formal verification?
What’s the right balance between tool consolidation and specialized solutions?
How do we maintain verification as VMs evolve?

Next Steps:

Random oracle model implementation in Lean (target: Q1 2025)
Circuit verification tooling improvements
Better documentation of optimization strategies
Preparation for ZKProof 7 in Sofia (March 2025) – with more work on Verified Verifier
Initial zkEVM verification frameworks and specifications

Kick-off session at ZKProof 6 in Berlin, May 2024

The Ouroboros of ZK: Why Verifying the Verifier Opens Up Longer-Term ZK Innovation.

Speaker: Ben Livshits (Matter Labs)

The world of zero-knowledge proofs is rapidly evolving. We increasingly have rollups and other ZK-based solutions coming to the forefront of blockchain scaling efforts. As these technologies become more widespread, we are faced with new challenges in ensuring their reliability, security, and efficiency. At ZKProof 6, we were fortunate to hear from Ben Livshits of Matter Labs (zkSync) on how we can improve the reliability of ZK systems.The primary goal of ZK technology is to move away from wasteful multi-execution on Layer 1 blockchains, in favour of the production of proofs of such execution, which is more efficient. This shift promises to make blockchain transactions more affordable and scalable. However, the journey doesn’t end with efficiency gains. There are significant reliability and correctness problems that also need addressing.

The State of Zero-Knowledge Systems in Practice

ZK rollups are coming into their prime. We have multiple competing companies that are developing complex software systems to achieve rollups and supporting functionalities. At present, the industry is still in a centralized deployment phase, but decentralization of block generation is on the horizon. This means we will slowly move towards decentralized proving, including prover pools and markets. This will allow proof generation to be done ubiquitously, by people or groups of people with the available resources.

ZK is Not Just Math

ZK systems in the real world are far more complex than just math. They are usually implemented as part of complex distributed systems with availability and scaling concerns. The specialised nature of ZK technology brings in software complexity, including difficult-to-interpret code. There is thus potential for bugs and vulnerabilities, as evidenced by recent audits. Some recent examples include a vulnerability discovered in a Linea audit in 2023, and a bug in recursive proof verification reported by Aztec in 2021.In his talk, Ben presented findings from his recent study of 141 bugs in deployed or pre-deployed ZK systems. Many issues stemmed from standard software development problems rather than flaws in the underlying mathematical algorithms. Some of these bugs were also found in production verifiers! This demonstrates that verifier vulnerabilities are not merely theoretical concerns but real issues that have been encountered in the wild.

The Verifier: The Last Line of Defence

In a decentralized proving ecosystem, the verifier is the critical safeguard against potential malicious or faulty provers. Even if proofs are “found on the street,” a robust verifier would prevent any compromise of the system’s integrity. An examination of current ZK rollup projects like zkSync Era, Polygon Hermez, Taiko, and Linea reveals that verifier code typically ranges from 1,000 to 2,000 lines. This is small compared to the prover’s codebase, but at the same time it represents the most mission-critical portion of the system!Performing formal verification on the implementation of the verifier is a tractable problem to solve. The verifier is relatively small, self-contained, and requires sophisticated reasoning techniques. Moreover, advancements in cloud computing power make tackling these complex verification tasks more feasible than ever before. A rigorous verification of the verifier would ensure they live up to their security guarantees and can handle provers of all flavors.

Approaches to Verifier Verification

In the talk, Ben outlined several approaches to verifying the ZK properties of completeness, soundness, and proof of knowledge. The formal verification tools in use include Lean, KEVM, and Easycrypt.Lean and KEVM, however, may not be sufficient for the probabilistic reasoning required for formal verification of cryptographic systems. Instead, the team at zkSync has focused on using Easycrypt, a tool that provides built-in support for probabilistic logic and reasoning. Their approach involves:- Code extraction: Converting existing Yul (the in-line assembly language for Solidity and Ethereum) code to Easycrypt statements.- Mathematical specification: Defining abstract representations of verification functions.- Equivalence proofs: Demonstrating that low-level implementations match high-level specifications.- Security derivation: Proving necessary security properties for the high-level implementation.The talk went briefly over examples of how this process works, showing how Yul code for Lagrange polynomial evaluation can be translated into Easycrypt and then reasoned about mathematically.

Challenges and Considerations

This approach is not without challenges:- We need to model Yul memory states and gas usage.- Datatype issues would need to be dealt with.- Balancing the complexity of the verification process with its scope.It is important to note that this formal verification is not intended for every smart contract but rather for the specialized task of verifying ZK verifiers.

The Broader Context: ZK and Formal Methods

The talk placed the verifier verification effort in the context of broader attempts to bring formal methods to the ZK space. While much work has focused on circuit verification and end-to-end protocol correctness, Ben argued that focusing on verifying the verifier represents a critical aspect of ZK security. The talk concluded with a call to arms for both the ZK and formal verification communities — ZK practitioners should embrace formal verification techniques to enhance the security and reliability of their systems, and formal verification experts should seek out challenging problems in the ZK space.

Future Directions and Open Questions

The talk sparked several important questions and areas for future research:- How should we approach verifiers for different proof systems with varying levels of complexity (e.g., Groth16 vs. PLONK-based systems)?- Can we develop standardized, reusable pieces of verified code for common ZK operations?- What’s the best way to structure lemmas and guide the proof process? Are there ways to streamline the process of generating provable statements from code?

Conclusion: The Importance of Verifier Verification

As the ZK space continues to evolve rapidly, ensuring the integrity of verifiers becomes increasingly critical. While ZK systems promise significant advantages in terms of privacy and scalability, their real-world implementations are not immune to bugs and vulnerabilities. By focusing on formal verification of verifiers, we can:- Enhance the security of ZK systems.- Increase confidence in their correctness.- Potentially catch and prevent serious vulnerabilities before they impact live systems.The challenges are significant, but the potential rewards are enormous. As Ben put it, verifiers are “as mission-critical as it gets” in the ZK space. By bringing together expertise from both the ZK and formal verification communities, we have the opportunity to build more robust, reliable, and trustworthy ZK systems.Investing in verifier verification now is not just about solving today’s problems; it’s about preparing for the challenges of tomorrow and ensuring that ZK technology can live up to its transformative potential. The road ahead may be long, but the work of verifying the verifier represents a critical step in the maturation of ZK technology. As we continue to push the boundaries of what’s possible with ZK proofs, It will continue to be fundamentally important to get the basics right. After all, in the world of cryptography and blockchain, trust is built on verifiable foundations.

Show More

Formal Verification of Arithmetic Circuits

Speaker: Marcin Kostrzewa, Reilabs

In his talk at ZKProof 6, Marcin Kostrzewa from Reilabs spoke about formal verification of arithmetic circuits, and the work done by the team at Reilabs to do this practically in the real world.
The vulnerabilities that arise in ZK protocols fall into five main categories:
– Underconstrained circuits
– Non-deterministic circuits
– Arithmetic issues (overflows, underflows, mismatching bit lengths)
– Assigned but not constrained variables
– Finite field arithmetic complexities
A reason for these issues is that unlike traditional programming, ZK circuit designers must work with non-linear polynomial equations and finite field arithmetic, which can be counterintuitive for developers accustomed to standard computer science paradigms.

The Power of Non-Determinism

Marcin pointed out that non-determinism is actually a powerful design principle in circuit writing. The ability to “produce values out of thin air” and then assert their correctness allows for elegant solutions to complex problems. He illustrated this with a common example: proving that a value is less than eight by decomposing it into a three-bit binary representation. However, this approach is not without pitfalls. Improper implementation, such as using the full bit width of the finite field (that is, not constraining individual bits to be binary), can lead to meaningless results and potential vulnerabilities.

Lean 4: A Powerful Proof Assistant

The team at Relays has been working using Lean 4, a dependently typed functional programming language that doubles as a proof assistant. Lean 4 leverages the Curry-Howard isomorphism, treating propositions as types and programs as proofs. This allows developers to reason about programs and mathematical structures with the same rigor applied to formal mathematical proofs.
Some features this allows for:
– Code-as-proof paradigm
– Maintainable and collaborative proof development
– Integration with version control systems
– Access to a vast corpus of implemented mathematics
– Building Composable Circuit Builders
Using Lean 4 to create a system for formally verifying arithmetic circuits involves the following steps:
– Representing constraint systems as propositions (type Prop)
– Using continuation passing style for composable circuit builders
– Implementing helpers that are unconstrained for existential quantification, and asserts for adding constraints
With these tools, developers can rewrite circuit elements, such as the binary representation example, in a more formalized and verifiable manner.
Proving Determinism and Semantic Properties
One of the key advantages of this approach is the ability to prove important properties about circuits, including semantic properties.

Application: Verifying the Semaphore Protocol

To showcase the practical utility of this approach, Marcin presented a case study of verifying the Semaphore protocol, a popular zero-knowledge system for anonymous signaling. Using Lean 4, they were able to prove critical properties of the protocol, such as:
– The signaler in any valid circuit assignment is present in the Merkle tree
– No unauthorized signaling is possible
– Double signaling (e.g., double voting) is prevented
These proofs directly correspond to the security guarantees outlined in the original Semaphore protocol paper, but with the added benefit of being tied to an actual implementation.

Compiling from Gnark

Recognizing that most developers don’t write circuits directly in Lean, Kostrzewa’s team developed a compiler that translates Gnark circuits into equivalent Lean representations. This allows developers to continue using familiar tools while gaining the benefits of formal verification. The workflow is as follows:
– Write circuits in Gnark
– Use the compiler to generate Lean definitions
– Define and prove theorems about the circuit properties
– Integrate verification into continuous integration (CI) pipelines
This approach makes formal verification an integral part of the development process, ensuring that desired properties are maintained with each code change.

Real-World Impact and Discoveries

The team uncovered a vulnerability in Gnark’s standard library, specifically in a number comparison gadget (resulting in a CVE).
They have also verified Worldcoin’s state management circuit, proving properties such as system progression and absence of circuit-level censorship.

Future Directions and Challenges

While the current system shows great promise, there are still areas for improvement being worked on:
– Improved support for probabilistic reasoning, crucial for modern ZK circuit development involving recursion and commitment schemes
– Integration with other circuit development frameworks, such as Noir (in partnership with the Aztec team)
– Addressing the limitations of deterministic reasoning in cryptographic contexts, particularly when dealing with concepts like collision resistance
Some of the discussions that arose from this talk included the potential for writing circuits directly in Lean, balancing theoretical elegance with practical adoption. However, this will be limited by performance issues with Lean when dealing with very large circuits (around 2,000 lines). Therefore, there are trade-offs between full correctness proofs and more targeted, automated checks for specific bug classes. There is also need to maintain abstraction and modularity in circuit design to manage complexity.
Formal verification of arithmetic circuits represents a significant step forward in enhancing the security and reliability of zero-knowledge protocols. By leveraging powerful tools like Lean 4 and integrating verification into the development workflow, we could address many of the common vulnerabilities that have plagued ZK systems. At the same time, it requires careful consideration of the balance between theoretical rigor and practical implementability.
The work presented by Marcin and his team at Reilabs opens up exciting possibilities for the future of ZK protocol development. When formal verification becomes more accessible and integrated into standard development practices, we may see a significant reduction in circuit-related vulnerabilities and an overall increase in the security of cryptographic systems right from the get-go.