一篇科学文章发表在《 ACM通讯》上 ，2018年10月，第61卷，第10期，第68−77页，doi：10.1145 / 3230627

2017年2月，一架直升机从波音在亚利桑那州的飞机跑道上起飞，执行的通常任务是：在最近的山丘上飞行。 他完全自主地飞行。 根据美国联邦航空管理局的安全要求，飞行员没有触摸控件。 这不是该公司称为无人小鸟（ULB）的第一架自动驾驶飞机AH-6。 他已经像这样飞行了很多年了。 但是，这次是在飞行途中，直升机遭到了网络攻击。 车载计算机攻击了摄录机的恶意软件，以及通过受感染的闪存驱动器传播的病毒，该病毒是在维护期间插入的。 这次袭击威胁了某些子系统，但不会影响飞机的安全运行。

关键思想

• 来自经过验证的微内核的软件体系结构的正式证据可以廉价地扩展到实际系统。
• 同一系统中不同级别的安全性和可靠性是可能的并且是期望的。 不必确保整个代码的最大可靠性。
• 适度的重新设计和重构足以将现有系统提高到高度可靠的代码水平。

您可能会认为，军用航空很容易击退这种网络攻击。 实际上，由DARPA委托的一支专业的测试人员团队，作为开发高度可靠的军用计算机系统的计划的一部分，在2013年成功开发了高保证网络军事系统（HACMS），成功破解了第一版ULB软件，该软件最初是为确保飞行安全而非保护而开发的来自网络攻击。 黑客有机会使直升机坠毁或将直升机降落在他们希望的任何地方。 因此，很难估计乘客登机受到此类攻击的风险，并且2017年2月的一次未成功的黑客尝试表明该软件发生了一些根本变化。

本文介绍了这些更改以及使之成为可能的技术。 这是作为HACMS计划的一部分开发的一项技术，旨在确保关键系统在敌对的网络环境中（本例中为几种自动驾驶汽车）的安全运行。 该技术基于正式的软件验证-这些程序具有经过自动验证的数学证明，并可以根据其规格运行。 尽管本文并未专门讨论形式化方法本身，但它说明了如何在实际中使用工件验证来保护实际系统。

HACMS的最令人印象深刻的结果可能是该技术可以扩展到现有的真实系统，从而大大提高了其抵御网络攻击的能力。 该过程称为“地震安全改造”，类似于地震建筑物的升级。 此外，大部分的重新设计工作都是由波音工程师而不是正式的验证专家完成的。


无人试飞中的“鸟”

并非所有的直升机软件都基于数学模型和证据。 正式验证领域尚未准备好达到如此规模。 但是，HACMS计划已证明，将正式方法策略性地应用于整个系统的最重要部分，可以大大提高保护水平。 HACMS方法适用于仅通过在体系结构级别实施即可实现所需安全功能的系统。 它基于经过sel4验证的微内核，我们将在下面进行讨论。 除了明确定义的受系统安全策略约束的通信通道外，它还确保子系统之间的隔离。 通过CAmkES验证的系统组件框架，可以在体系结构级别上确保这种隔离。 使用Galois Inc.的特定领域语言。 CAmkES与Rockwell Collins和明尼苏达大学的架构分析工具以及高度可靠的软件组件集成在一起。

HACMS的成就基于软件工程师的忠实朋友-模块化。 创新之处在于形式化方法证明了接口的可观察性和模块内部构件的封装。 这种对模块化的严格遵守，使那些不是正式方法专家的工程师（如波音公司）可以创建新的甚至是现代化的现有系统，并实现高稳定性。 尽管这些工具尚未提供系统安全性的完整证据。

正式验证

程序的数学正确性的证据至少可以追溯到1960年代 ，但是很长一段时间以来，它们对软件开发的真正好处在范围和深度上都受到限制。 但是，近年来，在经过验证的C CompCert编译器到经过验证的seL4微内核（参见有关它的科学 文章 ）， CoCon验证的会议系统，经过验证的CakeML ML编译器，经过验证的程序方面，在实际系统的代码级别上，形式验证在形式验证方面取得了许多令人瞩目的突破。为了证明Milawa和Candle的定理， FSCQ验证的故障安全文件系统，验证的IronFleet分布式系统以及验证的CertiKOS并行内核框架 ，以及 数学定理，包括四种颜色的问题， 开普勒假设的自动证明和奇数阶的信念-汤普森定理 。 所有这些都是真实的系统。 例如，CompCert是一种商业产品，seL4微内核用于航空和无人飞机，作为物联网的平台，而CoCon系统已在众多大型科学会议中使用。

这些验证项目需要大量的精力。 为了使正式方法公开可用，这些工​​作需要减少。 在这里，我们展示了形式化和非正式方法的战略性组合，形式化方法的部分自动化以及精心开发的软件以最大程度地发挥隔离组件的优势，这使我们显着提高了系统的可靠性，该系统的总体大小和复杂性比上述提到的要大几个数量级。

请注意，我们主要对系统安全性所依赖的代码应用形式验证。 但是还有其他好处。 例如，证明代码正确的证据是对代码执行环境的假设（例如，硬件行为和软件配置）。 正式验证使这些假设变得明确，这有助于开发人员专注于其他验证工具，例如测试。 另外，在许多情况下，系统包括已验证和未验证的代码。 在代码审阅，测试和调试期间，形式验证就像镜头一样，专注于未经验证的关键系统代码。

硒4

让我们从构建可证明可靠的系统的基础开始-操作系统（OS）的内核。 这是以经济有效的方式保证整个系统可靠性的最重要部分。

seL4微内核提供了一套经过正式验证的用于实施安全系统的最小机制。 与标准内核不同，它有目的地是通用的，因此适合于实现许多安全策略和系统要求。

开发seL4的主要目标之一是在运行于内核之上的互不信任的组件之间提供强大的隔离。 例如，它可作为整个Linux操作系统的管理程序来支持，同时将它们与可以协同工作的安全关键组件隔离开来，如图1所示。特别是，此功能允许系统开发人员使用带有隐藏功能的旧组件。高度可靠的组件旁边的漏洞。


图 1. seL4中的隔离和受控通信

seL4核心在通用微核中占据特殊位置。 它不仅在同类产品中提供了更好的性能 ，而且在人类历史上，它的10,000行C代码经过了比人类历史上任何其他公共可用软件更严格的形式验证，不仅包括证明行，而且还包括可靠的属性。 它基于C核心实现的“功能正确性”的证明。 它可以确保内核的任何行为都可以通过其正式的抽象规范来预测：请参阅在线应用程序以了解该证据的外观。 遵循这一保证，我们增加了其他证据，将在介绍原子核的基本机制后进行解释。

seL4 API

seL4内核提供了用于实施安全系统的最少机制集：流，功能管理，虚拟地址空间，进程间通信（IPC），信令和中断传递。

内核将其状态保留在“内核对象”中。 例如，对于系统中的每个线程，都有一个“流对象”，用于存储有关剪切，执行和访问控制的信息。 用户空间程序只能通过所谓的“功能”或“功能”间接引用内核对象，这些功能将到对象的链接与对它的一组访问权限组合在一起。 例如，一个线程如果不具有相应线程对象的“能力”，则无法启动或停止另一个线程。

线程通过进程间通信“端点”发送消息来进行交互和同步。 一个能够发送到相应端点的线程可以将消息发送到另一个可以接收到此端点的线程。 通知对象在二进制信号集之间提供同步。 虚拟地址转换由表示页面目录，页面表和框架对象的内核对象或相应处理器体系结构对象上的微妙抽象控制。 每个流都具有一定的“ VSpace”功能，该功能指向流地址转换对象树的根。 功能本身由内核管理，并存储在位于图结构中的“ CNodes”内核对象中，该对象将链接映射到具有访问权限的对象，类似于将虚拟页表与内存中的物理地址进行比较。 每个线程都有自己的能力来标识根CNode。 从此根开始可用的功能集，我们称为“ CSpace Stream”。 能力可以通过作业转移通过端点转移，也可以使用通用CSpace声明为共享。 图2显示了这些内核对象。


图 2. seL4系统中的内核对象，其中两个线程通过端点交互

安全证据

由于其多功能性，seL4内核API是低级的，并支持高度动态的系统架构。 因此，很难获得这些API的直接证据。

访问控制策略的高级概念从单个对象和内核功能中抽象出来，而是使用一组抽象的“主题”（组件）以及它们各自对其他对象的权力来捕获系统的访问控制配置（例如，读取数据和发送消息） 。 在图的示例中。 如图2所示，组件A和B在端点上获得了授权。

Sewell及其同事证明，seL4访问控制策略可确保遵守两个基本安全功能：特权限制和完整性。

权限限制意味着对于将来的任何状态，访问控制策略都是系统中特定功能和内核对象的静态（不变）安全近似值。 此属性意味着，无论系统如何发展，任何组件都不会获得比访问控制策略所预计的权限更多的权限。 在图2中，组件B的策略没有对组件A的写访问权限。因此，组件B将来将永远无法获得此访问权限。 此属性表示在策略级别进行推理是对系统中访问控制的特定状态进行推理的安全近似。

完整性意味着无论组件做什么，它都将永远无法更改系统中的数据（包括它可以进行的任何系统调用），因为该数据显然不允许更改访问控制策略。 例如，在图2中。 如图2所示，A对另一个组件的权限的唯一组成部分是向组件B接收信息的端点发送数据的权利，这意味着组件A只能更改其状态，线程B的状态以及消息缓冲区的状态。 它不能更改系统的其他部分。

当一个组件未经许可无法从另一个组件读取信息时，完整性的副作用就是机密性：这是seL4非传递性非干扰的强大特性。 也就是说，在正确配置的系统中（除了完整性方面有更严格的限制），没有任何组件未经许可就无法找到有关另一个组件或其执行的信息。 证明是根据信息流策略来表达此属性的，信息流策略可以从完整性证明中使用的访问控制策略中提取。 只有在政策明确允许的情况下，信息才会被传输。 该证明涵盖了显式信息流以及内核中潜在的隐藏存储通道。 但是同步通道不在其范围内， 必须通过其他方式进行处理 。

seL4中的进一步证据包括功能正确性的扩展，因此， 对于ARMv7体系结构 ，安全性定理扩展到二进制级别，而对于内核（ 1、2 ），最坏情况的运行时配置文件则是实时系统必需的。 seL4内核可用于各种体系结构：ARMv6，ARMv7 ARMv7a，ARMv8，RISC-V，Intel x86和Intel x64。 目前，它已经通过了针对整个验证堆栈的ARMv7体系结构以及具有用于功能正确性的hypervisor扩展的ARMv7a的机器测试。

架构安全

上一节介绍了seL4内核为可证明可靠的系统奠定坚实基础的编程方法。 内核构成了可靠的计算基础（TCB），这是软件的重要组成部分，必须正确运行才能确保系统安全。 在实际系统中，这个基础远不只是一个微内核。 为了获得与内核相同的置信度，有必要验证其他软件堆栈。 但是，有些类别的系统不需要进行此类验证：它们需要在内核级别进行隔离定理，才能在系统级别获得某些安全属性。 本节提供了这样一个系统的示例。

在这些系统中，组件体系结构已经实现了关键属性，也许还有几个小型的受信任组件。 我们的示例是四旋翼飞行控制软件，这是前面提到的HACMS程序中的演示设备。

图3显示了直升机的主要硬件组件。 该架构有意比四轴飞行器所需的架构更为复杂，因为它被认为可以代表ULB，并且在此抽象级别上类似于ULB的架构。


图 3.自动驾驶飞机的架构

该图显示了两个主要计算机：一个与地面站通信并控制车载软件（例如摄像机）的车载计算机，以及一个用于控制车辆的飞行，读取传感器数据和控制引擎的导航计算机。 计算机通过内部网络或直升机上的CAN总线，ULB上的以太网连接。 直升机还具有不受保护的WiFi点，这使得可以演示其他保护方法。

在此示例中，考虑车载计算机。 为此必须满足四个基本属性：

• 对地面站的命令进行适当的认证；
  
• 加密密钥的私密性；
  
• 没有用于导航计算机的其他消息；
  
• 来自其他机载系统的不可靠软件不会影响设备的飞行。

可行的假设是，相机不可靠，可能受到威胁或是恶意的，其驱动程序和过时的软件以及任何外部通信渠道都可能受到损害。在此示例中，我们假定加密正​​确且强大，即无法提取密钥，并且超出了抑制敌人与地面站的无线电通信的任务范围。

图4显示了如何设计直升机架构来提供这些属性。Linux虚拟机（VM）充当旧式机载设备软件，相机驱动程序和WiFi热点的容器。我们将密码控制模块隔离在其自己的组件中，并与CAN总线，地面站通道和Linux虚拟机连接，以将数据发送到地面站。加密组件的任务是通过堆栈的CAN接口将（仅）授权消息发送到车载计算机，并将诊断数据发送回地面站。无线电组件发送和接收由加密组件加密和解密（带有身份验证）的原始消息。


图4。简化的四轴机载计算机架构

设置系统的所需属性的过程仅限于隔离性和体系结构（在信息流方面）的行为，以及单个受信任密码组件的行为。假定此组件的行为正确，则不会破坏密钥，因为没有其他组件可以访问它们。 Linux和图1中的加密组件之间的通道。 4仅用于消息传递，不提供对内存的访问。由于密码组件是与总线的唯一通信，因此只有授权的消息才能进入CAN总线。作为Linux虚拟机一部分的不可靠软件和WiFi被组件隔离封装，并且只能通过受信任的加密组件与系统的其余部分进行交互。

不难想象，通过检查更高级别的机械推理模型和工具，可以在很大程度上将这种架构分析自动化。正如MILS系统所指出的那样，这种体系结构中组件的边界不仅是分区和代码管理的便捷工具，而且通过强制隔离，可以为系统行为的形式化推理提供有效的边界。但是，这完全取决于最终二进制系统实现中运行时组件边界的正确应用。

先前讨论的seL4内核机制能够提供这样的实现，但是机制的抽象级别与体系结构方案的方框和箭头形成鲜明的对比：比体系结构方案更抽象的访问控制策略仍然包含更多的细节。在这种规模的真实系统中，软件会创建数以万计的内核对象和“功能”，并且配置错误可能会导致安全漏洞。然后，我们讨论了如何不仅使这些代码的配置和创建自动化，而且还如何自动证明与体系结构边界的一致性。

组件视图验证

由于通过安全策略的正式抽象简化了安全证据，因此抽象也有助于系统设计。组件Camkes平台运行在底层内核机制之上的seL4抽象上，提供通信原语并将系统分解为功能单元，如图2所示。5.使用该平台，系统架构师可以根据seL4来设计和构建系统，这些系统可以通过诸如远程过程调用（RPC），数据端口和事件之类的连接器相互交互并与硬件设备进行交互。


图 5. CAmkES工作流程

代码生成

在内部，CAmkES使用seL4中的低级内核对象来实现这些抽象。每个组件包含（至少）一个流CSpace和VSpace。 RPC连接器使用终结点对象，并且CAmkES生成中间代码来处理消息并将其发送到IPC终结点。同样，数据端口连接器是通过共享内存（两个组件的地址空间中存在的通用帧）实现的，可以选择限制数据传输的方向。最后，事件连接器是使用seL4通知机制实现的。

CAmkES还生成语言capDL的对象的初始配置的低级别的说明书和系统内核的功能。该规范成为seL4初始化程序的输入，它在加载后首先启动，并执行必要的seL4操作以创建实例并初始化系统。

因此，组件平台无需开发人员的额外努力即可生成代码。组件体系结构描述了一组方框和箭头，实现任务归结为仅填充字段。平台生成其余部分，提供所描述体系结构的实现。

在具有传统组件的平台上，生成的代码将扩展系统的可信计算基础，因为它会影响组件的功能。但是，CAmkES也会产生证据。

汽车证据

生成“中间”代码时，CAmkES在Isabelle / HOL中生成形式证明，在翻译过程中进行验证，并证明生成的“中间”代码符合高级规范，并且生成的capDL规范是CAmkES描述的正确规范。我们还证明了seL4初始化程序可以在所需的初始配置中正确配置系统。同时，我们在不扩展可信计算基础的情况下使系统的大多数构建自动化。

开发人员很少关注代码生成器的发布；他们只对功能和业务逻辑感兴趣。我们还假定不需要验证中间代码的证据，也就是说，开发人员可以专注于证明自己代码的正确性。正如生成的CAmkES标头为开发人员提供了用于生成的代码的API一样，顶级引理运算符也生成了一个API作为证明。Lemmas描述了连接器的预期行为。在RPC中间件示例中，如图 6生成函数$$f提供了一种调用远程函数的方法$f$$$g在另一个组件中。要保存抽象，请致电$g$$$f应该等同于调用$f$$$$g$ 。 系统生成的引理可确保 $$生成的RPC代码中的 f行为类似于直接调用$f$$$$g$ 。


图 6.生成的RPC代码

对于系统生成的证据的实际使用，它们必须与用户提供的（几乎）任意证据（就功能而言）组成$$g，以及其中的上下文$g$$$$g$ 和 $$$f$ 。为了实现这种可组合性，可通过用户提供的远程功能规范对连接器规范进行参数化。这样，工程师可以通过为其组件提供规范和证据来推理其体系结构，并依靠所生成代码的规范。

到目前为止，我们已证明从开始用专用连接器CAmkES RPC（结束此过程1，2）。由于其他连接器（数据端口和事件）的模板比RPC简单得多，因此扩展证据生成器以支持这些连接器并不困难，这将使您可以创建更多不同的经过验证的系统。

在通信代码之后，CAmkES创建初始访问控制配置以应用体系结构的边界。为了证明这两个系统描述（capDL和CAmkES）彼此匹配，请考虑将CAmkES描述作为capDL描述的抽象。我们使用先前测试的框架从capDL描述中得出一个对象相对于另一个对象的权限。因此，我们将把证据增加到政治层面。另外，我们在CAmkES描述中定义了在组件之间撤回权限的规则。此证明可确保以特权图表示的capDL对象（按组件分组的对象）在组之间的边界与等效的CAmkES组件图中的边界相同。直观地讲，边界的这种对应关系意味着从CAmkES描述中分析策略体系结构将保存由capDL生成的描述中的策略，从而保证了满足权限，完整性和机密性的要求，如前所述。

最后，为了证明正确的初始化，CAmkES使用了一个通用的初始化程序，该初始化程序在加载后作为第一个用户任务启动。在seL4中，此第一个（也是唯一的）用户任务可以访问所有可用内存，并根据capDL的详细说明使用它来创建对象和“功能”，并接受它作为输入。事实证明执行初始化程序后的state满足指定规范中描述的状态。该证明适用于确切的初始化器模型，但尚未在实现级别使用。与其他证据链的深度相比，此限制似乎较弱，但它已是比一般安全评估标准的最高级别（EAL7）所需的正式证据。

地震安全升级

实际上，为了安全起见，很难从头开始开发系统；因此，升级旧软件的能力对于开发安全系统至关重要。我们的基于seL4的框架支持称为“地震安全性升级”的迭代过程，因为常规建筑师会升级现有建筑物以提高地震稳定性。我们以无人直升机的现有软件体系结构逐步适应为例，从传统的测试方案转变为具有正式方法支持的定理的高度可靠的系统，以说明这一过程。尽管此示例基于真实的ULB项目，但此处已对其进行了简化，并不包含所有详细信息。

直升机的原始架构与图1中描述的架构重合。3.它的功能由两台单独的计算机提供：导航计算机控制实际飞行，机载计算机执行高级任务（例如与地面站进行通信并从摄像机导航图片）。车载计算机的最初版本是Linux的整体应用程序。在现代化过程中，波音工程师采用了HACMS合作伙伴提供的方法，工具和组件。

步骤1.虚拟化

第一步是按原样使用系统，并在安全虚拟机管理程序之上的虚拟机中运行它（请参见图7）。在地震现代化的比喻中，这对应于将系统置于更具移动性的基础上。此系统中位于seL4顶部的虚拟机由一个CAmkES组件组成，该组件包括虚拟机监视器（VMM）和来宾操作系统（在本例中为Linux）。内核提供虚拟化硬件抽象，而VMM为虚拟机管理这些抽象。 seL4内核不仅限制了来宾操作系统，还限制了VMM，因此您无需信任VMM实现即可提供强制隔离。 VMM故障将导致来宾OS发生故障，但不会导致整个系统发生故障。


图7.一台虚拟机中的所有功能

, , . MMU IOMMU . , . 1 2.

2.

地震现代化的第二步是加固现有的墙壁。 在软件中，开发人员可以通过将源系统划分为几个子系统来提高安全性和可靠性，每个子系统都由仅运行部分源系统代码的虚拟机组成。 每个VM / VMM组合都是在单独的CAmkES组件中执行的，该组件在不同子系统之间引入隔离，不允许它们相互影响，然后允许不同安全级别共存。

通常，这些部分遵循现有的软件体系结构，尽管如果该体系结构不足以有效隔离，则可能需要重新设计。

通常，各部分应相互交互，因此在这一点上，我们还将添加通信通道。 为了确保安全性，这些接口必须狭窄，将分区之间的连接限制在绝对必要的范围之内。 此外，接口协议必须高效，并且消息或数据量最少。 seL4允许您控制和限制分区之间的内存交换，以最大程度地减少数据量，这一点至关重要。

除了代表源系统子系统的虚拟机之外，我们还提取并实现任何共享资源（例如网络接口）的组件。

您可以重复第2步，直到我们达到了所需的部分。 正确的细节一方面是绝缘强度与另一方面增加的通信开销和重建成本之间的折衷。

在我们的示例中，我们分为三个部分：虚拟机，该虚拟机实现运行Linux的地面站的通信功能； 实现基于摄像机的导航功能的另一个虚拟机（也运行Linux）； 和本地网络共享组件，如图2所示。 8。


图8。 功能分为几个虚拟机

步骤3.本机组件

当系统分解为虚拟机的各个部分时，某些或所有单独的部分可以重新实现为本机组件，而不是虚拟机。 这将显着减少相同功能的攻击面。 将组件转换为机器代码的另一个优点是减少了负载并提高了生产率，消除了来宾OS以及代码执行和VMM通信的开销。

本机组件还增加了应用形式验证和其他方法来提高组件可靠性的可能性。 选项是不同的：从本机代码的完整功能验证到代码和证据的联合生成，模型验证，使用类型安全的编程语言，静态分析或对较小代码库的传统严格测试。

由于seL4和组件体系结构提供的隔离，因此可以在具有不同可靠性级别的组件系统中一起工作。 在这种情况下，低可靠性组件不会降低系统的整体可靠性，并且开发人员将受益于您无需花费时间来验证此代码的事实。

在我们的示例中，我们将分析虚拟机，将车载计算机和地面站之间的通信通道转换为本地模块。 在本机组件中，实现了通信，加密和控制功能（任务管理器）。 我们将把摄像机和WiFi留在虚拟机中，作为不可靠的过时组件（见图9）。 这种分离已成为改造子系统的努力与使用本机组件在性能和可靠性方面的好处之间的折衷。


图 9.在本机组件中实现的功能

步骤4.系统整体的可靠性

收到所有必要的模块后，我们将采取最后一步：根据体系结构和各个组件的可靠性对整个系统进行分析。

在HACMS的框架内，以可证明类型安全的面向对象语言Ivory实现通信，加密和控制模块，并在堆上分配固定数量的内存。 没有额外的验证，象牙色不能保证我们功能的正确性，但是可以保证容错能力和紧急可靠性。 考虑到组件之间的隔离，我们认为这些保证仍然存在于不可靠的组件（例如摄像机虚拟机）中。

网络组件是在标准C代码上实现的，该代码由平台的用户代码和现有的库代码组成。 它的可靠性级别对应于通过仔细执行众所周知的代码而获得的级别。 通过使用诸如驱动程序综合之类的方法以及诸如Ivory之类的类型安全语言，可以在不花费大量费用的情况下提高可靠性。 在对系统安全性的一般分析中，对网络组件的任何妥协只会影响网络数据包。 由于流量是经过加密的，因此这种攻击不会危害仅授权命令进入车载计算机的规范条件。

便携式摄像机的虚拟机是系统中最薄弱的部分，因为它在Linux系统上运行，并且应该包含漏洞。 但是虚拟机是孤立的，因此如果攻击者破解它，他们将无法转移到其他组件。 攻击者最糟糕的事情是将错误的数据发送到控制组件。 像在直升机中一样，此组件检查从相机接收的数据。 并且他成功地承受了本文开头提到的网络攻击。 这是一次“白盒”攻击，Pentesters团队可以使用所有代码和文档以及所有外部通信渠道。 她被故意授予了对摄像机虚拟机的root访问权限，从而模拟了对过时软件的成功攻击。 遏制攻击和防御这种非常强大的情况的能力成为对我们的安全要求以及对任何遗漏的假设，接口问题或研究团队可能无法识别的其他安全问题的识别的值得测试。

局限性和未来工作

本文提供了一种方法的概述，该方法用于通过组件体系结构应用安全功能的系统实现非常高的安全级别。 我们已经证明了有关内核级别及其正确配置的定理，以及一些定理，这些定理保证了组件平台根据其体系结构的描述正确地设置了安全边界，并为远程过程调用生成了正确的代码。 与系统的高级安全分析的联系仍然是非正式的，并且通信代码定理未涵盖平台提供的所有通信原语。 为了自动获得从头到尾覆盖整个系统的定理，需要进行其他工作。 但是，在此阶段很明显这是可行的任务。

提出的工作的主要目的是大大减少特定类别系统的验证工作。 此处描述的纯体系结构方法可以扩展到ULB以外的其他系统，但是明显受到以下事实的限制：它只能表达由系统组件体系结构确定的属性。 如果此体系结构在程序执行期间发生更改，并且属性严重依赖于太多受信任组件或太大组件的行为，则返回值将减少。

减轻这些限制的第一步是创建一个具有高可靠性的预测试组件库，以用作此类体系结构中的可靠构建基块。 该库可能包含可能由更高级别的规范生成的安全模式（例如，输入数据，输出过滤器，隐私和运行时监视器的消毒），以及可重复使用的加密模块，密钥存储，文件系统，高度可靠的网络堆栈和驱动程序。 如果安全性依赖于不止一个这样的组件，则需要证明其交互和共享的可靠性。 这里的主要技术问题是有关并发性和协议的讨论，以及在存在受信任组件的情况下的信息流。 尽管存在这些局限性，但这项工作证明了基于seL4的真正高度可靠的系统的快速发展。 当前，可以以比传统测试更低的成本来创建这样的系统。

应用：人工成本

seL4的设计和代码开发花费了两年的时间。 如果我们添加所有针对血清型的证据，则对于8700行C代码将总共获得18个人年。为了进行比较，来自seL4家族的同等大小的微内核L4Ka :: Pistachio的开发花了6个人年，并且没有提供明显的可靠性。 这意味着经过验证的软件与传统软件之间的开发速度差异仅为3.3倍。 根据Colbert和Bohm评估方法 ，针对8700行C代码按照传统EAL7标准进行认证将花费超过45.9个人年。 这意味着按照通用标准，二进制级别的实施形式正式验证已经比最高级别的认证便宜2.3倍，同时还提供了更高的可靠性。

为了进行比较，此处描述的HACMS方法仅使用每个新系统的现有证据，包括工具生成的证据。 因此，与这种方法相匹配的系统的一般证明工作归因于工时周，而不是数年，而测试仅用于验证假设。