技术解析Circom-Pairing库核心零知识电路安全漏洞

我们将在本文深入剖析 Veridise 在 circom-pairing 库中发现的一个关键安全漏洞。circom-pairing 库是在业界有着广泛用途的 BLS12-381 椭圆曲线在 Circom 语言上的一个实现：零知识（Zero-Knowledge，ZK）证明系统依赖 circom-pairing 库实现对 BLS12-381 椭圆曲线（elliptic curve）上的签名（signature）的验证。在近期对于 Succinct Labs 的零知识协议进行的安全审计中，Veridise 团队截获了数个存在于 circom-pairing 库的问题。由于该库支撑了 Succinct Labs 的跨链桥（bridge）方案设计，这使得其中最严重的漏洞能被攻击者利用从而实现签名伪造。

想了解更多细节？ 前排出售瓜子汽水，坐稳扶好！起飞之前先简单看一下 circom-pairing 库的背景。

Circom-Pairing 库：基于配对的密码学算法的零知识实现

适用于零知识证明的编程语言诸如 Circom 可以将程序的计算逻辑编码成约束（constraints），编译器进而将约束编译为两个零知识证明组件：prover 和 verifier。这两个组件可以被用来验证计算逻辑的正确性。其中，基于满足上述约束的输入 – 输出对（input-output pairs），prover 可以用于生成对应的证明（proofs）：比如在 circom-pairing 中，prover 可以用来生成给定公钥的 BLS12-381 签名有效性的证明。而 verifier 组件则可以在不运行（且不知晓）目标计算逻辑的情况下，验证一个给定证明的有效性。并且，由于证明生成的时间取决于约束的规模，多数零知识系统还需要优化以减少 verifier 需要验证的约束的数量。说到这儿，你大概会觉得在 Circom 中实现基于配对的密码学算法（cryptographic pairing algorithms）是一项多么艰巨的任务——对，就是这样。

整数位数不足

实现 BLS12-381 配对算法的首个难点就来自曲线命名中的「381」：381 描述了曲线上表示整数对 (x,y) 所需要的位数（bits），但是现今 Circom 体系中证明的验证只支持 254 位表示的整数。为了绕过这个限制，circom-pairing 的作者需要创建一个支持任意位数整数（简称大整数，bigint）的表示和运算的库。其中，每个库函数及其运算都基于用 k 个寄存器表示的 n 位整数。举个例子，下述代码是一个比较函数（模板）BigLessThan 的整数表示的声明部分：

/*

Inputs:

-BigInts a, b

Output:

-out = (a < b) ? 1 : 0

*/

template BigLessThan(n, k){

signal input a[k];

signal input b[k];

signal output out;

…

}

如果 a 表示的大整数小于 b 表示的大整数，则输出信号（output signal）out 必须被设置为 1，否则为 0（译注：由于 BigLessThan 被用于生成约束而不是计算结果，因此其正确的调用方式中用户必须显式指定 out 的取值：0 或者 1）。circom-pairing 确保了 BigLessThan 中的 a 和 b 都能以大整数的方式表示（k 个寄存器表示 n 位整数）并参与运算，从而克服了原先 254 位的限制。

大规模约束

实现 circom-pairing 的另一个难点就是验证 BLS12-381 所需要的百万级别的约束规模——整个零知识系统中如此量级的约束对于开发者的优化提出了巨大的挑战，而 circom-pairing 中的一个设计决策成为了降低约束数量的关键，即：略过核心功能函数（模板）中的数据验证。比如，circom-pairing 中的一些核心电路（circuits）均假设其输入信号使用了正确的大整数表示并且落在特定范围内。因此，使用这些电路的时候，用户需要额外对其输入进行手动约束（数据验证），例如使用前述的 BigLessThan 函数（模板）。然而，接下来我们将挖掘这个设计所带来的更多安全问题。

信号都约束妥当了吗？仔细再查！

深挖漏洞

我们截获的一个关键漏洞是源于一个叫做 CoreVerifyPubkeyG1 的电路。顾名思义，这是一个用来验证公钥签名的关键电路，因此，在进行实际的签名验证之前，开发者必须确保 CoreVerifyPubkeyG1 的所有的输入数据都满足特定的假设（没错！为了优化约束规模，CoreVerifyPubkeyG1 需要用户手动添加输入约束）。这其中最重要的假设就是：所有曲线上的坐标点都被表示为大整数，并且属于由曲线的质数 q 所定义的有限域（finite field）当中，即[0, q-1) 所表示的整数区间。这些约束由下面的代码片段实现（包含了 10 次我们之前介绍的 BigLessThan 的调用）：

// Inputs:

// - pubkey as element of E(Fq)

// - hash represents two field elements in Fp2, in practice hash = hash_to_field(msg,2).

// - signature, as element of E2(Fq2)

// Assume signature is not point at infinity

template CoreVerifyPubkeyG1(n, k){

…

var q[50] = get_BLS12_381_prime(n, k);

component lt[10];

// check all len k input arrays are correctly formatted bigints < q (BigLessThan calls Num2Bits)

for(var i=0; i<10; i++){

lt[i] = BigLessThan(n, k);

for(var idx=0; idx<k; idx++)

lt[i].b[idx] <== q[idx];

}

for(var idx=0; idx<k; idx++){

lt[0].a[idx] <== pubkey[0][idx];

lt[1].a[idx] <== pubkey[1][idx];

… // Initializing parameters for rest of the inputs

}

…

}

看起来好像没啥问题，对吧？其实不然！关键问题就在于数组 lt 的所有输出信号都缺少约束。lt 是 BigLessThan 的实例化。如前文所述，BigLessThan 中如果 a 小于 b，则其输出信号必须被手动设置为 1，否则为 0。由于这里的 CoreVerifyPubkeyG1 并没有检查（设置）lt 的输出信号（译注：也就是说，这里的 lt 原本想约束的 pubkey[0]<q 和 pubkey[1]<q 并没有真正生效，因为 out 没有被设置），这使得整个电路允许非法的或者大于曲线质数 q 的 pubkey 存在。被忽略的额外的信号约束使得该函数（模板）的外层调用电路暴露出了可以被恶意攻击的漏洞。

漏洞修复

其中一个修复该问题的方案也很简单直接——我们只需要加上丢失的对于 lt 输出信号的约束即可。根据前文所述的 BLS12-381 椭圆曲线的性质，lt 的输出信号必须被设置为 1。以下即为我们给出的修复代码片段（该补丁已被合并入 circom-pairing 库官方版本）：

template CoreVerifyPubkeyG1(n, k){

…

var q[50] = get_BLS12_381_prime(n, k);

component lt[10];

… // Loops same as before

var r = 0;

for(var i=0; i<10; i++){

r += lt[i].out;

}

r === 10;

…

}

经验教训

正如去中心化金融（DeFi）的前尘所反复论及的「失之毫厘，谬以千里」的道理一般，零知识领域中的安全问题只会更加复杂难解：开发者不仅需要确保电路计算的正确性，还需要确保零知识验证组件不会接受预期以外的（多数情况下是非法的）输入输出对——这也使得传统的端到端（end-to-end）测试技术在有别于此的零知识系统架构面前显得捉襟见肘。因此，构建新型的程序分析和验证工具，对于辅助开发者应对种种前沿的零知识技术场景，有着举足轻重的作用。Veridise 的程序分析团队和安全专家们也正致力于研发更加尖端的分析和漏洞捕获工具。今后每月我们会陆续剖析 Veridise 在零知识电路审计过程发现的重大安全漏洞以及我们零知识安全工具的进展, 请关注 Veridise 的技术博客频道的更新。

致谢：我们要感谢 circom-pairing 的作者 Jonathan Wang、Vincent Huang 和 Yi Sun，以及来自 Succinct Labs 的 Uma Roy 和 John Guibas——感谢他们与 Veridise 团队在整个审计过程中的高效合作以及为本文写作提出的建设性的意见。