值得使用Circomspect - Trail of Bits博客
Fredrik Dahlgren
2022年9月15日
区块链, 密码学, 零知识证明
2019年10月，一名安全研究人员在以太坊网络上的去中心化非托管混币器Tornado.cash中发现了一个毁灭性漏洞。Tornado.cash使用零知识证明（ZKPs）允许用户私下存入和提取资金。这些证明本应保证每次提款都能与混币器中的对应存款匹配。然而，由于其中一个ZKP存在问题，任何人都可以伪造存款证明并从系统中提取资金。
当时，Tornado.cash团队通过利用该漏洞在其他人发现问题之前将资金从混币器中抽走，从而保护了用户的资金。然后他们修补了ZKPs并将所有用户资金迁移到新版本的合约中。考虑到底层漏洞的严重性，修复仅需两个字符几乎具有讽刺意味。
修复方法： 只需将 = 替换为 <==，一切就都好了（显然！）。
这个漏洞本可以通过我们今天开源的Circomspect（一种新的ZKP静态分析器）来发现。Circomspect可以找到使用Circom（Tornado.cash部署的ZKP所使用的语言）开发的ZKP中的潜在漏洞和代码异味。它可以识别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 bug查找器，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
页面内容
Circom的工作原理
Tornado.cash漏洞
我们的新Circom bug查找器，Circomspect
改进ZKP工具的状态
最近帖子
Trail of Bits的Buttercup在AIxCC挑战赛中获得第二名
Buttercup现已开源！
AIxCC决赛：记录表
攻击者的提示注入工程：利用GitHub Copilot
在NVIDIA Triton中 uncovering内存损坏（作为新员工）
© 2025 Trail of Bits。
使用Hugo和Mainroad主题生成。