利用约束不足的零知识证明电路

  • Dacian
  • 发布于 2024-07-02 11:47
  • 阅读 61

本文深入探讨了零知识证明(ZK)电路中的安全漏洞,重点分析了电路因约束不足而导致的模运算溢出漏洞,并通过示例展示了如何利用此漏洞伪造非素数证明。文章还提出了通过范围约束来防止溢出的解决方案,并强调了审计 ZK 电路时需注意的不同 p 值对范围约束和溢出产生的影响。

Zero-Knowledge (ZK) Circuits(零知识电路)允许:

  • Provers(证明者)在不泄露他们用来提出声明的私有信息的情况下提出声明

  • Verifiers(验证者)验证 Prover(证明者)提出的声明,而无需信任 Prover(证明者)或知道 Prover(证明者)用来提出声明的任何私有信息

ZK 属性

ZK 系统有 3 个重要的属性:

  1. Completeness(完整性)- 给定有效的输入,Prover(证明者)能够生成有效的 Proofs(证明),这些 Proofs(证明)被 Verifier(验证者)接受

  2. Soundness(可靠性)- 恶意的 Prover(证明者)无法(实际上概率非常低)生成无效/伪造的 Proofs(证明),这些 Proofs(证明)会被 Verifier(验证者)接受

  3. Zero Knowledge(零知识)- Prover(证明者)已知的 Private Inputs(私有输入)不会泄露,也不能从提供给 Verifier(验证者)的 Proof(证明)或 Public Inputs(公共输入)中进行逆向工程

ZK 漏洞

ZK Circuits(零知识电路)中的许多漏洞都涉及破坏这些重要属性中的一个或多个;大多数电路漏洞可以分为 3 个一般类别:

  1. Over-Constrained(过度约束)- Prover(证明者)能够创建一个有效的 Proof(证明),但 Verifier(验证者)无法验证它,因为 Circuit(电路)包含太多的 Constraints(约束),破坏了“Completeness(完整性)”属性

  2. Under-Constrained(约束不足)- 恶意的 Prover(证明者)可以创建一个无效的 Proof(证明),Verifier(验证者)随后会验证它,因为 Circuit(电路)包含的 Constraints(约束)太少,破坏了“Soundness(可靠性)”属性

  3. Non-Zero Knowledge(非零知识)- Prover(证明者)使用的 Private Inputs(私有输入)泄露或能够被 Verifier(验证者)或其他观察者逆向工程,破坏了“Zero Knowledge(零知识)”属性

易受攻击的 Circuit(电路) - “Is Not Prime(不是质数)”

让我们从创建一个 Circuit(电路)来证明一个数字不是质数开始。要设置存储库,请使用其中一个集成 Hardhat 的 Circom “starter(启动器)”存储库[ 1, [2]](https://github.com/alexroan/zk-playground/tree/main),以便更轻松地进行编译和测试工作流程。对于此示例,我们将使用[第二个](https://github.com/alexroan/zk-playground/tree/main)链接,然后

为了简单起见,我们不会创建新文件,而是简单地编辑已存在的文件;首先将我们的示例 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(私有输入)factorOnefactorTwo,它们是 Prover(证明者)用来断言其声明的秘密输入;这些输入不应泄露或以其他方式披露给 Verifier(验证者)或其他观察者

  • 包含 1 个 Constraint(约束)(使用 === 运算符),它强制 factorOnefactorTwo 的乘积结果为 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(电路)似乎工作正常!

利用 Under-Constrained(约束不足)的因子

回想一下,Circuit(电路)只有 1 个 Constraint(约束):两个因子的乘积必须等于被证明的值:

// constraint(约束):因子相乘得到 val
// 对于质数将失败
val === factorOne * factorTwo;

但是,对于 factorOnefactorTwo 的可能值没有 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(证明者)能够利用 factorOnefactorTwo 的约束不足来创建一个虚假的 Proof(证明),该 Proof(证明)成功验证了数字 7 不是质数,这当然是不正确的,因为 7 是一个质数!

约束因子

由于 Circuit(电路)是 Under-Constrained(约束不足)的,我们需要添加额外的 Constraints(约束)来防止 factorOnefactorTwo 等于 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(电路)。然而,仍然存在一个更加微妙的漏洞……

利用 Finite Fields(有限域)中的 Modular Arithmetic(模运算)溢出

ZK Circuits(零知识电路)使用 Modular Arithmetic(模运算)在 Finite Field(有限域)Fp 中运行,默认值p = 21888242871839275222246405745257275088548364400416034343698204186575808495617,尽管可以使用 -p 编译选项更改 p 的值。

由于 Modular Arithmetic(模运算),数字会回绕;为了简单起见,考虑 Finite Field(有限域)F11p = 11。然后,Prover(证明者)可以将以下输入传递给我们的“已修复”Circuit(电路):

  const sampleInput = {
    val: "7",
    factorOne: "6",
    factorTwo: "3"
  };

当 Circuit(电路)执行时,由于 F11p = 11 的 Modular Arithmetic(模运算),6 * 3 = 18 回绕到 7,因为 11 回绕到 0。一个恶意的 Prover(证明者)可以利用此溢出来创建一个虚假的 Proof(证明),证明 7 不是质数!因此,“已修复”的 Circuit(电路)仍然包含一个关键且更微妙的“Under-Constrained(约束不足)”漏洞,因为对使用 Finite Field(有限域)中的 Modular Arithmetic(模运算)Range(范围)内的输入没有 Constraint(约束)。

Range(范围)限制以防止溢出

为了处理 factorOne * factorTwo 的乘法溢出,我们需要约束两个因子,使其乘积小于 Finite Field(有限域)Fpp。为了实现这一点,我们将每个因子 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(范围)。

附加资源

特别感谢 rkm0959cergyk1337,感谢他们宝贵的 ZK 见解,并感谢 cyfrin.io 在审计之间为我提供研究时间来学习和探索。一些有用的附加资源包括:

  • 原文链接: dacian.me/exploiting-und...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
Dacian
Dacian
in your storage