ZKP项目方必读 | 电路审计：冗余约束真的冗余吗？

本文作者：Beosin安全研究专家Saya & Bryce

1. 前言

ZKP（Zero-Knowledge Proof）项目主要包含链下电路、链上合约两部分，其中电路部分由于涉及业务逻辑的约束抽象以及复杂的密码学基础知识，所以该部分是项目方实现的难点，同时也是安全人员的审计难点，由于Beosin最近在关于ZKP相关的审计中发现了诸多安全问题，下面列举一种容易被项目方忽视的安全案例 — “冗余约束”，目的是提醒项目方和用户注意相关安全风险。

2. 冗余约束能删除吗

审计ZKP项目时，通常会见到如下奇怪约束，但很多项目方实际并不理解具体含义，为了降低电路复用的难度和节省链下计算消耗，可能会删除部分约束，从而造成安全问题：

我们将上述代码删除前后生成的约束数量进行对比，发现在一个实际项目中有无上述约束，对项目约束总量的变化影响很小，因为它们很容易被项目方自动优化忽略

而实际上述电路的目的仅仅是为了在证明中附加一段数据，以Tornado.Cash为例附加的数据包括：接收者地址、中继relayer地址、手续费等，由于这些信号不影响后续电路的实际计算，所以可能会让部分其他项目方产生疑惑，从而将其从电路中删除，导致部分用户交易被抢跑。

下面将以简单的隐私交易项目Tornado.Cash为例介绍这种攻击，本文将电路中附加信息的相关信号和约束删除后具体如下：

为了便于理解，本文删除了电路中校验Merkle Tree和nullifierHash相关的部分，同时也将收款人地址等信息注释。该电路生成的链上合约中，本文使用两个不同的地址同时进行verify，可以发现两个不同地址都可以通过校验：

但是当将下面代码添加到电路约束中时，可以发现只有电路中设置的recipient地址才能通过校验：

所以当Proof未与recipient绑定时，可以发现recipient的地址可以被随意更换而zk proof都可以校验通过，那么当用户想从项目池中提款时就可能被MEV抢跑。下面是某隐私交易DApp的MEV抢跑攻击示例：

3. 冗余约束的错误写法

此外，电路中还有两种常见的错误写法，可能导致更加严重的双花攻击：一种是电路中设置了input信号，但是未对该信号进行约束，另一种是信号的多个约束之间存在线性依赖关系。下图为Groth16算法常见的Prove和Verify计算流程：

Prover生成证明Proof π = ([A]1,[C]1,[B]2)：

Verifier接收到证明π[A、B、C]后经过如下验证方程计算，如果成立则验证通过，否则验证不通过：

3.1 信号未参与约束

如果某个公共信号  在电路中不存在任何约束，那么对于其约束  来说，下列式子值恒为0（其中  是Verifier需要Prover计算的随机挑战值）：

同时，这意味着对于  来说，任意的  均有以下式子：

因此，验证方程中下列式子针对信号  有：

由于验证方程如下：

可以发现，无论  取任何值，该项计算的结果总是为0。

本文修改Tornado.Cash电路如下，可以看到该电路有1个公共输入信号recipient，以及3个私有信号root、nullifier、secret，其中recipient在该电路中并不存在任何约束：

本文将在最新的snarkjs库0.7.0版本上测试，将其隐式约束代码删除，以展示电路存在没有约束信号时的双花攻击效果，核心exp代码如下：

可以看到生成的两个Proof都通过了校验：

3.2 线性依赖型约束

实际开发的过程中，项目方可能为了提升效率采用一行约束包含上述的所有附加信号，但是如果公共信号  和 私有信号  存在线性依赖关系，那么攻击者可以伪造证明实现双花攻击。本文简单阐述攻击流程，具体的推导过程见参考文献。首先假设二者的线性依赖因子为  ，对于   ，可以通过下列计算伪造证明：

同样以Tornado.Cash为例，假设项目方用  来同时约束recipient、relayer、fee三个信号，具体电路如下：

上述电路可能导致双花攻击，具体的exp核心代码如下：

同样修改部分库代码后，我们在snarkjs 0.7.0版本上进行测试，结果为如下两个伪造的proof都可以通过验证：

• publicsingnal1 + proof1

• publicsingnal2 + proof2

4 修复方案

4.1 zk库代码

目前部分流行的zk库如snarkjs库会在电路中隐式的加入一些约束，例如一个最简单的约束：

上述式子在数学上恒成立，因此无论实际的信号值是多少，符合任何约束，都可以在setup期间被库代码隐式的统一添加到电路中，此外在电路中使用第一节的平方约束则是更为安全的做法。例如snarkjs在setup期间生成zkey时隐式添加了下列约束：

4.2 电路

项目方在设计电路时，由于使用的第三方zk库可能在setup或编译期间并不会添加额外约束，所以我们建议项目方尽量在电路设计层面保证约束的完整性，在电路中严格对所有信号进行合法约束以保证安全性，例如前文所示的平方约束。

Beosin作为一家全球领先的区块链安全公司，在全球10多个国家和地区设立了分部，业务涵盖项目上线前的代码安全审计、项目运行时的安全风险监控、预警与阻断、虚拟货币被盗资产追回、安全合规KYT/AML等“一站式”区块链安全产品+服务，目前已为全球3000多个区块链企业提供安全技术服务，审计智能合约超过3000份，在ZKP项目审计方面，Beosin非常具有经验。欢迎点击公众号留言框，与我们联系。

参考文献：https://geometry.xyz/notebook/groth16-malleability