ZKP systems have surged attention and held a fundamental role in contemporary cryptography. Zk-SNARK protocols dominate the ZKP usage, often implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. Underconstrained circuits refer to circuits that lack the necessary constraints, resulting in unexpected solutions in the circuit and causing the verifier to accept a bogus witness. Overconstrained circuits refer to circuits that are constrained excessively, resulting in the circuit lacking necessary solutions and causing the verifier to accept no witness, rendering the circuit meaningless. This paper introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving polynomial equation systems over a finite field by algebraic computation. The classification of verification results is refined, greatly enhancing the expressive power of the system. We proposed a tool, AC4, to represent the implementation of this method. Experiments demonstrate that AC4 represents a substantial 29% increase in the checked ratio compared to prior work. Within a solvable range, the checking time of AC4 has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.

翻译：零知识证明（ZKP）系统近年来受到广泛关注，并在现代密码学中扮演着基础性角色。Zk-SNARK协议主导了ZKP的应用，通常通过算术电路编程范式实现。然而，欠约束或过约束电路可能导致漏洞。欠约束电路指缺乏必要约束的电路，导致电路中存在意外解，使验证者接受虚假证明；过约束电路指约束过多的电路，导致电路缺失必要解，使验证者无法接受任何证明，从而使得电路失去意义。本文提出了一种新颖方法，用于精确定位ZKP电路中的两种不同类型漏洞。该方法将算术电路约束编码为多项式方程组，并通过代数计算在有限域上求解这些方程组。验证结果的分类得到细化，极大增强了系统的表达能力。我们提出了工具AC4来实现该方法。实验表明，与先前工作相比，AC4的检测率提升了29%。在可解范围内，AC4的检验时间也实现了显著改善，相较之前的工作展现出数量级级别的提升。