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.

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