Circomspect 新增分析通道！ - Trail of Bits 博客
TL;DR: 我们发布了 Circomspect 0.8.0 版本，这是我们为 Circom 设计的静态分析器和 linter。自 2022 年 9 月首次发布以来，我们新增了五个分析通道，支持标签、元组和匿名组件，提供了每个识别问题的详细描述链接，并修复了多个错误。请下载新版本并告诉我们您的想法！
新增分析通道
新增的分析通道（在工具的初始九个基础上）检查 Circom 代码中可能出现的多种问题：
- 未能正确约束中间信号
- 未能约束实例化模板中的输出信号
- 未能将除法操作中的除数约束为非零值
- 将 Circomlib 中特定于 BN254 的模板用于不同曲线
- 未能正确约束 Circomlib 的 LessThan 电路的输入
除了发现下面讨论的与 Circomlib LessThan 电路相关的问题外，这些分析通道还捕获了 Veridise 最近在 circom-pairing 库中发现的“百万美元 ZK 漏洞”。
为了理解 Circomspect 可以识别的问题类型，让我们深入探讨列表中的最后一个示例。该分析通道识别与 Circomlib（Circom 的事实标准库）实现的 LessThan 电路相关的问题。为了完全理解该问题，我们首先需要退一步，了解 Circom 如何表示有符号值。
GF(p) 中的有符号算术
Circom 程序操作称为信号的变量，这些变量表示有限域 GF(p) 中的元素，其中 p 是一个素数。通常，GF(p) 中的元素与半开区间 [0, p) 中的无符号整数相对应。然而，有时使用域元素表示有符号量是很方便的，就像我们使用 [0, 2^32) 中的元素表示有符号 32 位整数一样。为了反映用于表示有符号整数值的二进制补码定义，我们定义 val(x) 如下：
然后，如果 val(a) < val(b) 作为有符号整数，我们说在 GF(p) 中 a 小于 b。这意味着 q = floor(p/2) 是 GF(p) 中可表示的最大有符号值，而 -q = q + 1 是 GF(p) 中可表示的最小有符号值。这也意味着，可能有些令人惊讶的是，q + 1 实际上小于 q。这也是 Circom 编译器实现比较运算符 < 的方式。
通常，如果 a > 0，我们说 a 是正数；如果 a < 0，我们说 a 是负数。确保值 a 非负的一种方法是限制 a 的二进制表示的大小（以位为单位）。特别是，如果 a 的大小严格小于 log(p) - 1 位，那么 a 必须小于或等于 q，因此是非负的。
Circomlib 的 ‘LessThan’ 模板
有了这些背景，让我们将注意力转向 Circomlib 定义的 LessThan 模板。该模板可用于约束两个输入信号 a 和 b，以确保 a < b，其实现如下：
查看实现，我们看到它接受一个输入参数 n 和两个输入信号 in[0] 和 in[1]，并定义一个输出信号 out。此外，该模板使用 Circomlib 的 Num2Bits 模板来约束输出信号 out。
Circomlib 的 Num2Bits 模板接受单个参数 n，可用于将域元素转换为其 n 位二进制表示，由大小为 n 的数组 out 给出。由于二进制表示的大小受参数 n 的限制，Num2Bits 的输入也隐式约束为 n 位。在上面的 LessThan 实现中，表达式 (1 « n) + in[0] - in[1] 作为输入传递给 Num2Bits，这将绝对值 |in[0] - in[1]| 约束为 n 位。
为了理解 LessThan 模板实现的微妙之处，让我们首先考虑预期用例，即 LessThan 的两个输入最多为 n 位，其中 n 足够小以确保两个输入都是非负的。
我们有两种情况需要考虑。如果 in[0] < in[1]，那么 in[0] - in[1] 是一个负的 n 位值，而 (1 « n) + in[0] - in[1] 是一个正的 n 位值。因此，Num2Bits 输入的二进制表示中的第 n 位是 0，因此 out 必须等于 1 - 0 = 1。
另一方面，如果 in[0] ≥ in[1]，那么 in[0] - in[1] 是一个非负的 n 位值（因为两个输入都是正的），而 (1 « n) + in[0] - in[1] 是一个正的 (n + 1) 位值，最高位等于 1。因此，Num2Bits 输入的二进制表示中的第 n 位是 1，out 必须由 1 - 1 = 0 给出。
这一切都很有道理，如果我们想在自己的电路中使用 LessThan 进行范围证明，这会给我们一些信心。然而，如果我们忘记约束传递给 LessThan 的输入的大小，事情就会变得复杂。
使用信号表示无符号量
为了描述可能影响使用 LessThan 定义的电路的第一类问题，考虑信号用于表示无符号值（如货币金额）的情况。假设我们想允许用户从我们的系统中提取资金，而不泄露敏感信息，如单个用户的总余额或用户提取的金额。我们可以使用 LessThan 来实现电路的部分，验证提取金额是否小于总余额，如下所示：
ValidateWithdrawal 模板应确保用户不能提取超过其总余额的金额。
现在，假设一个恶意用户的余额为零，决定从系统中提取 p - 1 个代币，其中 p 是底层素域的大小。显然，这不应该被允许，因为 p - 1 是一个荒谬的大数，而且无论如何，该用户没有可用的代币用于提取。然而，查看 LessThan 的实现，我们看到在这种情况下，Num2Bits 的输入将由 (1 « 64) + (p - 1) - (0 + 1) = (1 « 64) - 2（所有算术都是模 p 完成的）给出。因此，输入二进制表示的第 64 位将是 0，LessThan 的输出将是 1 - n2b.out[64] = 1 - 0 = 1。这也意味着 ValidateWithdrawal 将识别提取为有效。
这里的问题是 p - 1 也代表 GF(p) 中的有符号量 –1。显然，-1 小于 1，并且我们没有约束提取金额为非负。添加一个约束，限制金额的大小小于 log(p) - 1 位，将确保金额必须是正的，从而防止这个问题。
更一般地说，由于 LessThan 的输入参数 n 仅限制差值 |in[0] - in[1]| 的大小，我们通常不能使用 LessThan 来防止溢出和下溢。这是一个许多开发人员忽略的微妙点。例如，考虑 0xPARC 维护的零知识（ZK）漏洞跟踪器中关于算术溢出和下溢的部分。在早期版本中，0xPARC 建议使用 LessThan 来约束相关信号，在一个几乎与上面定义的有漏洞的 ValidateWithdrawal 模板相同的示例中！
Daira Hopwood 在早期版本的 ZK 太空征服游戏 Dark Forest 中发现了另一种此类漏洞。这里，漏洞允许用户在游戏场地之外殖民行星。开发人员通过添加基于 Num2Bits 模板的范围证明来解决该问题，将坐标的大小限制为 31 位。
使用信号表示有符号量
现在，假设信号用于表示有符号量。特别是，让我们考虑如果将 q = floor(p/2) 和 q + 1 作为输入传递给 LessThan 会发生什么。我们将证明，尽管根据 Circom 编译器 q + 1 < q，但根据 LessThan，q 实际上小于 q + 1。回到 LessThan 定义中 Num2Bits 的输入，我们看到如果 in[0] = q 且 in[1] = q + 1，Num2Bits 的输入由以下表达式给出：
(1 « n) + in[0] - in[1] = (1 « n) + q - (q + 1) = (1 « n) - 1
因此，该值的二进制表示中的第 n 位是 0，LessThan 的输出是 1 - n2b.out[n] = 1 - 0 = 1。因此，根据 LessThan，q < q + 1，尽管根据编译器 q + 1 < q！
这里值得重申的是，LessThan 的输入参数 n 不限制输入的大小，只限制它们的差的绝对值。因此，我们可以自由地将非常大（或非常小）的输入传递给 LessThan。同样，如果 LessThan 模板的两个输入的大小都限制为小于 log(p) - 1 位，则可以防止此问题。
Circomspect 来救援（第一部分）
为了找到此类问题，Circomspect 识别使用 LessThan 的位置。然后，它尝试查看 LessThan 的输入是否使用 Circomlib 的 Num2Bits 模板约束为小于 log(p) - 1 位，如果没有找到此类约束，则发出警告。这允许开发人员（或审查员）快速识别代码库中需要进一步审查的位置。
最新版本的 Circomspect 在上面定义的 ValidateWithdrawal 模板上运行的输出。
如上图所示，Circomspect 的每个警告现在通常还包含一个指向潜在问题描述的链接，以及如何解决它的建议。
Circomspect 来救援（第二部分）
我们还想提到我们的另一个新分析通道。最新版本的 Circomspect 识别模板被实例化但模板定义的输出信号未被约束的位置。
例如，考虑上面介绍的 ValidateWithdrawal 模板。假设我们重写模板以包括输入信号 amount 和 total 的范围证明。然而，在重写过程中，我们意外地忘记包括确保 LessThan 输出为 1 的约束。这意味着用户可能能够提取大于其总余额的金额，这显然是一个严重的漏洞！
我们重写 ValidateWithdrawal 以包括两个输入 amount 和 total 的范围证明，但意外地忘记约束输出信号 lt.out 为 1！
有一些示例（如 Num2Bits），其中模板约束其输入，不需要对输出进行进一步约束。然而，忘记约束模板的输出通常表示错误，需要进一步审查以确定是否构成漏洞。Circomspect 将标记输出信号未被约束的位置，以确保每个位置都可以手动检查正确性。
如果 Circomspect 发现模板定义的输出信号未被正确约束，它现在会生成警告。
让我们谈谈！
Trail of Bits 对为过去几年出现的 ZK 工具和库的不断增长范围做出贡献感到兴奋。如果您正在使用 ZK 构建项目，我们很乐意与您交谈，看看我们是否能以任何方式提供帮助。如果您有兴趣让我们审查您的代码，或者如果您想将部分开发外包给可信的第三方，请与我们经验丰富的密码学家团队联系。
如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News
页面内容 新增分析通道 GF(p) 中的有符号算术 Circomlib 的 ‘LessThan’ 模板 使用信号表示无符号量 使用信号表示有符号量 Circomspect 来救援（第一部分） Circomspect 来救援（第二部分） 让我们谈谈！ 最近的帖子 构建安全消息传递很难：对 Bitchat 安全辩论的 nuanced 看法 使用 Deptective 调查您的依赖项 系好安全带，Buttercup，AIxCC 的评分回合正在进行中！ 使您的智能合约超越私钥风险 Go 解析器中意外的安全陷阱 © 2025 Trail of Bits。 使用 Hugo 和 Mainroad 主题生成。