本杰明·皮尔斯的安全架构

路加福音Muehlhauser:我以前采访Greg Morrisett关于安全工程，并关于计算机安全一般。你也为外管局的项目做出了贡献，并就该项目发表了"早期回顾"讲话(幻灯片)，我想问你一些有关它的更详细的问题。

特别是，我想问关于"验证信息流动结构为外管局开发的。你能给我们概述一下你能证明的关于这个系统的信息流安全特性吗?亚博体育苹果app官方下载

本杰明·c·皮尔斯:当然。首先，提醒您的读者:SAFE是一个全新的硬件/软件堆栈设计，其目标是构建一个对网络攻击具有高度弹性的网络主机。设计的一个支柱是跟踪信息流的普及机制。SAFE硬件提供了细粒度的标记，并在每个指令调度上有效地传播和组合标记。操作系统对这些通用工具进行虚亚博体育苹果app官方下载拟化，以提供“信息流抽象机器”，用户程序在其上运行。

形式验证从一开始就是SAFE设计过程的一部分。我们最初希望能够验证实际运行的操作系统代码的风格sel4，但我们发现，代码库太大，移动太快，对于一个小型验证团队来说，这是不现实的。相反，我们开发了一种结合了完整的正式验证的方法模型“基于属性的随亚博体育苹果app官方下载机测试”系统的主要特性(一个拉QuickCheck)的更丰富的系统功能子集。亚博体育苹果app官方下载

我们的最有趣的形式证明到目前为止，我们在SAFE硬件上的实现正确地保存了信息流抽象机器的关键安全属性——一个程序的秘密输入不能影响它的公开输出。这很有趣，因为抽象机器的行为是通过硬件“规则缓存”和软件层之间相当复杂的相互作用来实现的，软件层根据需要通过咨询当前安全策略的符号表示来填充缓存。因为这个机制位于SAFE架构安全保证的核心，所以我们想要完全确定它是正确的(它确实是正确的!)

路加福音你提到，由于你不能用你的可用资源正式地验证整个操作系统，你只能正式地验证系统的关键特性模型，并使用基于属性的随机测试系统的其他一些功能。亚博体育苹果app官方下载与拥有成功验证整个操作系统的资源相比，这种方法为系统安全性提供了多大程度的主观自信(投注几率)?亚博体育苹果app官方下载(一个粗略的“直觉猜测”是可以接受的!)

便雅悯假设一个未经验证但经过良好设计和道路测试的系统在安全级别上得到1分，而一个完全验证的操作系统得到8分。亚博体育苹果app官方下载让我们假设我们谈论的是SAFE的完成和优化版本(认识到我们现在拥有的是一个不完整的原型)，以及核心机制模型的正确性证明和一些较大组件的随机测试。我的直觉认为这个系统在这个尺度上可能是4。亚博体育苹果app官方下载我们所做的证明在范围上是有限的，但是它们在加深我们对核心设计的理解和指导我们实现一个干净的方面是非常有用的。

为什么我的最高等级是8而不是10?因为即使有一个完整的机器检查的正确性证明，也不意味着你的操作系统真的是无懈可击的。任何证据都是基于假设的——例如，硬件的行为是正确的，而如果攻击者有一个吹风机和物理访问CPU，这可能就不是事实了!因此，要获得高于8的值，就需要额外确保潜在损害的程度是有限的即使你的正式假设被打破了。

这表明了一种纵深防御策略。我们的目标在设计安全软件,使“omniprivileged”部分的代码(例如,部分可能导致机器做任何事情,如果攻击者可能会以某种方式让它表现不好)尽可能小,远远小于传统操作系统甚至明显小于微核。亚博体育苹果app官方下载检查安全策略和填充硬件的代码缓存规则是高度特权,垃圾收集器在我们当前的设计,但我们相信,剩下的操作系统可以写成一组“车厢”更有限的特权,使用标签的硬件来实现组件之间的分离。(证明这种说法正在进行中。)

路加福音:我曾与一些对正式验证是否能在很大程度上提高安全性持怀疑态度的人交谈过，因为很多安全问题来自于对漏洞的理解不够充分，无法在系统的正式需求中捕获所有漏洞，亚博体育苹果app官方下载而不是来自一个与设计规范不匹配的系统，而这种匹配可以通过亚博体育苹果app官方下载形式验证来捕获。然而，您似乎认为经过验证的系统比未经验证的系统安全得多。亚博体育苹果app官方下载你对此有什么看法?

便雅悯:是的,在其他条件相同的情况下我会把相当多的钱在一个验证系统比一个未经证实的——不是因为安全验证过程消除漏洞的可能性没有被认为是在规范,而是因为的过程亚博体育苹果app官方下载写作正式的规范要求有人坐下来仔细考虑至少系统试图实现的一些(安全性和其他)属性。亚博体育苹果app官方下载至少对其中一些问题有一个清晰的了解总比什么都没有好!

实际上，证明系统与规范相匹配会增加更大的价值，因为规范本身是复杂的工件，需要调亚博体育苹果app官方下载试的程度和指定的系统一样多!但是基于属性的随机测试——即，检查系统是否满足大量分布良好的随机输入的规范——可以是一个非常有效的中间步骤，以相对较小的亚博体育苹果app官方下载代价获得很大一部分效果。

路加福音:一般来说，你认为需要“高保证”安全或安保(相关的)的高度复杂的系统，需要“从头开始”为安全亚博体育苹果app官方下载或安保设计，以获得这样的高保证吗?或者，是否有很多情况下，一个高度复杂但高度保证的系统可以通过优化开发的一般性能，然后“修补”系统的安全性和安全性成功开发?亚博体育苹果app官方下载

并且，您是否猜测在您自己的子字段(s)和其他相邻的子字段中，这个问题最常见的回答可能是什么?

便雅悯当然，这取决于你所说的“高保证”是什么意思!相当多的人对这个术语下了定义只有适用于使用从第一天开始就考虑安全性和/或安全性的方法开发的软件。但是，即使我们对HA有一个更广泛的定义——“提供非常好的抵抗恶意渗透和灾难性故障”，或者诸如此类的东西——我的感觉是，这是非常难以改造的。

我个人在构建Unison时非常清楚地看到了这种效果，这是我在几年前与Trevor Jim和Jérome Vouillon一起开发的跨平台文件同步工具。在Unison之前，我已经做了几个同步器，但我总是发现行为似乎有问题的边缘情况，所以我们开始设计Unison时，试图写下一个非常精确(尽管大大简化了)的核心行为规范。除了帮助我们理解边缘情况，这个练习还有巨大的影响我们写代码的方式。例如，规范说，在同步器运行结束时，要同步的文件系统的每个部分都应该是亚博体育苹果app官方下载同步(随另一副本更新)或不变从同步器开始运行时开始(例如，如果存在用户选择不解决的冲突)。但是，由于同步器可以以各种方式终止(正常结束、被用户终止、网络连接中断、一台机器重新启动……)，这个需求意味着文件系统必须处于这两种状态之一亚博体育苹果app官方下载在每一个时刻在执行期间。这是非常难以实现的:有许多地方的代码需要做额外的工作缓冲区的事情在临时位置,直到他们可以自动进入的地方,使用两阶段提交,确保内部数据结构不损坏,等等,等等,需要额外的工作,原因往往是非常微妙的。事先有了规范，我们就不得不在进行的过程中进行这项工作。后来再回去，重新发现所有我们应该格外注意的地方几乎是不可能的。

至于我研究领域的其他人可能会对你的问题说什么，我决亚博体育官网定调查一些朋友，而不是只是假设。正如预期的那样，我得到的大多数评论都是“让一个复杂的系统在事实发生后真正变得安全基本上是不可能的”。亚博体育苹果app官方下载但是也有一些人提出了可以算作例子的系统，比如SELinux亚博体育苹果app官方下载和Apache。(实际上，SELinux是一个有趣的例子。一方面，它的目标只是向Linux添加强制访问控制;它甚至明确地没有尝试增加Linux本身的安全性。因此，对于针对内核漏洞的攻击，SELinux并不比普通Linux更好。另一方面，我被告知，在某些情况下——特别是为了保护web应用程序和其他面向网络的代码免受HTTP请求的各种攻击——SELinux可以提供非常强大的保护。)

路加福音本杰明:谢谢,!