使用虚假证明攻击欠约束的Circom电路
- RareSkills
- 发布于 2024-03-20 12:10
- 阅读 781
本文深入探讨了 Circom 中的 <-- 操作符的一个潜在漏洞，展示了如何通过创建伪造的见证文件来利用这一漏洞，从而违背开发者对电路期望的假设。在详细的步骤中，介绍了生成有效证明的过程，以及如何修改二进制见证文件以实现攻击。此漏洞的理解对于开发安全的电路至关重要。
The <-- 运算符在 Circom 中可能是危险的，因为它将值分配给信号但不对其进行约束。那么你实际上是如何 利用 编写这个漏洞的POC（概念验证）的呢？
我们将要黑入以下电路：
pragma circom 2.1.8;
template Mul3() {
signal input a;
signal input b;
signal input c;
signal output out;
signal i;
a * b === 1; // 强制 a * b === 1
i <-- a * b; // i 必须等于 1
out <== i * c; // out 必须等于 c，因为 i === 1
}
component main{public [a, b, c]} = Mul3();
将此电路保存为 mul3.circom（缩写为乘以三个变量）。
电路似乎强制 a 和 b 的乘积为 1，然后将 1 分配给 i。
最后，out 被约束为 i * c。由于 i 似乎只能取值 1，因此 out 必须等于 c。
这里的个错误在于 <-- 并没有创建一个约束，而是计算一个值并将其分配给 i。实际上，i 可以是我们想要的任何值，它不必是 a * b 或 1。
这个漏洞涉及分配一个不是 a * b === 1 的值给 i，使得 out ≠ c。
总而言之，电路编写者 期望 out = c，但我们将违反此假设。在当前的示例中，没有造成什么伤害，但在实际应用中，如果两个信号必须具有相同的值，这可能会成为一个问题。
但我们究竟如何创建这个漏洞？
利用的步骤
生成有效的证明
要为 Circom 电路创建一个证明，我们首先需要为电路创建一个 input.json：
{"a": "1", "b": "1", "c": "5"}
这将满足电路：
a * b === 1; // 1 * 1 === 1
i <-- a * b; // 1 <-- 1 * 1
out <== i * c; // 5 <== 1 * 5;
// out === c 正如开发者所期待的
我们使用以下命令将电路编译为 r1cs：
circom mul3.circom --r1cs --wasm --sym
然后，使用创建的 wasm 文件生成一个见证，使用 input.json 作为输入：
cd mul3_js/
node generate_witness.js mul3.wasm ../input.json ../witness.wtns
cd ..
我们可以通过以下命令查看 snarkjs 为我们计算的见证：
snarkjs wtns export json witness.wtns witness.json
cat witness.json
见证信号布局
见证向量中的第一个条目始终为 1。（这在我们的 r1cs 文章 中已有解释，读者可以查阅）。向量中其余元素是电路中的值。我们可以通过查看 input.json、mul3.sym 和 witness.json 文件来查看哪个元素对应哪个信号：
cat input.json
cat mul3.sym
cat witness.json
我们在下面的 witness.json 文件中显示输出并添加标签，用黄色标记：
