Circom-Pairing：一个价值百万美元的 ZK 漏洞被及早发现

这篇博文也有以下语言版本: 简体中文.

Veridise 博客文章系列: circom-pairing 安全审计。

在这篇博文中，我们将剖析由 Veridise 在 circom-pairing 库中发现的一个关键安全问题。circom-pairing 库是椭圆曲线配对的 circom 实现，用于广泛采用的 BLS12–381 曲线。这个库使零知识 (ZK) 系统能够验证 BLS12–381 曲线上的签名。Veridise 团队在 Succinct Labs 委托的安全审计中发现了 circom-pairing 中的几个问题，Succinct Labs 的创新桥设计 严重依赖于验证 BLS12–381 签名。我们的团队发现的最关键的错误可能允许攻击者伪造签名。

你对更多细节感兴趣吗？ 系好安全带，继续阅读！但首先，介绍一下 circom-pairing 及其设计的一些背景知识。

Circom-Pairing 库

像 Circom 这样的语言中的程序将计算编码为一组约束。给定这些约束，编译器会生成两个工件。第一个称为证明者，为满足程序约束的输入-输出对生成证明。例如，在 circom-pairing 的上下文中，我们可以证明给定公钥的 BLS12–381 签名的有效性。第二个工件称为验证者，可以验证证明的有效性，而无需运行实际计算。由于证明生成时间取决于约束的数量，ZK 系统旨在减少验证者需要检查的约束。鉴于所有这些，你可能会认为在 Circom 中实现密码配对算法是一项艰巨的任务。嗯，你是 100% 正确的。

位数不足。 在 BLS12–381 上实现配对的第一个挑战源于曲线名称的 “381” 部分，它表示描述位于曲线上的整数对 (x,y) 所需的位数。但是，当前用于验证 circom 证明的生态系统仅支持 254 位整数。为了绕过这个限制，circom-pairing 的作者必须创建一个任意位长度整数的库（简称大整数）。每个库函数都对一个大整数进行操作，该整数由包含 n 位整数的 k 个寄存器组成。例如，考虑以下来自比较两个大整数的函数的代码片段。

/*
Inputs:
  - BigInts a, b
Output:
  - out = (a < b) ? 1 : 0
*/
template BigLessThan(n, k){
  signal input a[k];
  signal input b[k];
  signal output out;
  ...
}

正如 BigLessThan 的注释所示，如果数组 a 表示的整数小于数组 b 表示的整数，则输出信号 out 将设置为 1。否则，out 将被设置为 0。此外，模板 BigLessThan 确保整数 a 和 b 被正确格式化，即它们的每个 k 寄存器都包含一个 n 位整数。

到处都是约束。 实现 circom-pairing 的另一个挑战是，验证 BLS12–381 需要检查数百万个约束。优化如此复杂的 ZK 系统对 circom-pairing 开发人员提出了巨大的挑战。circom-pairing 中一个至关重要的设计决策是省略库中几个核心模板中的数据验证，这大大减少了生成的约束数量。例如，circom-pairing 中的几个核心电路假设它们的输入是格式正确且在一定范围内的大整数。因此，这些电路的用户还必须使用 BigLessThan 模板对核心电路执行适当的数据验证。正如我们接下来将看到的，这个决定不幸地适得其反。

你检查过你的信号了吗？再检查一次！

让我们讨论一些错误。 我们的团队发现的关键错误源于一个名为 CoreVerifyPubkeyG1 的电路，顾名思义，它具有验证公钥签名的关键任务。在执行签名验证之前，CoreVerifyPubkeyG1 必须确保其所有输入都符合 circom-pairing 核心模板所做的假设（还记得优化吗？）。这些假设中最重要的是，所有曲线坐标都属于由曲线的素数 q 定义的有限域，即区间 [0, q-1)，并且是格式正确的大整数。这些检查发生在以下代码片段中，该代码片段使用了我们老朋友 BigLessThan 的十个实例。

// Inputs:
//   - pubkey as element of E(Fq)
//   - hash represents two field elements in Fp2, in practice hash = hash_to_field(msg,2).
//   - signature, as element of E2(Fq2)
// Assume signature is not point at infinity
template CoreVerifyPubkeyG1(n, k){
  ...
  var q[50] = get_BLS12_381_prime(n, k);

  component lt[10];
  // check all len k input arrays are correctly formatted bigints < q (BigLessThan calls Num2Bits)
  for(var i=0; i<10; i++){
    lt[i] = BigLessThan(n, k);
    for(var idx=0; idx<k; idx++)
      lt[i].b[idx] <== q[idx];
  }
  for(var idx=0; idx<k; idx++){
    lt[0].a[idx] <== pubkey[0][idx];
    lt[1].a[idx] <== pubkey[1][idx];
    ... // Initializing parameters for rest of the inputs
  }
  ...
}

看起来一切就绪，对吧？其实不然！缺少的一个关键是约束数组 lt 中每个组件的输出信号。回想一下，如果数组 a 表示的整数小于数组 b 表示的整数，则 BigLessThan 的输出信号设置为 1，否则设置为 0。由于上面的 CoreVerifyPubkeyG1 版本不检查 lt 中任何 BigLessThan 组件的输出信号，它可以接受大于曲线素数 q 或格式不正确的输入。在实现签名验证的最外层电路中省略这个关键的数据验证步骤会暴露一个巨大的攻击面。

修复

现在让我们看看如何修复这个问题。幸运的是，细微的问题通常有简单的修复方法。在这种情况下，我们只需要约束 lt 中组件的每个输出信号等于 1。我们的团队提出了以下针对此问题的修复方案，该方案已在 circom-pairing 库中 合并。

template CoreVerifyPubkeyG1(n, k){
  ...
  var q[50] = get_BLS12_381_prime(n, k);

  component lt[10];
  ... // Loops same as before

  var r = 0;
  for(var i=0; i<10; i++){
    r += lt[i].out;
  }
  r === 10;
  ...
}

经验教训

正如 DeFi 历史已经告诉我们的那样，即使是无伤大雅的错误也可能产生重大的安全影响。这段历史已经在 ZK 领域重演，尽管方式更加复杂。开发人员不仅需要确保他们的电路计算出正确的结果，而且还需要确保生成的验证者不会接受比预期更多的输入-输出对。因此，由于 ZK 系统的非传统系统架构，传统的端到端测试技术在这种领域中显得不足。为此，重要的是构建新的分析和验证工具，以帮助开发人员推理此类边缘情况。在 Veridise，我们的程序分析和安全专家团队一直在构建分析工具，以帮助我们发现此类错误。请继续关注我们正在构建的与 ZK 相关的工具的未来博客文章，这些工具可以帮助我们发现关键问题。

致谢

我们要感谢 circom-pairing 的作者 Jonathan Wang、Vincent Huang 和 Yi Sun，以及 Succinct Labs 的 Uma Roy 和 John Guibas，感谢他们在整个审计过程中成为优秀的合作者，并为这篇博文提供了深刻的反馈。

关于 Veridise

Veridise 是一家区块链安全公司，为区块链生态系统的所有层提供审计和软件分析工具，包括智能合约、web3 应用程序、零知识电路和区块链实现。Veridise 由形式化验证和软件安全研究人员团队共同创立，提供最先进的工具来加强区块链安全。我们的客户可以通过多种方式与我们合作，包括聘请我们进行安全审计，使用我们的自动化安全分析工具（用于测试、静态分析、形式化验证）或将两者结合起来。

如果你有兴趣了解更多信息，请考虑在社交媒体上关注我们或访问我们的网站：

网站 | Twitter | Facebook | LinkedIn | Github | 请求审计

• 原文链接： medium.com/veridise/circ...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～