本文深入探讨了零知识证明(ZK)电路中的安全漏洞,重点分析了电路因约束不足而导致的模运算溢出漏洞,并通过示例展示了如何利用此漏洞伪造非素数证明。文章还提出了通过范围约束来防止溢出的解决方案,并强调了审计 ZK 电路时需注意的不同 p 值对范围约束和溢出产生的影响。
Zero-Knowledge (ZK) Circuits(零知识电路)允许:
Provers(证明者)在不泄露他们用来提出声明的私有信息的情况下提出声明
Verifiers(验证者)验证 Prover(证明者)提出的声明,而无需信任 Prover(证明者)或知道 Prover(证明者)用来提出声明的任何私有信息
ZK 系统有 3 个重要的属性:
Completeness(完整性)- 给定有效的输入,Prover(证明者)能够生成有效的 Proofs(证明),这些 Proofs(证明)被 Verifier(验证者)接受
Soundness(可靠性)- 恶意的 Prover(证明者)无法(实际上概率非常低)生成无效/伪造的 Proofs(证明),这些 Proofs(证明)会被 Verifier(验证者)接受
Zero Knowledge(零知识)- Prover(证明者)已知的 Private Inputs(私有输入)不会泄露,也不能从提供给 Verifier(验证者)的 Proof(证明)或 Public Inputs(公共输入)中进行逆向工程
ZK Circuits(零知识电路)中的许多漏洞都涉及破坏这些重要属性中的一个或多个;大多数电路漏洞可以分为 3 个一般类别:
Over-Constrained(过度约束)- Prover(证明者)能够创建一个有效的 Proof(证明),但 Verifier(验证者)无法验证它,因为 Circuit(电路)包含太多的 Constraints(约束),破坏了“Completeness(完整性)”属性
Under-Constrained(约束不足)- 恶意的 Prover(证明者)可以创建一个无效的 Proof(证明),Verifier(验证者)随后会验证它,因为 Circuit(电路)包含的 Constraints(约束)太少,破坏了“Soundness(可靠性)”属性
Non-Zero Knowledge(非零知识)- Prover(证明者)使用的 Private Inputs(私有输入)泄露或能够被 Verifier(验证者)或其他观察者逆向工程,破坏了“Zero Knowledge(零知识)”属性
让我们从创建一个 Circuit(电路)来证明一个数字不是质数开始。要设置存储库,请使用其中一个集成 Hardhat 的 Circom “starter(启动器)”存储库[ 1, [2]](https://github.com/alexroan/zk-playground/tree/main),以便更轻松地进行编译和测试工作流程。对于此示例,我们将使用[第二个](https://github.com/alexroan/zk-playground/tree/main)链接,然后:
将 2-hardhat-integration
复制到一个新文件夹中,作为我们的项目文件夹
将 hardhat.config.js
中 ptau
的 URL 更改为 ptau: "<
https://hermez.s3-eu-west-1.amazonaws.com/powersOfTau28_hez_final_15.ptau
>"
为了简单起见,我们不会创建新文件,而是简单地编辑已存在的文件;首先将我们的示例 Circuit(电路)代码放入 circuits/multiplier.circom
中:
pragma circom 2.1.4;
// Prover(证明者)使用 Circuit(电路)`IsNotPrime` 来证明 `val` 不是
// 一个质数,而不泄露 Prover(证明者)知道并用来证明这一点的私有因子
template IsNotPrime() {
signal input factorOne;
signal input factorTwo;
signal input val;
// constraint(约束):因子相乘得到 val
// 对于质数将失败
val === factorOne * factorTwo;
}
// `val` 是公共的,因子是私有的
component main {public [val]} = IsNotPrime();
这个 Circuit(电路):
接受 1 个 Public Input(公共输入)val
,Prover(证明者)声称该数字不是质数
接受 2 个 Private Inputs(私有输入)factorOne
和 factorTwo
,它们是 Prover(证明者)用来断言其声明的秘密输入;这些输入不应泄露或以其他方式披露给 Verifier(验证者)或其他观察者
包含 1 个 Constraint(约束)(使用 ===
运算符),它强制 factorOne
和 factorTwo
的乘积结果为 val
- 如果这是真的,那么 val
不应该是质数
接下来将输入放入 circuits/multiplier.json
中:
{
"val": 21,
"factorOne": 3,
"factorTwo": 7
}
然后将测试放入 test/multiplier.test.js:
中:
const hre = require("hardhat");
const { assert } = require("chai");
describe("multiplier circuit", () => {
let circuit;
const sampleInput = {
val: "21",
factorOne: "7",
factorTwo: "3"
};
const sanityCheck = true;
before(async () => {
circuit = await hre.circuitTest.setup("multiplier");
});
it("produces a witness with valid constraints", async () => {
const witness = await circuit.calculateWitness(sampleInput, sanityCheck);
await circuit.checkConstraints(witness);
});
it("has expected witness values", async () => {
const witness = await circuit.calculateLabeledWitness(
sampleInput,
sanityCheck
);
assert.propertyVal(witness, "main.val", sampleInput.val);
assert.propertyVal(witness, "main.factorOne", sampleInput.factorOne);
assert.propertyVal(witness, "main.factorTwo", sampleInput.factorTwo);
});
});
使用 yarn circom:dev
编译,并使用 yarn test
运行测试 - 一切都通过了,我们的 Circuit(电路)似乎工作正常!
回想一下,Circuit(电路)只有 1 个 Constraint(约束):两个因子的乘积必须等于被证明的值:
// constraint(约束):因子相乘得到 val
// 对于质数将失败
val === factorOne * factorTwo;
但是,对于 factorOne
和 factorTwo
的可能值没有 Constraints(约束);Prover(证明者)可以将它们设置为他们喜欢的任何值。一个恶意的 Prover(证明者)可以滥用它来创建一个虚假的 Proof(证明)吗?事实证明答案是肯定的。
Prime Number(质数) 是一个无符号整数,它:
大于 1
不能写成两个较小数字的乘积,这两个数字本身也大于 1
在 test/multiplier.test.js
中更改 sampleInput
以将被证明的数字乘以 1:
const sampleInput = {
val: "7",
factorOne: "1",
factorTwo: "7"
};
然后使用 yarn test
重新运行测试套件,一切都通过了 - 一个恶意的 Prover(证明者)能够利用 factorOne
和 factorTwo
的约束不足来创建一个虚假的 Proof(证明),该 Proof(证明)成功验证了数字 7 不是质数,这当然是不正确的,因为 7 是一个质数!
由于 Circuit(电路)是 Under-Constrained(约束不足)的,我们需要添加额外的 Constraints(约束)来防止 factorOne
和 factorTwo
等于 1。在 Solidity 中,这将相对简单:
require(factorOne != 1 && factorTwo != 1);
然而,Circom Constraints(约束)必须是 Quadratic Equations(二次方程),以便它们可以轻松地与 Rank One Constraint System(秩 1 约束系统) (R1CS) 一起使用。因此,我们必须使用一些数学技巧来表达兼容形式的 require(x != 1)
。为此,我们将修改 circomlib 库中已有的一个数学技巧;将新的扩展 Circuit(电路)放入 circuits/multiplier.circom
中:
pragma circom 2.1.4;
// 略有修改自
// https://github.com/iden3/circomlib/blob/master/circuits/comparators.circom#L24-L34
// 数学技巧来实现 `require(input != 1)`
// 不能优雅地处理 input == 0 的情况
// 但此电路不需要这样做
// 因为 0 的因子不能用于创建
// 虚假的证明
template IsOne() {
signal input in;
signal output out;
// 中间信号
signal inv;
// 将数据存储到 `inv` 中间信号:
// 如果 input != 1 -> inv = 1/in
// 否则 input == 1 -> inv = 0
inv <-- in != 1 ? 1/in : 0;
// 使用数学技巧存储和约束 `out`,
// 这将使末尾的 constraint(约束)对于 input == 1 失败
//
// 情况 a) 如果 input 是 1,那么 inv = 0
// out <== -1 * 0 + 1
// out <== 1 (将使末尾的 constraint(约束)失败)
// 情况 b) 如果 input 是 2,那么 inv = 1/2
// out <== -2*1/2 + 1
// out <== -1 + 1
// out <== 0
out <== -in*inv + 1;
// constraint(约束)阻止因子为 1
// 情况 a) 如果 input 是 1,那么 in = 1 并且 out = 1
// in*out = 1*1 = 1 -> constraint(约束)失败
// 情况 b) 如果 input 是 2,那么 in = 2 并且 out = 0
// in*out = 2*0 = 0 -> constraint(约束)通过
in*out === 0;
}
// Prover(证明者)使用 Circuit(电路)`IsNotPrime` 来证明 `val` 不是
// 一个质数,而不泄露 Prover(证明者)知道并用来证明这一点的私有因子
template IsNotPrime() {
signal input factorOne;
signal input factorTwo;
signal input val;
// constraint(约束):因子相乘得到 val
// 对于质数将失败
val === factorOne * factorTwo;
// 阻止 factorOne == 1
component f1Check = IsOne();
f1Check.in <== factorOne;
// 阻止 factorTwo == 1
component f2Check = IsOne();
f2Check.in <== factorTwo;
}
// `val` 是公共的,因子是私有的
component main {public [val]} = IsNotPrime();
再次使用 yarn circom:dev
编译后,更改 test/multiplier.test.js
中的测试 sampleInputs
,以便为不同的运行使用不同的值,以验证 Prover(证明者)不能再通过将 val
乘以 1 来创建虚假的 Proof(证明):
// 失败,因为 factorOne == 1
const sampleInput = {
val: "21",
factorOne: "1",
factorTwo: "21"
};
// 失败,因为 factorTwo == 1
const sampleInput = {
val: "21",
factorOne: "21",
factorTwo: "1"
};
// 成功,因为 factorOne != 1 并且
// factorTwo != 1 并且
// factorOne * factorTwo == val
const sampleInput = {
val: "21",
factorOne: "7",
factorTwo: "3"
};
// 失败,因为 factorOne * factorTwo != val
const sampleInput = {
val: "21",
factorOne: "7",
factorTwo: "4"
};
我们的 2 个附加 Constraints(约束)和扩展的测试套件似乎已经解决了这个问题;一个恶意的 Prover(证明者)不能再通过让一个质数乘以 1 来错误地证明它不是质数来利用 Circuit(电路)。然而,仍然存在一个更加微妙的漏洞……
ZK Circuits(零知识电路)使用 Modular Arithmetic(模运算)在 Finite Field(有限域)Fp
中运行,默认值为 p = 21888242871839275222246405745257275088548364400416034343698204186575808495617
,尽管可以使用 -p
编译选项更改 p
的值。
由于 Modular Arithmetic(模运算),数字会回绕;为了简单起见,考虑 Finite Field(有限域)F11
的 p = 11
。然后,Prover(证明者)可以将以下输入传递给我们的“已修复”Circuit(电路):
const sampleInput = {
val: "7",
factorOne: "6",
factorTwo: "3"
};
当 Circuit(电路)执行时,由于 F11
中 p = 11
的 Modular Arithmetic(模运算),6 * 3 = 18
回绕到 7
,因为 11
回绕到 0
。一个恶意的 Prover(证明者)可以利用此溢出来创建一个虚假的 Proof(证明),证明 7
不是质数!因此,“已修复”的 Circuit(电路)仍然包含一个关键且更微妙的“Under-Constrained(约束不足)”漏洞,因为对使用 Finite Field(有限域)中的 Modular Arithmetic(模运算)Range(范围)内的输入没有 Constraint(约束)。
为了处理 factorOne * factorTwo
的乘法溢出,我们需要约束两个因子,使其乘积小于 Finite Field(有限域)Fp
的 p
。为了实现这一点,我们将每个因子 x
约束在 2 <= x < sqrt(p)
范围内;实际上,对于 Circom 的默认 p
,我们可以使用 2 <= x < 2 ** 100
,但审计员必须始终注意他们正在审计的 Circuit(电路)使用的 p
值,以及这对于由于 Modular Arithmetic(模运算)导致的 Range(范围)限制和溢出的影响。
对于我们更新的解决方案,我们将编写一个新的 InRange
模板来执行 Range(范围)检查,并利用circomlib 中的更多数学技巧。这允许我们删除以前强制执行 factor != 1
的 Constraints(约束),因为这现在由 Range(范围)检查处理。将新的完整代码放入 circuits/multiplier.circom
中:
pragma circom 2.1.4;
// helpers taken from circomlib
// 从 circomlib 获取的 helpers
template Num2Bits(n) {
signal input in;
signal output out[n];
var lc1=0;
var e2=1;
for (var i = 0; i<n; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] -1 ) === 0;
lc1 += out[i] * e2;
e2 = e2+e2;
}
lc1 === in;
}
template LessThan(n) {
assert(n <= 252);
signal input in[2];
signal output out;
component n2b = Num2Bits(n+1);
n2b.in <== in[0]+ (1<<n) - in[1];
out <== 1-n2b.out[n];
}
template LessEqThan(n) {
signal input in[2];
signal output out;
component lt = LessThan(n);
lt.in[0] <== in[0];
lt.in[1] <== in[1]+1;
lt.out ==> out;
}
template GreaterEqThan(n) {
signal input in[2];
signal output out;
component lt = LessThan(n);
lt.in[0] <== in[1];
lt.in[1] <== in[0]+1;
lt.out ==> out;
}
// written using circomlib helpers
// 使用 circomlib helpers 编写
// to enforce range constraints preventing
// 为了强制执行范围约束以防止
// overflow due to modular arithmetic
// 由于模运算导致的溢出
template InRange() {
signal input a;
signal input lowerbound;
signal input upperbound;
signal output out;
// if lowerbound <= a <= upperbound return 1 else 0
// 如果 lowerbound <= a <= upperbound 返回 1,否则返回 0
component lteCheck = LessEqThan(124);
lteCheck.in[0] <== a;
lteCheck.in[1] <== upperbound;
component gteCheck = GreaterEqThan(124);
gteCheck.in[0] <== a;
gteCheck.in[1] <== lowerbound;
out <== lteCheck.out * gteCheck.out;
}
// Prover(证明者)使用 Circuit(电路)`IsNotPrime` 来证明 `val` 不是
// 一个质数,而不泄露 Prover(证明者)知道并用来证明这一点的私有因子
template IsNotPrime() {
signal input factorOne;
signal input factorTwo;
signal input val;
// constraint(约束):因子相乘得到 val
// 对于质数将失败
val === factorOne * factorTwo;
// Circom circuits(电路):
// * operate in a Finite Field(有限域) Fp where p is one of
// several potential primes
// * 在 Finite Field(有限域) Fp 中运行,其中 p 是
// 几个潜在的质数之一
// * use Modular Arithmetic(模运算) (mod p) such that
// p wraps back around to 0
// * 使用 Modular Arithmetic(模运算)(mod p),以便
// p 包裹回到 0
//
// Consider simple case F11 so 11 wraps to 0, a Prover(证明者)
// could call this circuit with:
// 考虑简单情况 F11,所以 11 包裹到 0,一个 Provr(证明者)
// 可以使用以下内容调用此电路:
// factorOne = 6
// factorTwo = 3
// val = 7
//
// 6 * 3 = 18 which wraps to 7 due to mod 11
// 6 * 3 = 18,由于 mod 11,它包裹到 7
// Hence the Prover(证明者) could use this Circuit(电路)
// to create a false proof that 7 is not prime
// 因此,Prover(证明者)可以使用此 Circuit(电路)
// 创建一个虚假的证明,证明 7 不是质数
// by exploiting overflow due to Modular Arithmetic(模运算)
// 通过利用由于 Modular Arithmetic(模运算)导致的溢出
//
// To prevent overflow implement range check
// constraints on the factors
// 为了防止溢出,实现针对因子的范围检查约束
// {0, 1} not valid factors
// {0, 1} 不是有效因子
var MIN_RANGE = 2;
// must be below sqrt(p) for Fp, 2**100 works for default p
// 对于 Fp,必须低于 sqrt(p),2**100 适用于默认 p
// https://docs.circom.io/circom-language/basic-operators/#field-elements
var MAX_RANGE = 2 ** 100;
component f1RangeCheck = InRange();
f1RangeCheck.a <== factorOne;
f1RangeCheck.lowerbound <== MIN_RANGE;
f1RangeCheck.upperbound <== MAX_RANGE;
component f2RangeCheck = InRange();
f2RangeCheck.a <== factorTwo;
f2RangeCheck.lowerbound <== MIN_RANGE;
f2RangeCheck.upperbound <== MAX_RANGE;
// constraint(约束)to enforce factor range constraints
// 用于强制执行因子范围约束的约束
1 === f1RangeCheck.out * f2RangeCheck.out;
}
// `val` 是公共的,因子是私有的
component main {public [val]} = IsNotPrime();
虽然因子 Range(范围)检查 Constraints(约束)可以防止溢出利用,但一个需要注意的必然结果是,它们还限制了 Circuit(电路)可用于证明数字不是质数的数字 Range(范围)。
特别感谢 rkm0959 和 cergyk1337,感谢他们宝贵的 ZK 见解,并感谢 cyfrin.io 在审计之间为我提供研究时间来学习和探索。一些有用的附加资源包括:
- 原文链接: dacian.me/exploiting-und...
- 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!