标记，该你了：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编写的zkSNARK加速聚合BLS签名验证。ETH2.0轻客户端和BLS聚合的确切细节不是理解错误所必需的，但椭圆曲线复习和Circom中大整数算术的一些注释将有用。
ETH2.0轻客户端协议使用BLS12-381曲线上的聚合BLS签名1。公钥是BLS12-381曲线上的点(X, Y)，其中Y2 = X3 + 4 mod Q，其中Q是381位素数。注意BLS公钥的坐标是381位，而Circom信号最多只能表示254位。为了表示单个公钥坐标，circom-pairing使用七个Circom信号（称为"limbs"），每个持有55位值。为了确保大整数表示唯一并防止算术运算期间溢出，开发者必须确保每个limb的值小于2^55。
以太坊块包含压缩形式的同步委员会公钥承诺，意味着密钥存储为X坐标加一个额外位指示Y的符号2。为了与曲线点执行算术运算，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个limbs中的每一个都小于2^n。但此检查从未强制执行，导致中间计算中的不受控制溢出。利用此漏洞，恶意证明者可能导致协议陷入不可恢复状态，冻结轻客户端和任何依赖持续操作的桥接资金。
使用信号标签本可以防止此错误（TOB-SUCCINCT-1）和我们在审查期间发现的另外两个错误（TOB-SUCCINCT-2，TOB-SUCCINCT-14）。正确形成的大整数值应具有maxbits标签，其值对应于limbs的大小（在这种情况下为55）。BLS12-381坐标应额外具有fp标签，指示它们对基域素数取模。这两个标签一起用于指示期望大整数和约化有限域元素的模板的前置条件，本可以防止最终电路中的三个主要缺失约束。
结论
Circom标签是防止类型混淆、缺失范围检查和其他常见缺失约束导致的错误的强大特性。为了获得特性的全部好处并对自己负责良好的开发实践，请遵循上述四个简单规则。
标签不是ZK电路安全的完整解决方案。还有许多其他类型的逻辑、算术和集成错误可能危及系统安全。如有任何问题，请随时联系我们，如果您