格文·克莱因论形式方法

突出了克莱恩的想法，从下面的采访中:

• 验证不是为验证而设计的代码是非常困难和昂贵的。这种“事后验证”也有其他缺点。
• 程序设计人员可以使用抽象、模块化和显式架构选择来帮助使复杂的系统对人类透明。金宝博官方
• 概率在验证中有两种作用:(1)直接概率推理，在逻辑或在程序本身是概率的情况下进行，或(2)标准的非概率推理与主观的不确定推理相结合，对保证系统按预期工作的总体概率意味着什么。金宝博官方
• 真正的自动系统似乎还有很长的路要走金宝博官方，但如果你能够创造一个具有真正意想不到的行为的系统，那么你就不能让它变得安全。

路加福音Muehlhauser:在你即将发表的论文中操作系统微内核的全面正式验证，您和您的合著者描述了您用来确保其验证是易于处理的内核设计(seL4)。您还讨论了保持正式证明最新的过程，“因为系统的需求、设计和实现[改变]了近十年。”金宝博官方

seL4微内核有多“微”?也就是说，它提供了什么样的标准功能，以及什么样的功能(在较大的OS内核中常见)实现了它不提供吗?

Gerwin克莱因它是相当微的:它是L4传统中一个真正的微内核。这意味着与传统的单片操作系统内核相比，它是非常小的:Linux有几百万行代码，seL4有10,000行C.代码。seL4只提供构建操作系统所需的核心机制。这些包括线程和调度、虚拟内存、中断和异步信号，以及同步消息传递。seL4最重要的特性可能是它强大的访问控制机制，可以与其他组件一起使用，构建独立的组件，它们之间进行受控通信。这些组件可以是小型的独立设备驱动程序，也可以是整个Linux客户操作系统，开发人员可以选择粒度。

其原理是:如果一种机制严格需要特权硬件访问来实现，那么它在内核中，但是如果它可以使用其他机制作为用户级任务来实现，那么它就在内核之外。seL4没有提供设备驱动程序、图形、文件和文件系统、网络堆栈、甚至磁盘分页，但可以在其之上实现。金宝博官方您(希望)得到的是，棘手的复杂性集中在内核中，用户级操作系统组件变得更加模块化。

路加福音如果一个操作系统的微内核不是从一开始就特别适合于正式的验证，那么有没有人可能正式验证一个seL4大小的操作系统微内核，或者任何一个相当复杂的计算机程序?

具有我不是说验证不是为验证而设计的代码是不可能的，但这会显著增加成本和工作量。因此，目前不太可能有人会做类似的验证，不是为它设计的。这种情况可能会在5-10年的时间里发生改变，因为技术会变得更强大，而付出的努力会减少。

但即使有可能，我也不认为这是可取的。我听说有人把这种过程称为“事后验证”，我同意这种普遍观点。在一切都完成之后才开始验证就太晚了。如果你在验证过程中发现了严重的问题，如果一切都已确定，你能做些什么呢?此外，如果您认真地想要构建一个可证明正确的系统或一个高保证的系统，您应该这样设计和规划它。金宝博官方有趣的是，敏捷方法也有相同的方向:它们从一开始就进行测试和验证，即使它们不使用正式的方法。

如果您能将验证成本考虑到您的开发过程中，您的设计选择将更倾向于使系统正确工作的原因更加明显。金宝博官方根据我们的经验，这不仅降低了以后验证的成本，而且还导致了更好、更优雅的设计。当然，在验证和性能等因素之间也存在紧张关系，但这并不是黑白分明的:您可以评估成本并做出明智的权衡，有时有一些解决方案可以同时满足两者。

路加福音你提到，在设计时考虑到验证可能会促使设计选择朝着“让系统正确工作的原因更加明显”的方向发展——这是一个我有时称之为“透明度”的重要问题，即“对人类工程师来说透明”。金宝博官方我在透明度和安全关键系统金宝博官方．

我在那篇文章中提出的一个“开放式问题”是:“方法的透明度如何随着比例而改变?”也许一个小程序在编写时考虑到验证，它会比类似复杂度的贝叶斯网络更透明，但是您认为这随着规模的变化而变化吗?如果我们能够扩展正式的方法来验证比seL4大10,000倍的程序，那么对于人类工程师来说，它会比一个相当复杂的贝叶斯网络更透明还是更不透明?至少我们可以查询Bayes网络来询问“它认为X是什么”，而对于正式验证过的系统，我们就不能这样做了。金宝博官方(你可能也会认为我对这些问题的定义是错误的!)

具有你所说的透明度可能与复杂性密切相关，复杂性往往随着规模的扩大而增加。在传统的系统设计中，有许多处理复杂性的方法，例如抽象、模块化和体系结构。金宝博官方所有这些都有助于正式的验证，并使其更容易规模化。例如，抽象将实现的复杂性隐藏在接口后面，并使谈论某个部分成为可能不知道系统金宝博官方全部的情况下。

早期的抽象的力量是伦敦地铁地铁交通图:它告诉你这列车去和与其他列车,它给你一个粗略的地理关系,但它并没有告诉你的弯曲轨道,精确每个车站在哪,或者是什么电台之间的地面上。作为一名乘客，你可以自信地驾驭一个相当复杂的火车系统，而不需要知道任何关于每一件东西如何工作和具体位置的金宝博官方更详细的机制。

在我们的seL4验证中，我们最初不能充分利用抽象，因为在微内核中所有东西都是紧密相关的。在较大的系统中，这就金宝博官方没那么必要了，部分原因是内核之类的东西可以提供模块和隔离。

从长远来看，我们甚至在seL4验证中也能从抽象中获益。我们首先验证了代码正确地实现了更高层次的规范，这是真正的内核代码的抽象。多年以后，我们使用了更简单的抽象，甚至不用看复杂的C代码，就可以证明它具有非常特定的安全属性，比如seL4尊重完整性和机密性。因为我们第一次证明了这个规范是代码的一个真正的抽象，并且因为我们感兴趣的属性被这种抽象所保留，所以我们也自动获得了代码的验证。在努力中取得的胜利是显著的:完整性验证比原始代码验证便宜20倍。

在我看来，认真利用这些原则将是扩大核查规模的途径。这已经是系统工程师为复杂但关键的系统所金宝博官方做的事情。使用它进行验证的方法是更紧密地使用它，而不是制造破坏抽象或绕过系统体系结构的方便异常。金宝博官方最后，让人类更容易思考一个系统的一切，都将有助于验证它。金宝博官方

路加福音:您写道:“在传统的系统设计中，有许多处理复杂性的方法，例如抽象、模块化和体系结构。”金宝博官方您给出了使用抽象和模块化验证复杂代码的例子——您对使用架构使复杂系统的验证更容易处理有什么想法?金宝博官方

具有是的，谢谢你发现。

我认为好的架构可以通过两种主要方式来帮助验证。首先，明确的体系结构和设计将告诉您系统中存在哪些模块或层，以及它们如何相互连接。金宝博官方明确这一点将使您能够得出关于系统的一些初步结论，甚至不需要查看代码。金宝博官方例如，如果两个组件没有相互连接，并且底层操作系统正确地强制体系结构，那么这两个组件将不能相互影响对方的行为，这意味着您可以独立地验证每个组件。金宝博官方您现在有两个更简单的验证问题，而不是一个更大的问题。

当您从一开始就将感兴趣的关键属性直接验证到体系结构中时，第二种方法就起作用了。例如，假设关键设备中有一个受信任的数据记录组件。您可能希望从该组件获得的属性是:它只访问自己的日志文件，它只写数据，从不读，系统中的其他组件不能向这些日志文件写入数据。金宝博官方要在单片系统中验证此属性，您必须证明所有具有文件写访问权限的组件不会覆盖日志文件金宝博官方，或者必须证明复杂文件系统的访问控制机制是正确的。您可以在任何写入者和文件系统之间放置一个附加的小过滤器组件，而不是完成所有这些工作:该过滤器将拒绝向日志文件写入的请求，并允许其他请求。金宝博官方这很容易实现，也很容易证明是正确的。现在，您已经将一个巨大的、可能不可行的验证任务减少为一个(希望如此)小的运行时成本和一个体系结构属性。

要让这些工作，您需要确保真正的代码最终确实遵循体系结构，并且体系结构的通信和保护结构是由底层系统强制执行的。金宝博官方这就是为什么我们的小组正在考虑这样的安全架构模式:正式验证的微核是以这种方式构建高保证系统的完美构建块。金宝博官方

路加福音我想了解一下你对我以前做过的事情的看法问Emil Vassev:我们可以在多大程度上用今天的正式验证方法来证明演绎保证和概率保证?如果我们能够将正式的规范和验证程序推广到演绎保证和概率保证，也许我们可以验证更大、更复杂、更多样的程序。

在今天正式验证过的系统中，许多安全性能的演绎证明已经是设计者的“概率”金宝博官方有一些主观的不确定性至于正式的规范是否准确地捕获了直观上想要的安全特性，以及(不太可能)证明中某处是否存在错误。

但我想问的问题是关于证明本身的明确概率保证。例子:计算的验证器可以代表它耗尽之前,可以证明或者反驳系统是否有财产X,但鉴于其推理和搜索过程到目前为止是80%相信系统属性X,有点像人类研究人员今天不能证明P = NP与否,金宝博娱乐金宝博官方但他们主观上有80%的信心认为P≠NP。也许要做到这一点，我们首先需要解决一个问题，即一个正式的系统或逻辑演算如何能够对逻辑句子有内部一致的概率信念(和信念更新)。金宝博官方一个拉Demski 2012或Hutter等人，2012)．

具有埃米尔已经给了这个问题一个很好的答案，所以我将尝试从一个稍微不同的角度来处理它。我认为概率可以在验证中发挥两种作用:你直接思考概率,它只是在逻辑或即使在设置程序本身的概率,经典或另一个原因,但正试图找出这意味着您的系统的总体概率将按预期工作。金宝博官方

这两种方法都有很好的例子，而且都很有用，即使是在同一个项目中。正如埃米尔所指出的那样，最好是运用充分的推理，有能力得出明确的结论。但是当这是不可能的，你可能会满足于至少一个概率答案。例如，有许多概率模型检查器棱镜从玛尔塔Kwiatkowska的或概率一致性引擎(四氯乙烯从斯里兰卡)。这些工具将允许您将概率附加到系统中的某些事件上，或将概率附加到关于世界状态的信念上，并从那里进行推理。金宝博官方概率一致性引擎与你在问题中提到的非常接近:调和关于世界的潜在冲突的概率信念，并从这些描述中得出概率结论。

也有一些程序和协议可以直接处理概率问题，比如通过抛硬币来做出某些决定。例如，Firewire协议就使用了这种机制，尽管使用了概率，但您仍然可以对其行为作出明确声明。卡罗尔摩根他在新南威尔士大学和我们一起工作，一直在将此类程序的概率推理应用于安全问题和程序建设。为了让你了解这个领域的可能性:我们的一个博士生，David Cock，最近在《伊莎贝尔》中使用了Carroll的方法来推理微内核中的隐蔽通道以及它们可以泄露信息的最大带宽。

最后，还有一个关于需求的不确定性和关于物理世界的不确定性如何适合形式验证的问题。SRI的John Rushby对这个问题有一个很好的看法在他关于可能完美系统的论文中金宝博官方安全案例中的逻辑和认识论．他的观点是，有两种不同的可能性需要考虑:系统是正确的可能性，以及我们对世界的潜在不确定性。金宝博官方例如，一个乌托邦式的完全验证系统，其中我们正确地捕获了所有需求，并且我们得到金宝博官方了所有完美的东西，如果其中一个物理组件由于磨损、磨损、过热或者因为某人把它扔进了火山，那么它仍然可能失败。

正式验证对后一种可能性毫无作用，但是它增加了系统完美的可能性(即使它永远不能完全达到)。金宝博官方我们可以使用这个概念来确定哪里验证的影响最大，并量化它的影响有多大。例如，正式验证一个系统可能没有多大意义，因为它周围的世界表现得太随机了，即使是可能的最佳解决方案也只有大约50%的时间是正金宝博官方确的。另一方面，在需求和系统可以被精确捕获的环境中，我们可以从正式的验证中获得巨大的回报。金宝博官方拉什比的方法让我们可以量化差异。

路加福音：莱维特(1999)他认为，随着智能系统变得越来越自治，并在越来越不确定、金宝博官方未知的环境中运行，将不可能完全用控制理论等工具来建模它们的环境和可能的行为:

如果机器人将被用于更广泛的用途，它们将需要在没有人类干预的情况下，在户外、道路上以及正常的工业和居住环境中运行，在这些环境中不可预测的事件经常发生。当机器人遇到意想不到的事件或模糊的感知时，停止机器人的动作是不现实的，甚至是不安全的。

目前，商用机器人主要通过控制理论的反馈来决定它们的行动。控制理论算法要求将世界上可能发生的事情的可能性用软件程序所体现的模型来表示，这些模型允许机器人预先决定对任何与任务相关的视觉事件的适当行动反应。当机器人在开放的，不受控制的环境中使用时，将不可能为机器人提供先天的所有可能发生的物体和动态事件的模型。

为了决定对世界上未建模的、意外的或模糊解释的事件采取什么行动，机器人将需要在受控反馈反应之外增加他们的处理能力，并参与决策过程。

因此，他认为，自主程序最终将需要决策理论。

你对这个预测怎么看?总的来说，您认为什么样的工具和方法对未来的高度自治系统实现高安全性保证最为重要?金宝博官方

具有在这个领域还有很多工作要做，我认为我们还没有很好的解决方案。毕竟，我们仍然在努力构建更简单的系统。金宝博官方

另一方面，我同意更多的自主性似乎是系统正在走向的方向。金宝博官方在美国国防部高级研究计划局的HACMS项目中Kathleen Fisher负责管理我们正在研究一些高保证自动驾驶汽车的方法。例如，您可以做的一件事就是使用所谓的simplex架构。您使用两个控制器:一个复杂的、自主的控制器和一个额外的、更简单的、您可以提供高保证的安全控制器。在正常运行时，复杂的自治控制器运行，并提供方便，甚至智能的行为。简单的安全控制器停留在后台并监控操作。它只检查车辆是否仍在安全参数范围内。如果发生了不可预见的事情，比如故障、安全攻击或复杂控制器中的缺陷，简单控制器将接管并将系统置于安全模式。金宝博官方对于自动驾驶飞行器来说，这可以是“飞回基地”，或者“安全降落在自由地点”。这个解决方案并不是万能的，但它是很好的第一步。

我们是否真的会开始构建基于独立推理的，具有自己意想不到行为的系统，我不能说。金宝博官方在目前的自动驾驶汽车(如自动驾驶汽车)或配送无人机等提案中，情况显然还不是这样。我很难想象监管机构会同意这样的事情(有充分的理由)。这些系统目前是为了安全处理各种各样的问题而构建的，而不是试图预测一切。金宝博官方例如，你不需要精确地知道自动驾驶汽车会遇到哪种障碍。你不需要知道它是一个动物，碎片，还是一个小孩。这足以让你看到有什么东西挡住了你的路，或者是在碰撞的过程中，并比人类更好地做出反应。你宁可过于谨慎，也不愿冒险。例如，要想改善人类驾驶员目前的状态，你不需要建立一个完美的系统。金宝博官方你只需要造一个比人类驾驶安全得多的。 That is a much simpler problem.

金宝博官方如果你能证明推理是合理的，并且你能探索你所期望的情况的暗示空间，那么能够进行自己推理的系统仍然是安全的。问题是，自动推理是困难的——不仅仅是复杂的思考，而是一个理论上困难的问题，即使是简单的问题也需要大量的计算能力。直接为复杂情况构建金宝博官方系统目前比这要容易得多，所以我想说的是，能够进行自己推理的自动程序更接近于科幻小说，而不是现实。阿西莫夫(Asimov)在他著名的机器人定律中发挥了这种远见，在他的故事中，这些定律常常导致令人惊讶的，但完全有效的行为(根据这些定律)。最后，如果您真的想构建一个具有真正意想不到的行为的系统，那么根据定义，您无法验证它是金宝博官方安全的，因为您只是不知道它将做什么。你必须和他们打交道，更像和人打交道，而不是和机器打交道。

路加福音关于如何实现高保证率人工智能系统的研究，你认为未来十年有哪些有前景的“下一步”?金宝博娱乐金宝博官方

具有在这个领域还有很多工作要做，我认为我们还没有很好的解决方案。毕竟，我们仍然在努力构建更简单的系统。金宝博官方

我认为诸如HAC金宝博娱乐MS项目的研究是令人鼓舞的:高保证的控制和传感算法，高保证的操作系统，不仅仅是内核，还包括更广泛的系统基础设施，允许架构驱动的方法和分析的高级设计工具，以及通常更强大的验证金宝博官方工具，将是使这些自主系统更可靠和更安全的关键。

如果我们能破解系统规模的下一个数量级，事情就会变得有趣得多。金宝博官方对于这种开发，有一些很好的方法:我们已经在从规范中合成更多代码并自动生成相应的证明方面取得了一些初步的成功，而不是试图寻找没有上下文的证明。如果这种方法在更大的规模上奏效，它将使未来构建高保障系统的成本大大降低。金宝博官方

路加福音:谢谢,Gerwin !