人们如何发现错误？

您可能想知道人们如何发现错误。可以通过代码审查，静态分析，动态分析（如模糊测试）和其他技术来找到难以捉摸的果实错误。但是，我们深深的逻辑错误。那些您找不到的东西。可能实现的协议非常复杂，或者很难定义正确性，并且很难检测到边缘情况。我注意到的一件事是，重新访问协议是查找逻辑错误的绝佳方法。

伊恩·米尔斯（Ian Miers）曾说过这样的话：“您需要时间，专业知识和有意义的参与。”我喜欢那句话，尽管有人可以指出，这些特质是紧密相连的-没有时间和专业知识就无法拥有有意义的参与- -它确实表明发现错误需要“努力”。

好。有意义的互动可能导致有意义的错误，并且可以在不同级别发现有意义的错误，因此您在这里，在黑暗中坐在自己的内裤上，一边喝啤酒一边躺在地板上，一些超级吃的东西躺在地上。盯着你看，以不知所措的频率闪烁，等待您发现此协议中的错误，您怎么办？也许该协议没有证据，这使您想知道您是否可以为此写一个...

它适用于Ariel Gabizon，他在2018年发现了他正在研究的Zcash加密货币使用的2013年zk-SNARK论文中的一个细微错误，他通过尝试为他正在阅读的论文写证明来发现了这一点，意识到作者虽然过去的协议可以负担得起，但如今人们却更加困难-他们需要证明。阿里埃勒（Ariel）发现的漏洞可以使任何人伪造无限量的金钱而未被发现。稍后升级到网络。

Zcash公司雇用的密码学家Ariel Gabizon在发现时发现了一个健全性漏洞。 [BCTV14]的密钥生成过程在步骤3中，生成各种元素，这些元素是评估与被证明语句相关的多项式的结果。证明者未使用其中的某些元素，并错误地将其包括在内。但是它们的存在使作弊证明者能够绕过一致性检查，从而将一个陈述的证明转换为另一陈述的有效外观的证明。这打破了证明体系的稳健性。

如果协议已经有了证明怎么办？这并不意味着很多，人们喜欢编写难以理解的证明，人们总是在证明中犯错误，所以第二个想法是阅读并试图理解证明可能会导致证明中的错误。这里有一些对您有意义的约定。

2001年，Shoup重新审视了一些证明，并在RSA-OAEP的证明中发现了一些明显的差距，从而导致了一种新的OAEP +方案，该方案从未在实践中被采用，因为那时候，正如我说的那样，我们真的不在乎证明。

[BR94]包含OAEP满足某种技术特性的有效证据，他们称之为“纯文本意识”。让我们将此属性称为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]。我们认为我们的工作强调安全证明质量及其积极验证的必要性。

现在，阅读和验证证明始终是一个好主意，但是它很慢，不灵活（如果您更改协议，可以很好地更改证明），而且很有限（您可能想证明重用部分内容的不同事物）如今，我们开始弥合笔和纸质证明与计算机科学之间的鸿沟：这被称为形式验证。事实上，形式验证正在蓬勃发展，最近有很多论文十年来，仅通过以正式语言描述协议并验证其可以承受不同类型的攻击，就可以在各处发现问题。

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

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

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

关键问题是，当人们孤立地仔细查看握手和加密协议这两个组件时，显然没有人在将两个组件连接在一起时仔细查看这两个组件。我很确定对此有一个完整的怪胎模因。

当然，没有人仔细看这个东西的原因是这样做很简单。协议有多种可能的案例需要分析，而我们正处于人类可以真正推理或同行评审员可以验证的协议复杂性的极限。添加到组合中的片段越多，这个问题就越严重。最后，我们都知道答案是人类要停止这项工作。我们需要机器辅助的协议验证，最好与实现它们的实际源代码绑定在一起。这样可以确保该协议确实按照其说的去做，并且实现者不会进一步搞砸它，从而使安全性证明无效。

好吧，马修，我们确实有正式生成的代码！ HACL *和fiat-crypto是两个例子，有人听说过失败吗？我有兴趣...

无论如何，还剩下什么呢？很多！正式生成的代码很困难，通常只覆盖协议的一小部分（例如椭圆曲线的现场算术），那么我们还能做些什么呢？如果以前没有实现过，那么实施该协议就很容易了。 2016年，Zcash的工程师Taylor Hornby撰写了一篇他在将零现金论文实施到Zcash加密货币中时发现的错误：

在这篇博客文章中，我们报告了Zcash协议中发现的安全性问题，同时准备将其部署为开放的，未经许可的金融系统。伪造货币。拥有足够的计算能力来查找128位哈希冲突的人本可以将钱花在自己身上，从而凭空创造出Zcash。

最后一件事是，大多数代码尚未经过正式验证，因此当然可以查看代码，但是您需要时间，专业知识，金钱等，因此，测试该怎么办呢？已知会导致问题的测试向量：

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

在所有这些中，我什至没有谈论编写规范的好处……那是另一天的事情。