Circomspect 新增分析通道！ - Trail of Bits 博客

TL;DR：我们发布了 Circomspect 0.8.0 版本（Circom 静态分析器和林特工具）。自 2022 年 9 月首次发布以来，新增了五项分析通道，支持标签、元组和匿名组件，为每个识别问题添加深度描述链接，并修复了若干漏洞。请下载新版并反馈意见！

新增分析通道

新增的五项分析通道（初始九项基础上）可检测 Circom 代码中多类问题：

未正确约束中间信号
实例化模板中未约束输出信号
除法操作中未约束除数非零
在非 BN254 曲线上误用 Circomlib 的曲线特定模板
未正确约束 Circomlib 的 LessThan 电路输入

除下述 LessThan 电路问题外，这些分析还能捕获 Veridise 在 circom-pairing 库中发现的“百万美元 ZK 漏洞”。

深入理解 LessThan 电路问题

以列表末项为例，该分析通道识别与 Circom 事实标准库 Circomlib 的 LessThan 电路相关的问题。需先理解 Circom 中签名数值的表示机制。

GF(p) 中的签名算术

Circom 程序操作称为信号的变量，表示素数 p 模整数有限域 GF(p) 中的元素。通常用半开区间 [0, p) 中的无符号整数识别 GF(p) 元素，但有时需用域元素表示签名数值（类似用 [0, 2³²) 元素表示签名 32 位整数）。仿照双补码定义，设 val(x) 为：

[ \text{val}(x) = \begin{cases} x & \text{if } x \leq \lfloor p/2 \rfloor \ x - p & \text{if } x > \lfloor p/2 \rfloor \end{cases} ]

当 val(a) < val(b)（作为签名整数）时，称 a 在 GF(p) 中小于 b。这意味着 q = floor(p/2) 是 GF(p) 中可表示的最大签名值，-q = q + 1 是最小签名值，且 q + 1 实际小于 q（符合编译器对 < 的实现）。

若 a 的二进制表示位数严格小于 log(p) - 1，则 a ≤ q 即非负。

Circomlib 的 LessThan 模板

该模板约束两个输入信号 a 和 b 确保 a < b，实现如下：

1
2
3
4
5
6
7


template LessThan(n) {
    signal input in[2];
    signal output out;
    component n2b = Num2Bits(n+1);
    n2b.in <== (1 << n) + in[0] - in[1];
    out <== 1 - n2b.out[n];
}

使用 Circomlib 的 Num2Bits 模板（参数 n）将域元素转换为 n 位二进制表示（数组 out 大小为 n）。输入被隐式约束为 n 位。LessThan 中表达式 (1 << n) + in[0] - in[1] 作为 Num2Bits 输入，约束绝对值 |in[0] - in[1]| 为 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）。第 n 位为 1，out = 1 - 1 = 0。

未约束输入大小的问题

场景1：信号表示无符号值（如金额） 考虑以下提现验证模板：

1
2
3
4
5
6
7
8


template ValidateWithdrawal() {
    signal input total;
    signal input amount;
    component lt = LessThan(64);
    lt.in[0] <== amount + 1;
    lt.in[1] <== total + 1;
    // 注意：未约束 lt.out 必须为 1！
}

恶意用户余额为 0 时尝试提取 p - 1 代币（p 为域大小）。此时 Num2Bits 输入为： (1 << 64) + (p - 1) - 1 = (1 << 64) - 2 (模 p) 第 64 位为 0，LessThan 输出 1，验证通过。因 p - 1 代表签名值 -1（小于 1），且未约束提现金额非负。添加位数小于 log(p) - 1 的约束可防止此问题。

LessThan 的参数 n 仅约束差值 |in[0] - in[1]| 的大小，不能防止溢出/下溢（如 0xPARC ZK 漏洞追踪器曾错误建议使用 LessThan 约束信号）。

类似漏洞曾由 Daira Hopwood 在太空征服游戏 Dark Forest 早期版本中发现（用户殖民游戏区域外行星），开发者通过添加基于 Num2Bits 的 31 位坐标范围证明修复。

场景2：信号表示签名值 设输入为 q = floor(p/2) 和 q + 1。依编译器 q + 1 < q，但 LessThan 判断 q < q + 1： Num2Bits 输入为 (1 << n) + q - (q + 1) = (1 << n) - 1 第 n 位为 0，输出 1。再次强调需约束输入位数小于 log(p) - 1。

Circomspect 解决方案（第一部分）

Circomspect 定位 LessThan 使用点，检查输入是否通过 Circomlib 的 Num2Bits 约束至小于 log(p) - 1 位，否则发出警告。新版警告包含问题描述链接和修复建议。

Circomspect 解决方案（第二部分）

新增分析通道识别实例化模板后未约束输出信号的位置。例如重写 ValidateWithdrawal 包含金额和总额的范围证明，但遗漏约束 lt.out 为 1：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13


template ValidateWithdrawal() {
    signal input total;
    signal input amount;
    // 添加范围证明
    component rangeProofAmount = Num2Bits(64);
    rangeProofAmount.in <== amount;
    component rangeProofTotal = Num2Bits(64);
    rangeProofTotal.in <== total;
    component lt = LessThan(64);
    lt.in[0] <== amount + 1;
    lt.in[1] <== total + 1;
    // 漏洞：未约束 lt.out == 1
}

虽存在模板（如 Num2Bits）约束输入而无需额外约束输出，但未约束输出通常需人工审查是否构成漏洞。Circomspect 将标记未约束输出信号的位置。

联系我们

Trail of Bits 兴奋能为近年涌现的 ZK 工具生态贡献力量。如果您正在开发 ZK 项目，我们期待交流并提供支持。如需代码审计或委托开发，请联系我们的密码学专家团队。

（原文结束）

Circomspect 新增五大分析通道，强化 Circom 静态代码审计

本文深度解析 Circomspect 0.8.0 版本新增的五项静态分析功能，重点剖析 Circomlib 的 LessThan 电路约束漏洞、签名数值表示风险及输出信号未约束问题，包含实际代码案例和漏洞原理的数学证明。