Veridise截获Circom-Pairing核心零知识电路安全漏洞

本文由Veridise译自: Circom-Pairing: A Million-Dollar ZK Bug Caught Early
原文作者：Veridise
保留所有权利。

Image Not Showing Possible Reasons

The image file may be corrupted
The server hosting the image is unavailable
The image path is incorrect
The image format is not supported

Veridise技术博客系列：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团队在整个审计过程中的高效合作以及为本文写作提出的建设性的意见。

关于Veridise

Veridise专注于区块链安全并为所有区块链层级（智能合约、web3应用、零知识电路以及区块链实现）提供安全审计服务和软件分析工具。Veridise由长期从事形式化验证以及软件安全的知名教授和研究者创立，并旨在提供最尖端区块链安全加固技术。Veridise通过多种方式与客户建立深度合作关系，包括安全审计、自动化安全分析工具（模糊测试、静态分析、形式化验证等）以及两者结合等。

想了解更多相关信息，请关注我们的公众账号或者访问我们的网站：