While ZK brings trust to computation, software verification has long ensured program correctness;
explore this intersection in π
"The Ouroboros of ZK: Why Verifying the Verifier Unlocks Longer-Term ZK Innovation" by @dfirsov and @convoluted_code from @the_matter_labs! π§΅
explore this intersection in π
"The Ouroboros of ZK: Why Verifying the Verifier Unlocks Longer-Term ZK Innovation" by @dfirsov and @convoluted_code from @the_matter_labs! π§΅
π§ Zero-knowledge proofs (ZK) offer a secure, efficient alternative to traditional multi-execution models in blockchains. Sadly, bugs in provers and verifiers can jeopardize the entire system.
π Verifying the verifier is crucial. It reduces the trusted computing base (TCB), ensures integrity, and enables decentralized proof generation by potentially untrusted parties.
π οΈ Implementing ZK proofs isn't exactly just about math.
Real-world applications reveal discrepancies between theoretical and practical implementations, often leading to critical bugs, as our recent work demonstrates here: arxiv.org
Real-world applications reveal discrepancies between theoretical and practical implementations, often leading to critical bugs, as our recent work demonstrates here: arxiv.org
π An honest verifier is associated with the fundamental properties of proof systems: completeness, soundness, and proof of knowledge.
This means valid proofs are accepted, invalid ones are rejected, and proofs genuinely demonstrate knowledge of the underlying statement.
This means valid proofs are accepted, invalid ones are rejected, and proofs genuinely demonstrate knowledge of the underlying statement.
π Recent audits reveal significant vulnerabilities in ZK verifiers. Various ZK EVMs highlight the need for rigorous verification of the verifier to ensure the correctness of this mission-critical code.
π Decentralized proving markets (e.g., Snarketplace, Gevulot, and others) are rising.
Verifier verification is essential to safely include provers that run on untrusted, potentially custom-designed hardware, maintaining the integrity of the proof generation process.
Verifier verification is essential to safely include provers that run on untrusted, potentially custom-designed hardware, maintaining the integrity of the proof generation process.
π‘οΈ Our approach leverages EasyCrypt for formal verification of the zkSync Era verifier, implemented in YUL inline assembly.
This method involves extracting verifier code, defining mathematical specifications, and proving equivalence between implementations.
This method involves extracting verifier code, defining mathematical specifications, and proving equivalence between implementations.
π§ Translating YUL code to EasyCrypt presents challenges, but the custom-built YUL-to-EasyCrypt transpiler ensures soundness and effectively handles memory state and side effects.
π‘Bottom line: Formal verification of ZK verifiers is vital for the security and scalability of ZK systems.
It minimizes trust requirements and paves the way for a decentralized, secure future.
It minimizes trust requirements and paves the way for a decentralized, secure future.
π Embracing this approach can significantly enhance the reliability and robustness of ZK rollups, unlocking new possibilities for blockchain technology.
π¨οΈΒ Read the full paper: eprint.iacr.org
π¨οΈΒ Read the full paper: eprint.iacr.org
.@zkProof 6 in Berlin hosted the VP of Research @convoluted_code from @the_matter_labs team.
Watch the presentation here: youtube.com
Watch the presentation here: youtube.com
This is the last tweet of the thread.
Loading suggestions...