亚伦坟墓对人群沟通的正式验证

卢克·穆罕沃斯：DARPA的人群采购正式验证（CSFV.）计划“旨在调查大量非专家是否可以比常规过程更快地执行正式验证和更具成本效益。”为此，程序创建了Verigames.com，几个免费在线益智游戏的家。

您对Verigames的贡献是风暴。在一个博客，你的同事jeff Bell解释道:

以下是从[正式验证]的角度来看风暴如何工作的高级视图。首先，我们找出了我们想要证明的系统的属性......金宝博官方

基于我们对我们试图预防的共同错误来源的知识，我们在计划源代码中选择某些代码点，我们需要检查我们关心的属性实际上是真的......

不幸的是，在一个典型的程序中有许多这样的代码点，并且总是不容易找到需要在每个点上保存的确切属性。这正是StormBound玩家可以提供帮助的地方，所以请耐心听我解释……

我们在各种情况下运行系金宝博官方统的一系列次要旨在锻炼系统，因为它将在真实世界中使用它。正如我们所有这些时间运行所述金宝博官方系统，我们每次才能收集计算机内存中的数据的快照，每次该程序到达我们所识别的代码点之一。

这为我们提供了计算机内存中数据的大量示例。现在，我们希望在运行程序时达到相同的代码点时，我们希望识别有关每个代码点的数据。这些共同的事情实际上是我们正在寻找的属性。这是一个重要的一点：事实证明，计算机并不总是善于找到这些“共同点”，但人类非常擅长寻找模式，特别是视觉模式。

这便是《StormBound》游戏的切入点。实际上，每个游戏关卡都是由内存中特定代码点所包含的数据组成的。当你玩一个关卡时，你要在数据中寻找共同的模式。游戏向你展示数据(我们认为这是一种有趣且具有视觉吸引力的形式)，并允许你以各种方式“试验”数据，从而帮助你找到那些常见的模式。你在风暴束缚中使用的法术描述了模式。在(形式验证)世界中，我们称这些咒语为断言。我们将同一游戏级别的许多玩家发现的断言组合在一起，从而使我们使用的[正式验证]工具能够在相应的代码点证明所需属性的真实性。

到目前为止有多少玩家玩过StormBound ?他们有没有发现一些你认为自动搜索算法很难找到的东西?

亚伦坟墓：在这一点上，我们有数千名球员，他们统称超过100,000种模式（最终成为关于计划状态的逻辑断言）。目前可用的游戏是两个阶段中的第一个，并且允许玩家描述一个相对限制的断言。通常，我们在第一阶段收集的断言相对简单，并且可能使用自动化技术可发现。然而，在广泛的游戏中获得当前的游戏迭代已经教会了很多关于让玩家聘用的东西（或导致他们失去兴趣），也让我们了解对这些结果的理解we need to get from players but that aren’t encouraged (or, in a few cases, possible) with the current interface. We are using this information to design a second version that we expect will yield richer results beyond what automated tools would be likely to produce.

路加福音： 说得通。这是标准的硅谷智慧：发射最低可行的产品，迅速学习，迭代等。

你怎么知道风暴，甚至是CSFV完全（如果你正在运行它），已经成功或失败了？据推测，人群源正式验证援助的实质性可能与当前验证技术和问题相似的任何东西？

亚伦：我不能对DARPA发表谈论他们如何计划衡量该计划的成功，但我可以说我们如何知道我们如何知道我们如何成功验证特定的软件。典型验证技术的一个优点是完成了一个相当清晰的完成度。验证工具通常接受程序源代码加上代码的所需属性的一些语句。然后，该工具将尝试通常自动证明代码确实具有这些属性。如果他们成功，那么有很高的概率（不是100％，因为工具可能具有错误，本身），代码具有所需的属性。

StormBound构造成生成C代码的注释，该代码被发送到名为FRAMA-C的复杂工具。这些注释与一些内置定义相结合，描述了缺乏共同的安全漏洞。通过使用FRAMA-C，StormBound已经使用了最先进的验证技术。我们的目标计划是对互联网基础设施至关重要的大块开源软件，因此我们也与现实世界的问题合作。

那是一个关键问题：风暴会生成必要的注释，以允许验证成功吗？在第一阶段，我们发现玩家已经提出了一些有用的注释，但是错过了完整证明所必需的别人。在第二阶段，我们将更新游戏，以在面向游戏的术语中更新有关最终验证目标的显着上下文，我们预计这将导致更多参与者构建提供显着验证进度的解决方案。

路加福音：您编写“我们的目标程序是互联网基础架构至关重要的大块开源软件......”

是否对正式验证是否可能捕获的意见Heartbleed虫子在OpenSSL吗?

亚伦：是的，任何能够证明缺乏未定义行为的声音验证工具，如FRAMA-C，都未能证明Openssl是安全的。根据所使用的工具，该证明失败可能或可能无助于您识别错误的性质，但至少表明某些排序的一些错误存在，以及关于其粗略位置的一些错误。犹他大学计算机科学教授John Regehr写得很好博客其中特别提到了使用Frama-C来进行验证。

The key complication is that, in order to prove that such bugs don’t exist, tools like Frama-C require a lot of extra information from the programmer (or from game players, in the case of StormBound), encoded as annotations in the source code. In general, the effort required to create those annotations can exceed the time taken to write the program in the first place, and the process requires familiarity with verification tools, which is not widespread. We hope that StormBound will be able to significantly reduce the necessary effort and expertise, to the point where it becomes practical.

路加福音：您目前的猜测是如何普遍普通的CSFV从现在开始的5-10岁？一旦它们比在这些早期在这些早期的情况下，它们可能会如何适应一系列验证挑战的广泛攻击。

亚伦5-10年内会发生很多事情，所以我的答案是推测性的，只是反映了我自己的观点，而不是DARPA或者StormBound团队的其他成员的观点。

在过去的十年中，在可以通过计算机可靠地检查的数学证据的交互式建设工具方面取得了重大进展。从本研究中出现了一些非常一般和强大的工具，如ACL2，COQ，Isabelle和PVS。金宝博娱乐（大多数人最初也比上一年更早地创造，但最近的方法已经变得越来越大。）这些工具已被用于软件验证中的重要事业，以及一般数学，导致简单的证明用手不可行（正确地）。但是，这些工具对于用于现实软件系统的证明，这些工具是耗时的，需要罕见的专业知识。金宝博官方

我们一直在考虑下次修订风暴借款的下一步，从这些互动定理普通的技术支撑，结果，结果是相当一般的。虽然暂定的设计构建了这些想法，但它通过现有工具使用的界面提供了非常不同的界面，我们希望这将允许人们在没有相同程度的数学背景中证明至少一些定理。

目前，关键是未知的是没有数学背景的玩家将如何能够发展进步所需的直觉。目前的设计草图在许多地方使用视觉模式识别代替标准的数学推理技术，但典型的数学定理证明仍然依赖于基于多年的经验的深度洞察力。与此同时，验证软件的一些基本安全属性所需的证据通常远不得比数学家花时间的错综复杂。

所以，为了最终找到答案，我可以在未来十年看到几个可能的结果。我们可以有一个显著不同的交互定理证明界面，这可能会使专家用户更有效率。然而，一个更令人兴奋的可能性是，我们可以有一个系统，允许非专业人士通过识别模式和应用一些相对简单的规则来尝试证明本质上任何数学定理。金宝博官方在任何一种情况下，我希望结果将比简单地证明软件的安全属性更加普遍。

路加福音：谢谢，亚伦！