标签，该你了：Circom中的信号标签
Trail of Bits团队持续审查大量使用零知识（ZK）证明的应用。尽管Halo2、Plonky2和Boojum等快速算术化和折叠库日益流行，Circom仍是ZK电路设计的主力。我们曾通过Circomspect（我们的静态分析器）讨论过Circom安全性；本文则将聚焦一个较少被提及的语言特性——信号标签（signal tags），并展示如何用它防范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
|
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
|
template OR() {
signal input a;
signal input b;
signal output out;
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;
}
|
注意逻辑与原始版本完全一致；标签不影响编译后的约束系统。但如果我们现在编译EnforceAuth模板，会得到编译器错误：
1
2
3
4
5
|
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
|
输入标签是前置条件：模板输入必须满足的要求。通过将信号标签附加到输入，开发者表示相应属性必须已被强制执行；模板本身可以假设但不强制执行该条件。
很酷！现在我们如何重写程序以正确使用标签？让我们定义一个新模板，在计算OR值之前正确检查每个值是否为零。
1
2
3
4
5
6
7
8
|
template ToBinary() {
signal input in;
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
|
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
|
template Example {
signal input {binary} in;
signal x <== in;
signal one_minus_x <== 1 - x;
1 === OR()(x, one_minus_x); // 编译器错误
signal not_x <== NOT()(x);
1 === OR()(x, not_x); // 正常
}
|
信号数组的元素具有标签当且仅当所有数组成员都具有该标签。
1
2
3
4
5
6
7
8
9
|
template Example {
signal input {binary} a;
signal input {binary} b;
signal input 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
|
template EnforceMaxBits(n) {
assert(n < 254);
signal input in;
signal output {maxbits} out;
out.maxbits = n;
Num2Bits(n)(in);
out <== in;
}
template AddMaxBits(){
signal input {maxbits} a;
signal input {maxbits} 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;
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
|
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
|
template BinaryConstant(b){
signal output {binary} out;
assert(b == 0 || b == 1);
out <== b;
}
template EnforceBinary(){
signal input in;
signal output {binary} out;
in * (in - 1) === 0;
out <== in;
}
template AssertBinary() {
signal input {binary} in;
}
template ToBinary() {
signal input in;
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;
signal output {binary} out <== a*b;
}
template NOT(){
signal input {binary} in;
signal output {binary} out <== 1 - in;
}
template OR() {
signal input {binary} a;
signal input {binary} b;
signal output {binary} out;
out <== a + b - a*b;
}
|
一旦建立了足够丰富的模板库，开发者很少需要手动在其他地方添加标签。减少手动标签数量使正确性审计更加容易。
高级模板的后置条件可以使用断言模板（如AssertBinary）记录，而无需使用输出标签注释：
1
2
3
4
5
6
7
8
9
10
|
template IsZero() {
signal input in;
signal output out;
signal isNonZero <== ToBinary()(in);
out <== Not()(isNonZero);
AssertBinary()(out);
}
|
规则 #3：显式标签值分配应稀少且有文档记录
大多数标签值应由库函数自动分配，如maxbits示例。每当信号被分配标签值时，附近应有解释性注释。
规则 #4：带值的标签必须始终有值
代码库中的每个标签必须始终有关联值或从无关联值。混合两者可能导致混淆，尤其是在处理信号数组时。
真实世界示例
我们将查看Succinct Labs的Telepathy审查中的两个问题，并解释如何使用Circom标签预防它们。
Telepathy是以太坊同步委员会轻客户端协议的实现，使用Circom编写的zkSNARK加速聚合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
11
12
13
14
15
16
17
18
|
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];
}
}
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标签，指示它们已按基域素数取模。这两个标签一起使用，用于指示期望大整数和约化有限域元素的模板的前置条件，本可以防止最终电路中的三个主要缺失约束。
结论
Circom标签是防止类型混淆、缺失范围检查和其他常见缺失约束导致的错误的强大功能。为了获得该功能的全部好处并对自己负责良好的开发实践，请遵循上述四条简单规则。
标签不是ZK电路安全的完整解决方案。还有许多其他类型的逻辑、算术和集成错误可能危及系统安全。如有任何问题，请随时联系我们，如果您希望我们审查、指定或实现任何ZK电路或协议，请与我们联系。
- BLS签名（Boneh–Lynn–Shacham）和BLS曲线（Barreto-Lynn-Scott）中的“BLS”首字母缩写仅与Ben Lynn重叠，其关于配对的论文是优秀资源。
- 对于任何X，最多有两个对应的Y值，形式为sqrt(X³ + 4)和-sqrt(X³ + 4)。