零知识证明安全利器：Circomspect静态分析器深度解析

Tornado.cash安全事件回顾

2019年10月，安全研究人员在以太坊去中心化混币器Tornado.cash中发现了一个严重漏洞。该平台使用零知识证明（ZKPs）确保用户资金隐私存取，但由于某个ZKP实现问题，攻击者可以伪造存款证明并盗取资金。

令人惊讶的是，修复这个严重漏洞仅需修改两个字符：将=替换为<==。如果当时使用了我们今天开源的Circomspect静态分析器，这个漏洞在开发阶段就能被发现。

Tornado.cash使用Circom开发，这是一种领域特定语言（DSL）和编译器，用于生成和验证ZKPs。ZKPs是强大的密码学工具，允许在不泄露隐私信息的情况下证明陈述的真实性。

Circom编译器接收程序并生成证明者和验证者。证明者使用公开和私有输入运行计算并生成输出和证明，验证者则验证公开输入和计算输出与证明是否匹配。

问题出现在MIMC哈希函数中，该函数在定义输出时仅使用了赋值运算符<--（实际使用=，在旧版编译器中两者等效）。这导致在证明生成阶段赋值，但在验证阶段未进行约束，使得验证合约存在漏洞。

Circomspect是我们为Circom DSL开发的静态分析器和代码检查工具，基于Circom编译器相同的解析器实现。当前版本能够检测多种潜在问题：

该工具能够发现上述Tornado.cash漏洞，所有标记的问题都需要人工审查确认是否为真正漏洞。

像Circom这样的零知识DSL使得ZKPs技术民主化，让没有数学或密码学背景的开发者也能构建隐私保护系统。但由于ZKPs通常用于保护用户隐私或确保计算完整性，任何漏洞都可能对整个系统的安全性和隐私保证产生严重影响。

在Trail of Bits，我们积极填补这一工具空白。今年早些时候我们发布了Cairo语言的静态分析器Amarna，现在又开源了Circomspect。Circomspect正在积极开发中，可从crates.io安装或从GitHub仓库下载。

欢迎尝试并提供反馈，我们期待您的所有评论、错误报告和新分析功能的想法！