值得使用Circomspect - Trail of Bits博客

Fredrik Dahlgren
2022年9月15日
区块链, 密码学, 零知识证明

2019年10月，一名安全研究人员在以太坊网络上的去中心化非托管混合器Tornado.cash中发现了一个毁灭性漏洞。Tornado.cash使用零知识证明（ZKPs）让用户能够私下存入和提取资金。这些证明本应保证每次提款都能与混合器中的对应存款匹配。然而，由于其中一个ZKP存在问题，任何人都可以伪造存款证明并从系统中提取资金。

当时，Tornado.cash团队通过利用该漏洞，在问题被他人发现之前将资金从混合器中抽走，从而保护了用户的资金。然后他们修补了ZKPs并将所有用户资金迁移到新版本的合约中。考虑到底层漏洞的严重性，修复仅需两个字符几乎具有讽刺意味。

修复方法： 只需将=替换为<==，一切就都好了（显然！）。

这个漏洞本可以通过使用Circomspect来发现，这是我们今天开源的一个新的ZKP静态分析器。Circomspect可以找到使用Circom开发的ZKPs中的潜在漏洞和代码异味，Circom是Tornado.cash部署的ZKPs所使用的语言。它可以识别Circom程序中可能出现的各种问题。特别是，它本可以在开发过程的早期，即在合约部署到链上之前，就发现Tornado.cash中的漏洞。

Circom的工作原理

Tornado.cash是使用Circom开发的，这是一种领域特定语言（DSL）和编译器，可用于生成和验证ZKPs。ZKPs是强大的密码学工具，允许你在不泄露任何私人信息的情况下对陈述进行证明。对于像完整计算机程序这样的复杂系统，使用ZKPs的困难部分在于将陈述表示为证明系统可以理解的格式。Circom和其他DSL用于描述计算，以及对程序输入和输出（称为信号）的一组约束。Circom编译器接受一个程序并生成一个证明者和一个验证者。证明者可用于在公共和私有输入集上运行DSL描述的计算，以产生输出，以及证明计算正确运行的证明。验证者然后可以接受公共输入和计算输出，并根据证明者生成的证明进行验证。如果公共输入与提供的输出不对应，验证者会检测到这一点。

下图显示了一个小的Circom程序玩具示例，允许用户证明他们知道一个私有输入x，使得x⁵ - 2x⁴ + 5x - 4 = 0：

行y <== x⁵ - 2 * x⁴ + 5 * x - 4告诉编译器两件事：证明者应在证明生成阶段将右侧的值分配给y（在Circom中表示为y <-- x⁵ - 2 * x⁴ + 5 * x - 4），以及验证者应在证明验证阶段确保y等于右侧（在Circom中表示为y === x⁵ - 2 * x⁴ + 5 * x - 4）。这种二元性在像Circom这样的零知识DSL中经常出现。证明者执行计算，验证者必须确保计算正确。有时，同一枚硬币的两面可以用相同的代码路径描述，但有时（例如，由于在基于R1CS的系统如Circom中如何指定约束的限制）我们需要使用不同的代码来描述计算和验证。如果我们忘记添加描述与证明者执行的计算相对应的验证步骤的指令，就可能伪造证明。

Tornado.cash漏洞

在Tornado.cash的情况下，结果发现用于计算证明中Merkle树根的MIMC哈希函数在定义输出时仅使用了赋值运算符<--。（实际上，它使用了=，如上面的GitHub差异所示。然而，在Circom编译器的先前版本中，这与<--的解释方式相同。今天，此代码将生成编译错误。）正如我们所看到的，这仅在证明生成期间为输出分配了一个值，但未在证明验证期间约束输出，使验证合约易受攻击。

我们的新Circom漏洞查找器，Circomspect

Circomspect是一个用于以Circom DSL编写的程序的静态分析器和linter。它的主要用途是作为审查Circom模板和函数的安全性和正确性的工具。实现基于Circom编译器，并使用与编译器相同的解析器。这确保编译器可以解析的任何程序也可以使用Circomspect解析。解析器生成的抽象语法树转换为静态单赋值形式，这允许我们对输入程序执行简单的数据流分析。

当前版本实现了许多分析过程，检查Circom程序中的潜在问题，如未约束信号、未使用变量和遮蔽变量声明。它警告用户每次使用信号赋值运算符<--，并且通常可以检测电路是否使用<--将二次表达式分配给信号，表明可以使用信号约束赋值运算符<==代替。此分析过程本可以发现上述Tornado.cash中的漏洞。Circomspect标记的所有问题并不代表漏洞，而是应审查的位置以确保代码按预期执行。

作为Circomspect可以找到的问题类型的示例，请考虑来自circom-pairing存储库的以下函数：

此函数乍一看可能有点令人生畏。它使用扩展欧几里得算法实现模p的逆元。在包含文件上运行Circomspect会产生许多警告，告诉我们数组y、v和newv的赋值对函数的返回值没有贡献，这意味着它们不能影响见证或约束生成。

在函数find_Fp_inverse上运行Circomspect会产生许多警告。

仔细查看实现发现，变量y仅用于计算newv，而newv仅用于更新v，v仅用于更新y。因此，变量y、v和newv都不对函数find_Fp_inverse的返回值有贡献，并且都可以安全地删除。（顺便说一句，这完全合理，因为在两个互质整数num和p上运行扩展欧几里得算法会计算两个整数x和y，使得x * num + y * p = 1。这意味着如果我们对num模p的逆元感兴趣，它由x给出，并且不需要y的值。由于x和y是独立计算的，用于计算y的代码可以安全地删除。）

改进ZKP工具的状态

像Circom这样的零知识DSL已经民主化了ZKPs。它们允许没有数学或密码学背景的开发人员构建和部署使用零知识技术保护其用户的系统。然而，由于ZKPs通常用于保护用户隐私或确保计算完整性，ZPK中的任何漏洞通常对整个系统的安全和隐私保证产生严重影响。此外，由于这些DSL是新兴技术，开发人员可用的工具支持非常少。

在Trail of Bits，我们正在积极努力填补这一空白。今年早些时候，我们发布了Amarna，这是我们用于以Cairo编程语言编写的ZKPs的静态分析器，今天我们开源了Circomspect，这是我们用于Circom程序的静态分析器和linter。Circomspect正在积极开发中，可以从crates.io安装或从Circomspect GitHub存储库下载。请尝试并告诉我们您的想法！我们欢迎所有评论、错误报告和新分析过程的想法。

如果您喜欢这篇文章，请分享：
Twitter
LinkedIn
GitHub
Mastodon
Hacker News

页面内容
近期帖子
使用Deptective调查您的依赖项
系好安全带，Buttercup，AIxCC的评分回合正在进行中！
使您的智能合约超越私钥风险
Go解析器中意外的安全隐患
我们审查首批DKLs23库的收获
来自Silence Laboratories的库
© 2025 Trail of Bits。
使用Hugo和Mainroad主题生成。