Scalable Verification of Zero-Knowledge Protocols

The application of Zero-Knowledge (ZK) proofs is rapidly growing in the industry and has become a key element to enable privacy and enhance scalability in public distributed ledgers. In most practical ZK systems, the statement to be proven is expressed by means of a set of polynomial equations in a prime field that describe an arithmetic circuit. Describing general statements using this kind of constraints is a complex and error-prone task. This can be partly mitigated by using high-level programming languages, but at the cost of losing control over the added constraints and, as a result, obtaining too large systems for complex statements. In this context, having tools to automatically verify properties of the constraint systems is of paramount importance to guarantee the security of the protocol. However, since non-linear polynomial reasoning over a finite field is needed for checking challenging properties, existing automatic tools either do not scale or cannot detect non-trivial bugs. In this paper, we present a new scalable modular technique based on the application of transformation and deduction rules that have proven to be very effective in verifying properties over the signals of a circuit given as a set of polynomial equations in a large prime field. Our technique has been implemented in a tool called CIVER and applied to verify safety properties for circuits implemented in circom, which is one of the most popular languages for defining ZK protocols. We have been able to analyze large industrial circuits and detect subtle vulnerabilities in circuits designed by expert programmers.