Zcash的Ironwood升级后检测伪造——Tachyon项目

tachyon.z.cash 发布于 2026-07-08 阅读 12

Zcash的Orchard屏蔽池近期被发现一个不可检测的伪造漏洞,已通过网络升级修复。为了确保安全性,社区计划启动基于Orchard的新池Ironwood,并采用形式化验证来彻底排除不可检测的伪造bug。文章详细分析了各种类型的伪造漏洞,包括规范漏洞和实现漏洞,指出只有规范漏洞可能导致不可检测的伪造。形式化验证通过数学证明确保了协议的正确性,从而消除了所有不可检测的伪造风险。

上个月,Shielded Labs 安全研究员 Taylor Hornby 发现了我们的旗舰屏蔽池 Orchard 中的一个伪造漏洞。该漏洞已在一个网络升级中修复,且据信未曾被利用。1

然而,由于该漏洞的利用无法被检测,我们的社区宣布计划启动一个新的屏蔽池,名为 Ironwood。该池基于 Orchard,但以漏洞已修复的状态重新启动。得益于协议中的旋转门机制,钱包可以通过将资金从 Orchard 迁移到 Ironwood 来帮助证明从未发生过伪造,同时保护其用户。与此同时,旧 Orchard 池内的支付将被禁用,从而对流通 ZEC 的供应量设定上限。

我们再也承受不起在 Zcash 中发布重大 bug 的代价,因为我们可能没有足够幸运再次自己发现下一个漏洞。仅仅修补最近发现的 bug 是不够的,因此我们的社区采取了多管齐下的努力,以确保即将到来的 Ironwood 池的正确性。这包括使用前沿 AI 工具进行广泛的审计和分析。

我们的团队主要进行了一项全面的努力,对 Ironwood 进行形式化验证排除了不可检测的伪造 bug。在本文中,我们想介绍这一努力及其将为 Ironwood 安全性提供的强有力保证。

伪造漏洞

伪造 bug 并非 Zcash 等隐私加密货币所独有。任何透明账本都可能存在此类漏洞,包括比特币,它在早期历史上曾发生过伪造事件

在比特币中,交易值是公开的。这意味着,一个隐蔽 bug 被利用后很可能很快就会被注意到,这就是比特币的 bug 被迅速修补的原因。2 爆炸半径有时也更小,因为缺乏隐私意味着伪造资金可以在修复过程中被识别。3

更重要的是,公开账本中伪造 bug 的利用首先是可以检测的,这意味着我们可以检查账本历史,看看这些缺陷是否曾被利用过。 Zcash 过去著名的伪造漏洞缺乏这一特性,这尤其令人恼火:我们似乎都在它们被利用之前就发现了它们,但在通过旋转门收集证据之前,我们无法明确断言。

不可检测的伪造

不可检测的伪造漏洞只有在 Zcash 中才可能出现,因为它具有强大的隐私性:用户保留自己的交易信息,而协议则使用密码学来检查没有人违反规则。这意味着屏蔽池内货币供应的稳健性依赖于密码学假设。

每一个可设想的伪造漏洞都源于协议规范中的错误、实现它的软件中的错误,或两者之下被打破的密码学假设。

按可检测与不可检测伪造,以及按被打破的假设、规范 bug 和实现 bug 组织的伪造漏洞分类表。

实现 bug 只能产生可检测的伪造。规范 bug 可以通过数学方式排除。密码学假设是不可避免的。

被打破的假设可能引入不可检测的伪造漏洞,但它们不是 bug,而且 Zcash 历史上没有任何伪造漏洞是由此引起的。随着时间的推移,我们减少了对高风险假设的依赖:我们较新的屏蔽池完全避免了可信设置和配对密码学,并依赖于大多数其他加密货币所依赖的同一类离散对数(DLOG)假设。4

规范与实现 Bug

一旦我们将密码学假设视为理所当然,伪造漏洞就分为两种:规范中的 bug 和实现中的 bug。规范是我们密码学协议的形式化描述,我们可以用数学方式推理。它描述了协议的算法,并陈述了它们旨在提供的安全属性。实现则应该执行这些算法。

我们的形式化验证工作基于一个简单的观察:不可检测的伪造 bug 只能存在于规范中。

实现 bug,无论它们可能造成其他什么损害,都只能产生可检测的伪造。区块提交了每个交易的完整内容,包括其证明,因此通过修正后的软件重放历史是任何人都可以执行的确定性计算。任何被有 bug 的软件错误接受的交易都会成为永久的公开证据。

Zcash 的历史说明了这两种类型。

Zerocash InternalH 碰撞 Bug (2016)

Zcash 的屏蔽协议围绕两个密码学对象:一个票据,它封装了货币价值和一个有权花费它的密钥;以及一个空化器,它作为一种撤销Token防止双花。票据在功能上类似于比特币交易输出,用户通过明确标识它们来花费它们,以便网络可以将它们标记为已消耗。

为了保护用户隐私,Zcash 网络上的每个用户改为为他们花费的每个票据揭示一个空化器。所有这些空化器都被添加到一个列表中,并且禁止重用,这样空化器就充当了票据的公共墓碑。为了防止伪造,空化器必须在密码学上绑定到被花费的票据,以便一个给定的票据只能产生一个唯一的空化器。

Zcash 中的票据以密码学承诺的形式揭示。这些承诺应该是隐藏的,意味着发现其内容很困难,并且是绑定的,因此以多种解释打开承诺也很困难。

原始 Zerocash 论文中票据承诺的哈希结构使用截断的哈希输出来实现强隐藏属性,但破坏了防止双花所需的计算绑定属性。

原始的 Zerocash 论文(Zcash 基于此构建)在此绑定属性中存在一个缺陷,即承诺并未绑定到完整的票据。由于用于计算空化器的值仅通过截断的哈希绑定,攻击者可以找到哈希碰撞5 并替换第二个值,从而两次花费同一个票据。

这个缺陷由 Taylor Hornby 在 Zcash 启动前发现并修复。这是协议规范中的一个错误,其利用将是不可检测的。

电路 Bug

在不揭示票据的情况下花费它们需要证明遵守了规则。每个屏蔽交易都携带一个 zk-SNARK(一种零知识证明),表明被花费的票据存在于池中且其空化器被正确派生等要求。被证明的陈述被表示为一个电路,它用数学方程的形式描述计算,而网络的验证器根据这些方程检查每个交易的证明。

最近的 Orchard 漏洞是由 zk-SNARK 电路中的一个“稳健性” bug 引起的,这个缺陷让不诚实的证明者能够说服验证器接受一个虚假的陈述。

Orchard 电路代码中缺失的行,以及对应置换多项式系数中缺失的转置。

Orchard 电路代码中缺失的行(左图)悄悄打乱了底层的数学(右图)。形式化验证可以直接检查方程,证明其中没有错误,而无需审计代码本身

从道德上讲,这不是实现中的 bug。zk-SNARK 电路模拟了真实计算,因此其规范足够复杂,以至于在实践中我们使用代码来表示和描述它。全节点从不针对交易运行你上面看到的代码。相反,它推导出验证器所依赖的数学公式。

我们也曾捕获过 Zcash 的 zk-SNARK 电路中的其他 bug,尽管它们从未在正式发布中出现。在 Sprout(Zcash 最初的屏蔽池)首次启动之前,我们在重新实现 Zerocash 协议时发现了一个缺失的布尔约束。像这样的错误始终是规范中的 bug,因为推理 SNARK(及其电路)对于建立关于协议安全保证的任何有用断言都是必要的。

当我们对 zk-SNARK 进行形式化验证以排除 bug 时,我们实际上并不研究电路代码。相反,我们用代数方式表示验证器的指定行为,并直接证明我们需要的正确性属性。这同时捕获了电路 bug 和 SNARK 本身的 bug。

[BCTV14] 稳健性缺陷 (2018)

最初的 Sprout 协议也存在一个不可检测的伪造 bug(由 Ariel Gabizon 发现),源于描述 Sprout 部署的 Pinocchio 风格 zk-SNARK 的 [BCTV14] 论文中的一个错误。像这样的早期 zk-SNARK 需要可信设置:一个仪式,采样秘密随机数并将其编码到用于创建和检查证明的公共参数中。该仪式需要事后销毁随机数。

BCTV14 论文节选,高亮显示了证明者不需要但若泄露会破坏稳健性的可信设置元素。

已发布的 zk-SNARK 构造要求设置过程产生证明者不需要的元素,但任何获得它们的人都可以用代数方式干扰验证器的公共输入。这些元素没有分发给用户,但在可信设置记录中可用。

在这种情况下,缺陷同样在于 zk-SNARK 验证器的规范,而不是代码。论文想当然地认为,将某些多项式编码包含在可信设置参数中后稳健性仍然成立,但这从未被严格证明,并且被证明是错误的。6 事实上,对指定验证器的形式化分析会揭示问题:有了这些值,验证器接受的证明不再保证证明者知道一个有效的见证。7

查询碰撞 Bug (2025)

规范 bug 也可能产生可检测的伪造 bug。去年,zkSecurity 识别出了 Orchard 使用的证明系统 halo2_proofs 中的一个稳健性 bug。某些特制的电路会导致验证器从证明字符串中消耗一个冗余的多项式求值而不检查其正确性,从而允许恶意证明者对此撒谎并破坏稳健性。

这是规范中的 bug,而非实现中的:对于受影响的电路,冗余求值和缺失的检查都出现在电路推导出的验证器的代数描述中。形式化分析可以捕获所有这种形式的 bug,因为对该验证器证明知识稳健性的尝试将会失败。

有趣的是,利用将是可检测的,尽管 zkSecurity 的报告没有探讨这一点。Orchard 或任何其他已知的生产部署实际上并未受到影响,但如果有一个受影响,每一个被接受的证明都会永久记录冗余求值和它本应一致的值。诚实的证明者总是使两者一致,因此任何两者不同的被接受证明都是利用企图的证据。

验证 Bug (2016)

Zcash 在实现中也存在 bug。

最初在 Zcash 中使用的零知识证明基于配对友好椭圆曲线。这些构造围绕两个椭圆曲线群(分别名为 和 )展开。在最初的 Sprout 协议中,使用的椭圆曲线(BN254)给了我们一个素数阶椭圆曲线群 ,但 是一个不同复合阶椭圆曲线群的素数阶子群

不幸的是,libsnark 中的一个 bug 意味着元素未被检查是否存在于实际的素数阶子群中。读者可能从著名的 CryptoNote 伪造 bug 中认识到这种 bug。就像那个 bug 一样,因为它存在于实现中,它是可检测的:有 bug 的验证器接受的任何交易都永远留在链历史中,而在其上重新运行正确的验证器会暴露它。该 bug 在 Zcash 启动后不久就被修复,并且如果它曾经可被利用8,我们知道它从未被利用过。

类似的实现缺陷可能存在于我们的曲线和域算术中。规范基于抽象群操作定义了密码学协议,因此如果真实实现有时行为异常,这种偏差将因同样的原因变得可检测。

空化器与锚点缓存失效

并非每个实现风险都是密码学性质的。全节点负责防止重复的空化器,有几种错误可能悄然允许重用:链重组期间的缓存失效 bug,或区块和交易中的边界情况。类似的危险围绕“锚点”,即每个交易引用的 Merkle 树根,用于证明它花费的票据存在于池中;只有在区块边界上该锚点是该池的有效候选时,锚点才被接受。

Zcash 从未有过这种类型的 bug。尽管如此,这些将是实现中的 bug,并且如果被利用将是可检测的。

形式化验证

对我们来说幸运的是,用数学方式排除密码学规范中的 bug(从而排除所有不可检测的伪造 bug)远比排除软件中的 bug 容易得多,软件的正确性依赖于关于我们代码执行环境的难以捉摸的断言。9 这不仅仅是退而求其次的问题。软件中的 bug 会在链历史中暴露自己,正如我们所见,而底层数学中的错误恰恰是那些可能永远隐藏的。

我们分析形式化协议的数学结构和行为,将其正确性简化为我们规范中陈述的安全概念和密码学假设。10 那么唯一有点不牢靠的主张是,Zcash 网络上的真实软件实际上执行了我们形式化的算法,而任何偏差都是实现 bug,重放历史将暴露它。任何潜在的伪造 bug 都无处可藏:它要么是形式化协议中的一个缺陷(此分析可消除之),要么是软件中超出该范围的偏差(总是可检测的),要么是底层假设的破坏。

现代工具如 Lean 可以在编写后自动检查这些证明,提供对其数学正确性的确定性,而由人类引导的大语言模型可以将生成这些机器辅助证明的过程缩短到仅需数周,即使对于我们这样复杂的密码系统也是如此。我们已将时间和资源转向为 Ironwood 提供这种分析,与我们自己的 Tal Derei、来自 zkSecurity 的 Gregor Mitscha-Baude(我们已签约他协助此工作)以及 Zcash Open Development Lab 的 Daira-Emma Hopwood 合作。得益于我们设计并形式化分析 Tachyon 即将推出的协议的经验,我们在过去几周取得了实质性进展。

结论

以上并非每种伪造 bug 或我们协议中严重缺陷的每种可能影响的详尽列表。相反,它表明形式化验证我们的规范足以排除我们协议及其实现中可能存在的所有不可检测的伪造漏洞。

原则上,形式化验证可以走得更远:实现本身以及其中的每一个 bug 都可以接受同样的数学审视,我们打算随着时间的推移追求这一点。但不可检测的伪造是风险最高的一类 bug,而且只有数学才能解决这个问题,因此我们的努力首先集中于此。大部分分析依赖于一个称为知识稳健性的属性,它的故事,以及我们形式化的验证器与网络实际运行的软件之间的比较,将在下一篇文章中讨论。


  1. 发现伪造漏洞的利润最大化攻击者面临一场与发现、修补、竞争攻击者(尤其是在我们代码开源的情况下)、交易所干预以及最终市场崩盘的竞赛。他们的动机是在机会消失前将尽可能多的伪造币转换为外部价值,同时保持在引发怀疑的门槛以下。一旦漏洞被公开,同样的逻辑就变成了一场更广泛的退出竞赛:信心下降,流动性恶化,交易所和用户采取防御性反应,而预期他人(包括其他伪造者)抛售是迅速抛售的有力理由。目前尚未观察到任何此类现象。

  2. 在比特币中发现的 bug 在几小时内得到修补,随后进行了跨越数十个区块的区块链重组。这次修复剥夺了诚实矿工新挖出的数千比特币,并从账本中抹去了数十亿伪造币。

    Jeff Garzik 关于比特币区块 74638 的 Bitcointalk 帖子截图,显示了两个巨大的输出值。

  3. 如果比特币 bug 在利用发生数月后才被发现,结果会怎样?可能修复会大不相同;跨越数月历史的链重组是不现实的,因此很可能伪造资金下游的交易图会被作废。但若这些资金已经流通,信任危机可能无法承受。

  4. 我们还整合了假设。例如,我们依赖 Pedersen 哈希的抗碰撞性用于基于 Merkle 树的累加器,这紧密归约到一个我们已为稳健性假设的现有假设(DLOG)。此外,我们未来将继续弱化假设以防御量子对手,或向协议添加冗余。

  5. 哈希输出被截断为 位,因此生日攻击可以用大约 次试验找到碰撞。使用现成硬件的成本约为两千美元,对于有能力在 Zerocash 方案中创建和花费票据的动机攻击者来说完全可承受。

  6. 这个疏忽是同一批作者在冗长分析中的一个微小点,但该构造从未被正式证明,并且被原始同行评审者以及随后的多次审计所遗漏。形式化验证当时还不是如今广泛使用的工具。

  7. 破坏稳健性的值,除了被可信设置隐藏外,还以某种方式编码在验证器的公共参数中,恶意证明者可以通过精心选择证明字符串来替换这些值。这专门是知识稳健性的失败。

  8. 素数阶与 所在群的余因子之间的差距防止了低阶点;它并未完全阻止子群外的点。缺乏子群检查意味着证明者可以使用任何阶的点,但它也以尚未完全理解的方式增加了攻击者的灵活性。实际上,未检测到任何利用。

  9. 即,我们正确实现了数学算法,代码在忠实的执行环境中运行,并且没有恶意行为者以违反我们假设的方式篡改网络参与者的硬件或软件。我们可能还假设我们依赖的密码学是稳健的,但这些假设被明确陈述,并且可以随时间放宽。

  10. 例如,知识稳健性,它规定任何说服验证器接受一个证明的对手实际上必须“知道”一个有效的见证。这是一个常见的密码学概念,我们旨在为我们的构造证明它。

  • 原文链接: tachyon.z.cash/blog/dete...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~

相关文章

0 条评论