Loading...
系列： 形式化验证系列 · 第 2 部分，共 3 部分 读者： 新手。第 1 部分介绍了形式化验证；在这里，我们将了解促使它变得迫切的真实漏洞。所需的一切都会从头解释。 你将收获： 对加密证明系统如何可能包含健全性漏洞的直观而准确的理解、2026 年 Zcash“Orchard”漏洞究竟是什么、为何这类漏洞能隐藏多年，以及为何它以前也发生过。
在第 1 部分中，我们说过，测试可以证明漏洞的存在，却永远无法证明漏洞不存在；而最危险的漏洞存在于系统的规范中，也就是其底层数学。本文就是一项案例研究。2026 年，人们发现 Zcash 的 Orchard 隐私池存在缺陷，该缺陷可能让攻击者悄无声息地制造无限量假币。它历经四年和多次审计仍未被发现。理解它及其前例，是理解为何必须证明系统正确性的最清晰理由。
Zcash 是一种具有隐私模式的加密货币。在其隐私池中，交易的金额、发送方和接收方都被隐藏。这种隐私是通过零知识证明实现的：一种能够证明交易遵守所有规则、却不透露交易内容的加密证明。
这种设计是一把双刃剑。在像 Bitcoin 那样的透明账本上，如果有人凭空变出代币，膨胀后的数字对所有人都可见，网络可以发现并回滚它。在隐私池中，数字按设计就是隐藏的。因此，如果证明系统本身存在缺陷，让无效交易看起来有效，那么伪造行为将会无法检测。你无法通过检查账本发现它，因为账本本来就被刻意设计为不透明。
这正是 Orchard 中实际发生的风险。要理解它，我们需要看看零知识证明实际在检查什么。
想象一位边境官员，必须在不直接查看旅客证件的情况下批准他们入境。每位旅客填写一份检查清单，官员会批准任何所有项目均已勾选的旅客。这份清单被设计为：只有合法旅客才能勾选每一项。
现在假设清单漏掉了一个关键项目，例如“护照未过期”。几乎所有人依然会如实填写，一切看似正常。但持有过期护照的人同样能勾选所有剩余项目并顺利通关。系统在日常使用中看起来没有问题。这个漏洞只会对专门寻找它的人产生影响。
零知识证明就像这样的检查清单。它不透露私密细节；它检查这些细节是否满足一组固定条件。如果一个必要条件被意外遗漏，那么某些无效输入也能通过，而一切仍会看起来正常。
让我们精确说明“条件检查清单”的含义，因为漏洞恰恰存在于这里。
在底层，“这笔交易有效”这一陈述会被编码为一个电路：由固定的一组算术条件构成，这些条件称为约束，并以数值上的方程式表示。为了生成有效证明，证明者必须提供满足每一个约束的秘密数值（即见证）。证明能够使验证者相信这样的见证存在，同时不泄露它。
我们需要这个系统具备一种称为以下名称的性质：
健全性： 必须不可能为一个错误陈述生成有效证明。只有真实陈述才应拥有满足所有约束的见证。
健全性是防止伪造的保证。如果健全性成立，有效证明就确实意味着“一笔真实、遵守规则的交易发生了”。如果健全性存在缺口，有效证明可能根本不代表任何意义。
约束常常需要将一个数值限定为简单形式。一个常见例子是：强制数值 b 成为一个位，即 0 或 1。实现这一点的标准方式是一个约束：
b × (b − 1) = 0
为什么它有效？只有当乘积的某个因子为零时，乘积才为零。因此，b × (b − 1) = 0 强制 b = 0 或 b = 1，不允许其他值。在从 0 到 16 的每个值中进行检查（在以 17 为模回绕的算术中），满足它的唯一数值恰好是 0 和 1。✓
现在想象这行代码被意外遗漏出电路。b 就突然不受约束了。不诚实的证明者可以将 b 设置为 5、9，或任意其他值，同时仍满足其余约束。这一行缺失的表达式就是一个健全性缺口：错误陈述现在也拥有满足条件的见证。
这并非假设。开发期间，人们在 Zcash 的第一个隐私设计 Sprout 中发现了恰好这种类型的布尔约束缺失，并在上线前修复了它。约束不足是构建这些电路时最常见、最危险的错误之一。
这就是 Orchard 漏洞的完整形态，只是以小规模呈现。现在来看真实情况。
Zcash 的隐私证明建立在椭圆曲线之上；椭圆曲线是一种数学对象，其点可以相互组合，也可以被数字“乘法”运算，而电路必须通过约束来强制这些操作正确执行。电路中包含执行椭圆曲线乘法并检查其正确性的组件。
根据 Shielded Labs 和研究员 Taylor Hornby 的披露，Orchard 缺陷具体是：
Orchard 电路中一个约束不足的元素，使得人们能够向椭圆曲线乘法输入任意错误输入，同时仍让乘法检查通过。
通俗地说，电路的检查清单缺少了本应锁定该乘法运算的项目。由于这个缺口，技术能力足够强的攻击者可以构造一个系统会接受的交易证明，即使该交易是凭空创造价值。这就是伪造；由于隐私池中的金额被隐藏，它在账本上会是无法检测的。Tachyon 团队后来从代码层面将同一缺陷描述为：电路中缺失的几行代码悄然扰乱了底层方程。
它与我们的检查清单故事完全对应：
| 检查清单故事 | Orchard 漏洞 |
|---|---|
| 缺少“护照未过期”项目 | 椭圆曲线乘法缺少约束 |
| 持过期护照的旅客仍然通过 | 任意错误输入通过乘法检查 |
| 其他所有人不受影响，因此看不出问题 | 正常交易完美运行，掩盖了缺陷 |
| 只有专门寻找它的人才会发现漏洞 | 专家刻意探查电路数学后才发现它 |
需要明确的是，这个问题极其严重：研究员借助 AI 编写了一个完整可用的攻击程序，并在本地测试网络中确认它能够生成无限量、无法检测的假币。这是一个真实且可被利用的缺陷，不是理论上的担忧。
该漏洞从 2022 年 5 月激活时起，一直存在于 Orchard 中，直到 2026 年 6 月的紧急修复才被消除，期间经历了世界上一些顶尖密码学家进行的多次专业审计。为什么？
因为正如第 1 部分所警告的，**测试只能抽样检查情形，而这个缺陷存在于无人抽样的情形中。**普通交易从未触发缺失的约束，因此每项测试都通过了，每天的正常运行也都毫无瑕疵。只有刻意构造一个专门针对该缺口的异常见证，才能触发这一缺陷。最终发现它的并非运行测试，而是推理电路的数学原理。
这项发现本身表明了安全领域的发展方向。2026 年 4 月，Shielded Labs 专门聘请安全研究员 Taylor Hornby 来寻找恰好这一类缺陷。2026 年 5 月下旬，一个新的前沿 AI 模型（Anthropic 的 Claude Opus 4.8）发布后不久，Hornby 将其与自定义分析工具和传统方法结合，在针对 Orchard 电路的审查中使用。2026 年 5 月 29 日，该审查发现了这一漏洞。
披露中有两项值得直白说明的冷静事实：
Orchard 漏洞属于一个反复出现的家族；看到这个家族，会让形式化验证不再像是可选项，而显得不可避免。伪造漏洞总能追溯到三个来源之一（第 1 部分的分类法）：规范（数学本身）、实现（代码未能遵循正确数学）或被破坏的假设。至关重要的是：
只有当伪造漏洞存在于规范中时，它才会无法检测。实现漏洞会留下永久公开证据，因为每个区块都会记录每笔交易的完整内容；因此，使用修正后的软件重放历史记录，便会暴露任何被有缺陷代码错误接受的交易。
Zcash 自身的历史说明了这一模式：
| 漏洞（年份） | 来源 | 可检测？ |
|---|---|---|
| Zerocash 承诺缺陷（2016，上线前） | 规范（截断哈希破坏了绑定属性） | 无法检测 |
| 可信设置健全性缺陷（2018） | 规范（底层 zk-SNARK 论文中的错误） | 无法检测 |
| 证明系统查询碰撞（2025） | 规范（证明系统中缺少检查） | 可检测 |
| 曲线子群验证漏洞（2016） | 实现（缺少子群检查） | 可检测 |
| Orchard 约束不足的乘法（2026） | 规范（电路） | 无法检测 |
贯穿其中的线索很鲜明：可能永远隐藏的缺陷，正是数学中的缺陷。这正是对规范进行机器检查证明所能消除的类别，一次性覆盖所有情形。测试和审计只能抽样；只有证明数学才能覆盖每一种输入。
Zcash 的开发者迅速分阶段采取了行动：
第二步正是形式化验证进入故事的地方，也是第 3 部分的主题。团队据此采取行动的认识值得预先说明，因为它将整个系列串联起来：
无法检测的伪造缺陷只能存在于协议的规范中。因此，如果你能证明规范排除了伪造，就能消除在此处隐藏四年的整类漏洞。
这正是第 1 部分中第一支柱的思想：验证规范，你就能弥合测试永远无法弥合的缺口。
我们进行了有意的简化。真实电路涉及数百个区域和数千项约束，实际缺陷在技术上也比单一缺失的位检查更复杂；我们使用位检查，是因为它恰好展示了约束不足电路的形态，也因为这种确切的错误真实存在于 Zcash 的历史中。正如官方披露所述，精确的 Orchard 缺陷是一次约束不足的椭圆曲线乘法。我们也压缩了披露和补救的时间线。如需权威技术说明，请参阅 Shielded Labs 的披露及 Project Tachyon 的文章。
b(b−1)=0 将 b 强制为 0 或 1；去掉它，b 可以是任何值。这一类漏洞真实存在于 Zcash 的历史中。）| 术语 | 通俗含义 |
|---|---|
| Shielded pool | Zcash 的隐私模式，金额和参与方均被隐藏 |
| Zero-knowledge proof | 证明一个隐藏陈述有效、但不透露其他信息的证明 |
| Circuit | 有效交易必须满足的一组固定算术条件 |
| Constraint | 电路中的一个条件（方程） |
| Witness | 满足约束的秘密数值 |
| Soundness | 只有真实陈述才能生成有效证明的保证 |
| Soundness gap | 使错误陈述能够通过的缺失约束 |
| Under-constrained | 电路缺少其所需条件，是 Orchard 漏洞的根源 |
| Detectable / undetectable | 利用行为是否会在公开账本中留下证据 |
真的制造出了假冒的 Zcash 吗？ 没有发现被利用的证据，团队也认为其可能性较低。但由于这一缺陷无法从账本中检测出来，仅凭账本无法完全证明它从未发生，这也是应对措施如此彻底的原因。
为什么隐藏金额会让漏洞更严重？ 在透明链上，铸造的代币可见，并可被发现和逆转。当金额因隐私而被隐藏时，伪造漏洞不会产生可见异常，因此可以在无人察觉的情况下持续存在。
为什么多年的审计没有发现它？ 审计和测试主要检查真实场景下的行为。这个缺陷只会在特意构造、针对数学边界情形的异常输入下出现，常规审查没有触发它。它是通过针对电路的推理发现的，而非测试。
真的只需缺少一个约束就够了吗？ 是的。证明系统的强度取决于其完整的约束集合。遗漏一个必要条件，就足以让无效陈述通过。
AI 起到了什么作用？ 一位研究员结合前沿 AI 模型、自定义工具和传统方法，审查电路数学并发现了该缺陷。AI 越来越多地被用于安全攻防两端，这也是为什么现在证明系统正确性变得如此重要。
假设一笔隐私交易本应证明“流入的资金等于流出的资金”，但电路忘记约束其中一个输出值。不诚实的证明者可以做什么？为什么公开账本看起来会完全正常？（答案见下文。）
由于该输出未受约束，证明者可以将其设置得大于真实输入允许的数值，从而凭空创造价值，即伪造。证明仍会通过验证，因为缺失的约束是唯一能发现这种不平衡的条件。而且由于隐私池隐藏金额，账本只会显示“一笔有效交易发生了”，没有可见的不平衡来发出警报。伪造是真实的，但不可见；这正是电路健全性如此重要、也正是它必须被证明而非测试的原因。
第 3 部分 · Ironwood： 修复不只是一次补丁。Zcash 的工程师构建了一个新的隐私池，并为其附上一份机器检查的数学证明：在既定假设下，它不可能创造假币。这份证明在 Lean 证明助手中写成，包含超过 2,700 个定理。我们将了解“余额完整性”和“知识健全性”分别意味着什么、证明究竟覆盖和不覆盖什么，以及旧隐私池如何被安全退役。
属于 ZecHub 的 Formal Verification 系列。