Scalable Verification of Zero-Knowledge Protocols
Miguel Isabel, Clara Rodríguez-Núñez, Albert Rubio
IEEE Symposium on Security and Privacy 2024 · Day 2 · Continental Ballroom 6
This talk, presented by Clara Rodríguez-Núñez alongside Miguel Isabel and Albert Rubio from the University of Complutense Madrid, delves into the critical challenge of verifying **Zero-Knowledge Protocols (ZKPs)**. Specifically, it addresses the pervasive issue of **under-constraint bugs** in arithmetic circuits, which form the computational backbone of many ZKPs. These vulnerabilities can have severe security implications, potentially allowing malicious actors to forge valid proofs for false statements, thereby undermining the integrity and trustworthiness of ZKP-based systems.
AI review
This talk introduces Cyber, a groundbreaking tool for scalable semantic verification of Zero-Knowledge Proof circuits, directly tackling the pervasive and critical issue of under-constraint bugs. By innovating with transformation rules for finite fields and modular reasoning for massive circuits, it offers a robust solution where prior approaches failed. Its proven ability to find real-world vulnerabilities makes it indispensable for ZKP security.