人们是如何发现软件 bug 的？

容易找到的 bug 可以通过代码评审、静态分析、动态分析（例如 fuzzing）以及其它技术发现。但是，深层逻辑 bug 是如何被发现的？那些 bug 很不容易被人们找到。也许实现的协议太复杂，或者正确性很难定义，或者边界案例很难监测。我有一点发现：重新审视协议是发现逻辑 bug 的一种很好的方法。

伊恩·迈尔斯曾说过：“你需要时间、专业知识和有意义的参与“。我喜欢这句话，尽管有人指出，这些特质是紧密联系的——没有时间和专业知识的话，你不可能会有意义的参与——这确实表明，发现 bug 需要“努力”。

有意义的参与会发现有意义的 bug，而有意义的 bug 可以在不同的级别找到。所以就在这，你在黑暗中穿着内裤坐着，一边拿着啤酒，一边放着一些零食。你的电脑正盯着你，以你察觉不到的频率闪烁，等待你在这个协议中发现一个 bug。你是做什么的？也许这个协议没有证明，这导致你在想是不是为它写一个...

阿里尔·加比松（Ariel Gabizon）就是这样，他 2018 年在正研究的 Zcash 加密货币使用的2013 zk-SNARK论文中发现一个细微错误。他尝试为正在看的一篇论文写一个证明，然后意识到作者做了一些手脚，发现其中的错误。虽然当时的协议可以支持它，但是现在的人们更加困难——他们需要证明。阿里尔发现的这个 bug 可以让任何人在不被发现的情况下伪造无限量的加密货币。这个 bug 在几个月后对网络的一次升级中被悄悄修复了。

Ariel Gabizon,，Zcash 公司雇佣的一名密码学家在研究时发现一个可靠性漏洞。在步骤 3 中，[BCTV14]的主要生成程序，生成各种与被证明的声明有关的多项式求值的结果等元素。其中一些元素没有被证明者使用，并被错误地包含在内；但它们的存在使得作弊的证明者能绕过一致性检查，从而将一个声明的证明转换成另一个声明的有效证明。这破坏了证明系统的可靠性。

如果协议已经有证明呢？好吧，这并不能说明什么，人们喜欢写莫名其妙的证明，而且人们总是在证明中犯错。因此，第二个想法是，阅读并尝试理解一个证明可能会发现这个证明中的一个 bug。下面是一些有意义的参与。

在 2001 年，Shoup 重新审视了一些证明，发现了RSA-OAEP的证明中存在一些错漏，从而提出了一个新的 OAEP+方案，但在实践中从未被采用过。因为那时，我们真的不关心证明。

[BR94]包含了一个有效证明，OAEP 满足他们称为“明文感知（plaintext awareness）”的某个技术属性。我们称之为属性 PA1。然而，它没有证据表明，PA1 意味着对选择密文攻击和非可塑性的安全性。此外，作者指的是自适应选择密文攻击（如[RS91]所述），还是无差别的（又称午餐时间）选择密文攻击（如[NY90]所述），都还不清楚。

2018 年晚些时候，针对 OCB2 区块密码的一系列发现迅速导致破解密码的实际攻击。

我们提出了一个针对 OCB2 的实际伪造和解密攻击，OCB2 是一个备受关注的 ISO 标准的认证加密方案。这因为 OCB2 的证明与实际构造之间存在差异而是可能的，尤其是将 OCB2 解释为一种结合 XEX 和 XE 的 TBC 模式。我们评论说，因此证明中的错误，'可证明安全的方案'有时仍然会被打破，或者方案仍然是安全的，但是其证明需要被修复。即使我们把重点放在 AE 上，我们也能发现许多这样的例子，例如 NSA 的 Dual CTR [37,11]、 EAX-prime [28]、 GCM [22] 以及 CAESAR 的一些意见[30,10,40]。我们认为，我们的工作强调了安全证明的质量及其积极验证的必要性。

现在，阅读和验证一个证明通常是一个好主意，但是比较慢，而且不灵活（如果你改变协议，就需要改变证明），而且很有限（你可能想要复用证明的某些部分证明不同的东西，但这很不直观）。今天，我们开始弥合笔算证明和计算机科学之间的差距：这被称为形式验证。事实上，形式证明正蓬勃发展，近年来，许多论文通过用一种正式语言描述协议并验证它们能否抵御不同类型的攻击。

使用Diffie-Hellman重新审视协议上的小型子组和无效曲线攻击：

我们在 Tamarin Prover 中实现了我们的改进后的模型。我们发现了 Secure Scuttlebutt Gossip 协议的一种新攻击，独立发现了针对 Tendermint 安全握手的攻击，并评估了针对最近的蓝牙攻击提出的缓解措施的有效性。

似乎合法：针对使用签名的协议的细微攻击的自动分析:

我们在 Tamarin Prover 中实现了我们的模型，产生了自动执行这些分析的第一种方法，并在几个案例研究中验证了它们。在这个过程中，我们发现了针对 DRKey 和 SOAP 的 WS-Security 的新攻击，这两个协议在传统的符号模型中被证明是安全的。

但即使是这种技术也有局限性！（天呐，David，你什么时候能停下来？）

在 2017 年，Matthew Green写到:

我不想花时间讨论 KRACK 本身，因为其漏洞非常简单。相反，我想谈谈为什么这个漏洞在 WPA 标准化这么多年后仍然存在。另外，回答一个问题：这种攻击是如何得逞的，尽管 802.11i 握手已经被正式证明是安全的？

他后来写到：

关键问题是，当人们孤立地仔细观察这两个组件——握手和加密协议时，显然没有人仔细观察这两个组件连接在一起的时候。我敢肯定这里面肯定有问题。

指的是“2 个单元测试。0 个集成测试”。开玩笑。

他然后意识到这是一个难题：

当然，没有人仔细观察这些东西的原因是这么做很难。协议有指数级的案例需要分析，而我们处于人类可以搞明白或者同行评审员可以验证的协议复杂度的极限。你向其中加入的东西越多，这个问题就越复杂。最后，我们都知道，答案是人们停止做这件事。我们需要机器辅助的协议验证，最好与实现它们的源代码绑定。这将确保协议真正按它所说的执行，并且实现者不会把它搞的更糟，从而使安全性证明无效。

好吧，Matthew，我们都有正式生成的代码！HACL*和fiat-crypto是两个例子。有人听说过那种失败吗？我会感兴趣的...

不管怎样，我们还剩下什么？很多东西！正式生成的代码很难，通常只覆盖你的协议的一小部分（例如，椭圆曲线的字段算法）。那我们还能做什么呢？如果一个协议之前没有实现就去实现这个协议，是无脑的。在 2016 年，Zcash 的一位工程师 Taylor Hornby 写到了他在 Zcash 加密货币中实现无现金论文时发现的一个bug：

在这篇博客中，我们报告了我们在准备将 Zcash 协议部署为一个开放的无许可的金融系统时发现的安全问题。如果我们在没有发现并修复 InternalH Collision 漏洞的情况下推出 Zcash，它可能会被用来伪造货币。有足够的算力来发现 128 位散列碰撞的人将可以双倍花钱给自己，凭空创造出 Zcash。

也许用另一种语言重新实现这个协议可能奏效？

最后，大部分代码并没有经过正式验证。当然， 评审代码是可行的，但是你需要时间、专业知识、金钱等等。因此，测试怎么样？这就是Wycheproof通过实现一些已知会导致问题的测试向量所做的：

这些观察结果促使我们开发了 Wycheproof 项目，这是用于测试已知弱点或检查某些加密算法的预期行为的单元测试集合。Wycheproof 项目为大多数加密算法提供了测试，包括 RSA、椭圆曲线加密和认证加密。我们的密码学家系统地调研了文献并实现了大部分已知的攻击。我们有 80 多个测试用例，发现了 40 多个 bug。例如，我们发现我们可以恢复广泛使用的 DSA 和 ECDHC 实现的私钥。

原文链接：

https://cryptologie.net/article/511/how-do-people-find-bugs