Formalizing Soundness Proofs of Linear PCP SNARKs
Bolton Bailey, Andrew Miller
33rd USENIX Security Symposium · Day 1 · USENIX Security '24
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.
AI review
This talk presents a critical deep dive into the formal verification of SNARK soundness proofs using the Lean theorem prover. By successfully formalizing and verifying six prominent linear PCP SNARKs, including Groth16, this work provides unprecedented assurance for foundational cryptographic primitives. It's a significant advancement in cryptographic security, directly addressing the subtle complexities and potential hidden errors in manual proofs.