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的检查时间也有明显改进，展现出较先前工作数量级级的提升。