Tag, you’re it: Circom中的信号标签
Trail of Bits团队为大量使用零知识（ZK）证明的应用程序执行安全审查。虽然Halo2、Plonky2和Boojum等快速新算术化和折叠库正迅速获得采用，但Circom仍然是ZK电路设计的主力。我们之前曾在Circomspect（我们的linter和静态分析器）的背景下写过关于Circom安全性的文章；在这篇文章中，我们将探讨另一种使用一种较不为人知的语言特性（称为信号标签）来防范Circom电路中的错误的方法。我们提出了四个简单的规则，将信号标签纳入您的开发过程，这将有助于保护您免受常见错误的影响，并促进代码库的审计。
本文假设对Circom语言有一定熟悉度。我们将研究一些简单的Circom程序，并演示如何使用信号标签来检测和防止常见类别的错误；我们还将指出信号标签特性的潜在陷阱和弱点。
警告： 在本文的剩余部分，我们将使用Circom 2.1.6。标签传播的细节自2.1.0以来已经改变——我们强烈建议使用版本2.1.6或更高版本，因为早期版本包含本文未提及的严重陷阱。
什么是信号标签？
信号标签是Circom 2.1.0中引入的一个特性，允许开发者在编译时指定和执行模板上的临时前置条件和后置条件。Circom标签帮助开发者确保模板的输入始终满足模板的要求，防范健全性错误，同时减少约束的重复。
以下是CircomLib中布尔OR门的实现：
1
2
3
4
5
6
7
|
template OR() {
signal input {binary} a;
signal input {binary} b;
signal output {binary} out;
out <== a + b - a*b;
}
|
假设我们正在编写一个ZK电路，要求每当两个值（例如，传出值转移）中的任何一个非零时，都需要认证证明。工程师可能会编写这个模板来强制执行认证要求。
1
2
3
4
5
6
7
8
9
|
// 每当传出值非零时，要求 `authSucceeded` 为 `1`
template EnforceAuth() {
signal input valueA;
signal input valueB;
signal input authSucceeded;
signal authRequired <== OR()(valueA, valueB);
(1 - authSucceeded) * authRequired === 0;
}
|
当用随机或典型值测试时，这个模板似乎行为正确；只有当 authSucceeded 为1时，才允许 valueA 和 valueB 的非零值。
但是，当 valueA == valueB == 2 时呢？注意 authRequired 将为零，因此 EnforceAuth 的所需不变量将被违反。
那么哪里出了问题？OR模板有一个隐含的前置条件，即 a 和 b 都是二进制的——也就是说，在集合 {0,1} 中。违反这个条件会导致意外行为。
解决这个问题的一种方法是为OR门添加约束，要求输入是二进制的：
1
2
3
4
5
6
7
8
9
10
11
|
template OR() {
signal input a;
signal input b;
signal output out;
// 约束a和b为二进制
a * (1 - a) === 0;
b * (1 - b) === 0;
out <== a + b - a*b;
}
|
这种方法的问题在于，我们刚刚使每个OR门所需的约束数量增加了两倍。通常输入已经在电路的前面被约束过，这使得这些约束纯粹是冗余的，并毫无必要地增加了编译和证明时间。
在许多语言中，输入约束会表示为类型。与Halo2等更灵活的API驱动框架不同，Circom不支持表达性类型；所有信号可以携带0到P之间的任何值。然而，Circom 2.1.0及更高版本确实支持信号标签，可以用作一种临时类型系统。
让我们看看使用信号标签的OR模板会是什么样子：
1
2
3
4
5
6
7
|
template OR() {
signal input {binary} a;
signal input {binary} b;
signal output {binary} out;
out <== a + b - a*b;
}
|
注意逻辑与原始版本完全 unchanged；标签完全不影响编译后的约束系统。然而，如果我们现在尝试编译 EnforceAuth 模板，我们会得到一个编译器错误：
1
2
3
4
5
6
7
|
error[T3001]: Invalid assignment: missing tags required by input signal.
Missing tag: binary
┌─ "example1.circom":18:26
│
18 │ signal authRequired <== OR()(valueA, valueB); │ ^^^^^^^^^^^^^^^^^^^^ found here │ = call trace: ->EnforceAuth
previous errors were found
|
输入标签是前置条件：模板输入必须满足的要求。通过将信号标签附加到输入，开发者表示相应的属性必须已经被强制执行；模板本身可以假设但不强制执行该条件。
很酷！现在我们如何重写程序以正确使用标签？让我们定义一个新的模板，在计算OR值之前正确检查每个值是否为零。
1
2
3
4
5
6
7
8
9
10
11
12
13
|
// 当 `in` 非零时，`out` 为1，否则为0
template ToBinary() {
signal input in;
// 后置条件：out是0或1
// 证明：
// in != 0 => out == 1 (通过约束(2))
// in == 0 => out == 0 (通过约束(1))
signal output {binary} out;
signal inv <-- in!=0 ? 1/in : 0;
out <== in*inv;
in*(1 - out) === 0;
}
|
这本质上是CircomLib IsZero模板的否定，对输入进行归一化并向输出添加二进制标签。注意 binary 只是一个任意字符串——Circom不知道我们打算让 binary 具有的语义，特别是不会检查 out 是否在集合 {0,1} 中。Circom只是将不透明的标签 binary 附加到IsZero的输出线上。
输出标签是后置条件：开发者向下游信号用户做出的承诺。
注意，由于Circom不为我们检查后置条件，我们必须非常小心，不要意外地将标签分配给可能携带超出标签允许值的信号。为了跟踪信号被分配标签的所有可能方式，我们建议在任何带有标签的模板输出上方包含注释，解释后置条件满足的原因。
现在我们可以将其插入到我们的 EnforceAuth 电路中，一切编译通过！
1
2
3
4
5
6
7
8
9
10
11
12
|
// 每当传出值非零时，要求 `authSucceeded` 为 `1`
template EnforceAuth() {
signal input valueA;
signal input valueB;
signal input authSucceeded;
signal spendsA <== ToBinary()(valueA);
signal spendsB <== ToBinary()(valueB);
signal authRequired <== OR()(spendsA, spendsB);
(1 - authSucceeded) * authRequired === 0;
}
|
在底层，Circom正在传播附加到 ToBinary 输出信号的标签，因此 spendsA 也具有该标签。然后当OR检查其输入具有 binary 标签时，它得到满足。
标签传播
标签通过直接赋值传播，但不通过算术运算传播。在以下示例中，信号 x 从 in 获取 binary 标签。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
template Example {
signal input {binary} in;
// x 获取 `binary` 标签
signal x <== in;
// one_minus_x 没有 `binary` 标签；
signal one_minus_x <== 1 - x;
// 编译器错误
1 === OR()(x, one_minus_x);
// 假设NOT定义为返回二进制输出，如OR。
signal not_x <== NOT()(x);
// 那么这是OK的
1 === OR()(x, not_x);
}
|
信号数组的元素具有标签当且仅当所有数组成员都具有该标签。
1
2
3
4
5
6
7
8
9
10
11
|
template Example {
signal input {binary} a;
signal input {binary} b;
signal input c;
// xs 没有标签 `binary`，因为 `c` 没有该标签
signal xs[3] <== [a, b, c];
// 错误：缺少标签
1 === OR()(xs[0], xs[1]);
}
|
带值的标签
零知识电路中健全性错误的一个常见来源是算术运算意外溢出有限域模数。Circom中的信号标签也可以携带值，这些是编译时变量，随标签一起传播。使用带值的标签，我们可以在编译时确保操作永远不会溢出。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
template EnforceMaxBits(n) {
assert(n < 254); // 有限域中的位数
signal input in;
// 原因：Num2Bits约束in可由 `n` 位表示
signal output {maxbits} out;
out.maxbits = n;
Num2Bits(n)(in);
out <== in;
}
// 添加两个数字，确保结果不溢出
template AddMaxBits(){
signal input {maxbits} a;
signal input {maxbits} b;
// 原因：log(a + b) <= log(2*max(a, b)) = 1 + max(log(a), log(b))
signal output {maxbits} c;
c.maxbits = max(a.maxbits, b.maxbits) + 1
assert(c.maxbits < 254);
c <== a + b;
}
// 乘两个数字，确保结果不溢出
template MulMaxBits(){
signal input {maxbits} a;
signal input {maxbits} b;
// 原因：log(a * b) = log(a) + log(b)
signal output {maxbits} c;
c.maxbits = a.maxbits + b.maxbits;
assert(c.maxbits < 254);
c <== a * b;
}
|
标签值必须在信号赋值之前分配。如果标签值通过信号赋值传播到已经具有不同标签值的信号，Circom将抛出错误。
避免不正确的标签分配
虽然信号标签可以帮助防止编程错误，但语言特性语法很容易允许意外或无保证地向信号添加标签。错误地将标签分配给未被约束遵守标签规则的信号会破坏标签系统的保证，并很容易导致严重的安全问题。为了获得信号标签的全部好处，我们建议严格遵守这些使用规则。
规则 #1：输出和内部标签注释必须附有解释性注释
我们之前提到，向输出信号添加标签注释是危险的。内部信号也可以用标签注释声明，这会无条件地向信号添加标签。例如，这个对原始 EnforceAuth 程序的不安全修改使用了带标签的内部信号：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
// 每当传出值非零时，要求 `authSucceeded` 为 `1`
template EnforceAuth() {
signal input valueA;
signal input valueB;
signal input authSucceeded;
// 这些信号获取 `binary` 标签
// _没有_ 任何检查值实际上是二进制的
// 这是不安全的
signal {binary} spendsA <== valueA;
signal {binary} spendsB <== valueB;
signal authRequired <== OR()(valueA, valueB);
(1 - authSucceeded) * authRequired === 0;
}
|
我们强烈建议尽可能避免手动标记的内部和输出信号。任何输出或内部信号标签注释必须附有注释，解释为什么标签要求得到满足。
规则 #2：标签应使用专用库模板添加到信号
为了最小化高级代码中手动信号标签注释的使用，我们建议提供一个助手模板库，包含使用标签的安全API。以下代码示例了一个用于二进制值的库，其中包含构造函数和类型安全操作符。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
// binary.circom
// 标签：
// binary: 信号必须是0或1
// 从常量0或1创建二进制值
template BinaryConstant(b){
// 原因：编译时只允许有效值
signal output {binary} out;
assert(b == 0 || b == 1);
out <== b;
}
// 约束信号为二进制并返回带标签的输出
template EnforceBinary(){
signal input in;
// 原因：只有x*(x-1) = 0的解是0和1
signal output {binary} out;
in * (in - 1) === 0;
out <== in;
}
// 空模板仅断言输入被标记
// 用于检查/记录输出信号上的后置条件
template AssertBinary() {
signal input {binary} in;
}
// 当输入为“真”（非零）时返回1，当输入为零时返回0
template ToBinary() {
signal input in;
// 原因：
// in != 0 => out == 1 (通过约束(2))
// in == 0 => out == 0 (通过约束(1))
signal output {binary} out;
signal inv <-- in!=0 ? 1/in : 0;
out <== in*inv;
in*(1 - out) === 0;
}
template AND(){
signal input {binary} a;
signal input {binary} b;
// 原因：1*1 = 1, 1*0 = 0, 0*1 = 0, 0*0 = 0
signal output {binary} out <== a*b;
}
template NOT(){
signal input {binary} in;
// 原因：1 - 0 = 1, 1 - 1 = 0
signal output {binary} out <== 1 - in;
}
template OR() {
signal input {binary} a;
signal input {binary} b;
// 原因：a = 0 => out = b - 0*b = b, a = 1 => out = 1 + b - 1*b = 1
signal output {binary} out;
out <== a + b - a*b;
}
|
一旦建立了足够丰富的模板库，开发者很少需要手动在其他地方添加标签。减少手动标签的数量使得审计正确性容易得多。
高级模板的后置条件可以使用断言模板（如 AssertBinary）来记录，而不使用输出标签注释：
1
2
3
4
5
6
7
8
9
10
11
|
template IsZero() {
signal input in;
// 后置条件：out具有 `binary` 标签
signal output out; // 避免这里使用有风险的输出标签注释
signal isNonZero <== ToBinary()(in); // 避免这里使用有风险的内部标签注释
out <== Not()(isNonZero);
AssertBinary()(out); // 无运行时成本地记录和检查后置条件
}
|
规则 #3：显式标签值分配应稀少且有文档记录
大多数标签值应由库函数自动分配，如 maxbits 示例。每当信号被分配标签值时，附近应有解释性注释。
规则 #4：带值的标签必须始终有值
代码库中的每个标签必须要么始终有关联值，要么从未有关联值。混合两者可能导致混淆，尤其是在处理信号数组时。
一个真实世界的例子
我们将查看我们对Succinct Labs的Telepathy的审查中的两个问题，并解释如何使用Circom标签来防止它们。
Telepathy是以太坊同步委员会轻客户端协议的实现，使用用Circom编写的zkSNARKs来加速聚合BLS签名的验证。ETH2.0轻客户端和BLS聚合的确切细节不需要理解错误，但关于椭圆曲线的复习和一些关于Circom中大整数算术的注释将是有用的。
ETH2.0轻客户端协议使用在BLS12-381曲线上的聚合BLS签名。公钥是BLS12-381曲线上的点 (X, Y)，其中 Y² = X³ + 4 mod Q，其中Q是一个381位素数。注意BLS公钥的坐标是381位，而Circom信号最多只能表示254位。为了表示单个公钥坐标，circom-pairing使用七个Circom信号（称为“肢体”），每个持有55位值。为了确保大整数的表示是唯一的，并防止算术运算期间溢出，开发者必须确保每个肢体的值小于2⁵⁵。
以太坊块包含对同步委员会公钥的压缩形式承诺，意味着密钥存储为X坐标加上一个额外位以指示Y的符号。为了执行曲线点的算术运算，Telepathy电路要求证明者提供与公钥X坐标对应的Y坐标。然后通过 SubgroupCheckG1WithValidX 模板验证该Y值，该模板强制执行曲线方程成立。
1
2
3
4
5
6
7
8
9
10
|
/* 验证见证的Y坐标使公钥位于曲线上 */
component isValidPoint[SYNC_COMMITTEE_SIZE];
for (var i = 0; i < SYNC_COMMITTEE_SIZE; i++) {
isValidPoint[i] = SubgroupCheckG1WithValidX(N, K);
for (var j = 0; j < K; j++) {
isValidPoint[i].in[0][j] <== pubkeysBigIntX[i][j];
isValidPoint[i].in[1][j] <== pubkeysBigIntY[i][j];
}
}
|
1
2
3
4
5
6
7
8
9
|
template SubgroupCheckG1WithValidX(n, k){
signal input in[2][k];
var p[50] = get_BLS12_381_prime(n, k);
var x_abs = get_BLS12_381_parameter();
var b = 4;
component is_on_curve = PointOnCurve(n, k, 0, b, p);
for(var i=0; i<2; i++)for(var idx=0; idx<k; idx++)
is_on_curve.in[i][idx] <== in[i][idx];
}
|
然而，PointOnCurve 假设输入是正确格式化的大整数——特别是Y的k个肢体中的每一个都小于2ⁿ。但这个检查从未强制执行，导致中间计算中的不受控制溢出。利用此漏洞，恶意证明者可以使协议陷入不可恢复的状态，冻结轻客户端和任何依赖持续操作的桥接资金。
使用信号标签本可以防止这个错误（TOB-SUCCINCT-1）和我们在审查期间发现的另外两个错误（TOB-SUCCINCT-2，TOB-SUCCINCT-14）。正确形成的大整数值应具有 maxbits 标签，其值对应于肢体的大小（在这种情况下为55）。BLS12-381坐标应额外具有 `fp