首发地址：http://trialley.top/pages/53ac44/
CSDN地址：https://blog.csdn.net/lgfx21/article/details/117606097
翻译与转发许可：

作者：Gernot Heiser gernot@sel4.systems

翻译：TriAlley lg139@139.com

翻译版本：1.2 2020-06-10

原文：https://sel4.systems/About/seL4-whitepaper.pdf

译者学识浅薄，文中许多专有名词和英语文化表达尚未明晰，均用括号标注英文原文。如果您有翻译建议，欢迎评论或邮件告知于我，不胜感激。

vuepress的markdown不支持引文，文中[^1]样式的字段表示在文末有相应参考文献

译注

翻译中出现了许多容易混淆的名词，且某些词组仅在本文档中初出现过，国内外都找不到其他出处。由于译者并不是专业翻译，也不是微内核从业者，因此对这些名词只能尽量进行进行合理的意译，不周之处还请批评指正。

1. security and safety
   1. security：包括防盗，防欺诈和篡改等。如data security数据加密防盗
   2. safety：指自身运行的安全特性。如data safety数据备份防丢失
   3. 在中文语境中，security和safety都可以指代安全，但英文中他们侧重不同。不同行业都使用这两个词语，但各领域对应中文翻译也不尽相同。译者综合分析，决定将security翻译为安全性，safety翻译为稳定性。
2. incremental cyber retrofit >> 渐进式模块化改造
   1. 内外网只能找到incremental retrofit这个词组，翻译为渐进式改造或增量改造
   2. incremental cyber retrofit 可以翻译为渐进式网格化改造，渐进式模块化改造？
   3. 最终译者决定翻译为渐进式模块化改造😁
3. hypervisor与VMM
   1. hypervisor是虚拟化层
   2. VMM通过虚拟化层控制VM
4. Capability 能力
   1. 参考https://gitee.com/laokz/sel4_reference_manual
5. communication channels
   1. 交流通道

摘要

本白皮书对 seL4 进行了介绍。我们将解释 seL4 是什么 (以及不是什么)，并探讨它的特性。我们将解释是什么使 seL4 有资格成为安全关键系统、通用嵌入式嵌入式和信息物理系统(Cyber-Physical System)所选择的操作系统内核。我们将解释 seL4 的安全故事(assurance story)、它的防盗和稳定(security and safety)相关特性以及它的基准性能。我们还讨论了典型的使用案例和已有系统的渐进式改造案例。

1 seL4 概述

seL4是微内核。

操作系统 (OS) 是一种控制计算机系统资源并提供安全性的底层系统软件。与用户态程序不同， OS 可以使用 CPU 的特权模式（kernel mode），这意味着 OS 可以直接访问硬件。而用户态程序只能使用用户模式（user mode），仅可以访问 OS 允许它访问的的硬件。

操作系统微内核是操作系统的最小化内核，它将高权限代码的数量降到最少。seL4 是 L4 微内核家族 的成员，这个家族可追溯到 90 年代中期. (seL4 和 seLinux没有任何关系)

seL4 是虚拟机管理器

seL4 支持运行客户操作系统 (如 Linux)。seL4 的交流通道(communication channels)使客户机和它的应用程序可以彼此通信，本地程序也一样（as well as with native applications. ）。

在第二章中了解更多关于 seL4 微内核的信息及其作为虚拟机管理器的使用方法。在第七章中了解真实世界的部署场景和现有系统改造方法。

seL4 的正确性验证

seL4提供了一个正式的、数学的、机器检查的形式化验证，这意味着就其规范而言，内核很大程度上上是“没有bug的”。事实上， seL4 是世界上第一个经过形式化验证系统¹。

seL4 是安全的

除了实现上的正确性之外，seL4还进一步提供了安全性验证²。在一个正确配置的sel4系统中，内核保证了机密性、完整性和可用性等经典的安全属性。关于这些证明的更多内容在第三章。

seL4通过能力进行安全高效的访问控制

能力是访问令牌，它可以对哪个实体可以访问系统中的特定资源进行非常细粒度的控制。他们根据最低特权原则(也称为最低权威原则，POLA)设计，提供强大的防盗能力。这是高安全系统的核心设计原则，在主流系统(如Linux或Windows)中是不可能实现访问控制的。

seL4 可作为稳定性硬实时操作系统

seL4是世界上唯一一个对最坏情况执行时间(WCET)进行了完整和合理分析的内核(至少在开放文献中)³⁴。这意味着，如果正确配置了内核，所有的内核操作在固定时间内完成，这是构建硬实时系统的先决条件。在硬实时系统中，如果不能在严格限定的时间内对事件作出反应，后果将是灾难性的。

seL4是最先进的混合关键系统

它为混合关键实时系统(MCS)提供了强大的支持。在这些系统中，关键活动与在同一平台上执行的不可信代码共存，要确保关键活动的时效性。一些成熟的MCS操作系统使用严格分区的时间和空间资源管理，seL4则通过更灵活的资源管理提高了利用率⁵。更多关于seL4的实时性和MCS特性见第5章。

seL4是最快的微内核

一般来说，速度和安全二者不可兼得，seL4的独特之处在于它全都要。seL4支持广泛的现实世界用例。无论安全性多重要重要，卓越的性能都是必需的。关于seL4性能的更多信息见第6章。

seL4 发音 “s-e-l-four”

sell four这个发音弃用了，现在直接读字母即可。

2 没有IPC的虚拟机管理器不是好的微内核

宏内核VS微内核

主流操作系统(如Linux)和微内核(如seL4)之间的区别见图2.1。

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-kdtIorGn-1635304626728)(https://i.loli.net/2021/05/21/lLrjHg8qmOPIaGX.png)]

左边是Linux的架构图。黄色的部分是操作系统内核，它为应用程序提供文件存储和网络等服务。所有实现这些服务的代码都在CPU的特权模式下执行，也称为内核模式或管理模式，即对系统中所有资源的无限制访问和控制的执行模式。相反，应用程序以非特权或用户模式运行，对硬件的访问受到限制，受限的资源必须通过操作系统访问。操作系统内部结构为许多层，其中每一层提供由下面的层实现的抽象(The OS is internally structured in a number of layers, where each layer provides abstractions implemented by layers below. 看不懂这句话)。

特权模式代码的问题在于它很危险：如果这里出了什么问题，就没什么阻止破坏的办法了。特别是如果特权模式代码有一个漏洞，攻击者可以利用该漏洞以特权模式运行非法代码(称为特权升级或任意代码执行攻击)，那么攻击者可以对系统为所欲为。这些缺陷是主流系统中都有的。

当然，软件错误是现实存在的，操作系统也不例外。Linux内核由2000万行源代码组成(20 MSLOC)；可以估计它包含成千上万的bug ⁶。这显然是一个巨大的攻击面！Linux有一个很大的可信计算基础(TCB)，这个技术是整个系统的子集，整个系统的安全运行依赖于TCB。

微内核设计背后的理念是大幅缩小TCB，从而减少攻击面。如图2.1右侧所示，仅有很小一部分处于特权模式。seL4有一万行源代码(10 kSLOC)，比Linux内核小了三个数量级，攻击面也相应地缩小了(可能更小，因为bug的密度可能随代码大小线性增长)。

很明显，不可能在如此小的代码库中提供与Linux相同的功能。事实上，微内核几乎不提供任何服务：它只是对硬件的一个薄薄的包装，仅仅足够安全地复用硬件资源。微内核主要提供的是隔离，即一个程序可以在不受其他程序干扰的情况下执行的沙箱。同时它提供了一种受保护的过程调用机制(出于历史原因，称为IPC)。这允许程序安全地调用另一个程序中的函数。微内核在程序之间传输函数的输入输出并控制接口使用权：函数只能在一个导出的入口点被调用，并且只能被授权的客户端调用(第4章)。

关于seL4 IPC怎么用，建议阅读博客

https://microkerneldude.wordpress.com/2019/03/07/how-to-and-how-not-to-use-sel4-ipc/

微内核系统使用IPC来提供宏内核在内核态中实现的服务。在微内核世界中，这些服务只是程序，与应用程序没有区别，它们运行在自己的沙箱中，并为应用程序调用提供IPC接口。应用的故障将局限在沙箱内，系统的其余组件则不受影响(译注：指其余组件的安全性不受影响，但其余组件都无法继续使用故障组件提供的服务了)。这与宏内核形成了鲜明的对比，在宏内核系统中，内核故障将导致整个系统不可用。

译注：我觉得作者主要想说微内核可以将不可挽回的故障限制在某用户进程，内核和其他进程不受影响；而宏内核的内核一旦故障，运行其上的所有软件就都不可用了。

这种影响可以被量化：我们最近的研究表明，在Linux中所出现的严重问题，29%将被微内核设计完全消除，另外55%将被大大减轻，不再被列为关键问题⁷。

seL4是微内核，不是OS

seL4是一个微内核，设计的目的是确保通用性同时最小化TCB。它是L4微内核家族的成员，可以追溯到90年代中期；图2.2显示了seL4的起源。它是由我们在UNSW/NICTA的团队开发的，最近一段时间被称为可信系统(TS)。当时，我们在开发高性能微内核方面有15年的经验，并有实际部署的跟踪记录：我们的OKL4微内核搭载在数十亿高通蜂窝调制解调器芯片上，我们的L4 -嵌入式内核从10年代中期就在所有iOS设备的安全协处理器(secure enclave)上运行。

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-iHl7gqHC-1635304626731)(https://i.loli.net/2021/05/21/JDdEmiT4YNtQush.png)]

作为一个微内核，seL4不包含任何常见的操作系统服务；这些服务是由运行在用户模式下的程序提供的。这是微内核设计缺陷之一：正常运行总需要很多组件。可以从开源操作系统(如FreeBSD或Linux)移植，也可以从头开始编写。但无论如何，编写组件是一项重要的工作。

为了扩大规模组件规模，我们需要社区的帮助，而seL4 Foundation是使社区能够为基于seL4的系统合作、开发或移植此类服务的关键机制。其中最重要的是设备驱动程序、网络协议栈和文件系统。我们有相当数量的此类组件，但还需要更多。

的组件开发来说，组件框架很重要，它允许开发人员专注于实现服务本身，不必关注seL4的某些细节。seL4目前有两个主要的开源组件框架:CAmkES和Genode。

CAmkES是一个针对嵌入式和信息物理系统的框架，这些系统通常是静态架构，这意味着它们由一组定义好的组件组成，一旦系统完全启动，这些组件就不会改变。

Genode在很多方面都是一个更强大、更通用的框架，它支持多个微内核，并且已经提供了大量的服务和设备驱动程序，特别是针对x86平台。它比CAmkES更方便，而且肯定是快速建立复杂系统的方法。然而Genode也有缺点：

1. 由于Genode支持多个微内核(并非所有微内核都像seL4那样强大)，因此它的功能是所有微内核种类的共同子集。它不能使用所有的seL4的安全和安全特性。
2. 它没有可靠的故事(assurance story)。关于这一点，参见3.2节。

seL4是虚拟机管理器

seL4是一个微内核，但它也是一个管理程序:可以在seL4上运行虚拟机，如Linux。

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-RguoLFRr-1635304626733)(https://i.loli.net/2021/05/22/IuRgJkjhWfeXvVt.png)]

这提供了另一种提供系统服务的方法，即让Linux VM提供系统服务。这样的设置如图2.3所示，其中显示了一些服务如何从多个Linux实例中借用，这些实例作为客户机运行。

在本例中，我们提供两种系统服务：网络和存储。

网络是由直接运行在seL4上的本机协议栈提供的，lwIP或PicoTCP是常用的栈。我们没有移植网络驱动程序，而是借用Linux的一个驱动程序，这个精简的Linux客户机只有一个网卡驱动程序。协议栈通过sel4提供的通道与Linux通信，应用程序同样通过与协议栈通信获得网络服务。注意，在图中显示的设置中，应用程序没有到网卡驱动虚拟机的通道，因此不能直接与它通信：这是通过基于seL4能力而实现的(见第4章)

存储服务与此类似；文件系统是Linux虚拟机提供的，而存储驱动程序则是本地的。同样，组件之间的通信也是受通道限制的，应用程序不能直接与存储驱动程序通信，两个Linux虚拟机不能相互通信。

当用作虚拟机管理器时，seL4以特权模式运行(Arm上的EL2, x86上的Root Ring-0, RISC-V上的HS)，这是比客户机更高的特权级别。seL4只在特权模式执行作为虚拟机管理器所进行的少量工作工作，其余的工作都留给用户模式。

具体来说，这意味着seL4负责“世界切换”，当虚拟机的执行时间到期时，或者由于某些其他原因必须切出时，seL将进行状态切换操作。它还捕获虚拟化异常(Intel虚拟化架构中术语是VM exits )，并将它们转发给一个用户级处理程序，称为虚拟机监视器(VMM)。然后，VMM负责执行模拟操作。

每个VM都一个VMM，VMM与客户操作系统以及其他VM相互隔离，如图2.4所示。这意味着VMM不能打破隔离，因此并不比客户操作系统本身更可信。特别是，这意味着不需要验证VMM，因为只要不验证来宾操作系统(通常是Linux)，就不会增加真正的安全性。

译注：

由该小节可见，在seL4中，VM包含GuestOS与GuestApps，VMM可与VM交流但不能与GuestOS交流。

那么问题来了，VM在seL4中是一个实体还是一个由GuestOS和GuestApps组成的虚拟概念？

另外，VMM和Hypervisor要怎么在中文里进行区分？

seL4不是seLinux

许多人会搞混 seL4 和 seLinux (或许他们以为 seL4 是第 4 代 seLinux；译注：也可能因为 seL(inux) 缩写，就像 K8S). 事实上除了都开源， seL4 跟 seLinux 没有任何关系。他们在代码或概念上没有任何交集。 seLinux 不是微内核，它是 Linux 内置的安全框架。虽然比标准 Linux 更安全，但 seLinux 和标准 Linux 面对相同的问题：巨大 TCB 和相当大的攻击面。换句话说，seLinux 是一个根本不安全的操作系统的组件，因此仍然是根
本不安全的。相比之下， seL4 提供了武装到牙齿的隔离。

简而言之， seLinux 并不适合安全要求严格的情景，而 seL4 就是为这些用途而设计的。

3 验证过程(Verification Story)

2009年，seL4成为世界上第一个在源代码级别上经过机器证明功能正确性(machine-checked functional
correctness proof)的操作系统内核。当时由20万行证明脚本，是有史以来最大的(我们认为它是第二大)。以前人们以为不会有功能正确(functionally correct)的OS内核，我们证明它是存在的。

从那时起，我们将验证的范围进行了扩展，图3.1显示了证明链，下面将对此进行解释。重要的是，我们在内核不断发展的过程中一直保持这个验证措施：只有在不破坏证明的情况下，才允许提交到主线内核源代码，否则我们就更新证明代码(otherwise the poofs are updated as well)。这种证明工程是一种新事物。我们的seL4证明构成了迄今为止最大的还在维护的证明集(proof base)。到目前为止，证明脚本已经超过了100万行，其中大部分是手工编写然后用机器检查的(manually written and then machine checked)。

正确性和安全性

功能正确(Functional correctness)

seL4验证的核心是功能正确性证明，要确保C代码没有缺陷。更准确地说，内核的功能有一个正式的规范，用一种称为高阶逻辑(high-order logic, HOL)的数学语言表示。这由图中写着“abstract model”的方框表示。C实现是抽象模型的具体化，这意味着C代码的可能行为是抽象模型允许的行为的子集。

C语言不是形式化语言；为了允许在定理证明器中对C程序进行推理(我们使用Isabelle/HOL)，必须将其转换为数学逻辑(HOL)。这是由一个用Isabelle编写的C解析器完成的。解析器定义了C程序的语义，并根据这个语义形成HOL。这种形式化是数学(抽象)模型的改进(It is this formalisation which we prove to be a refinement of the mathematical (abstract) model)。

请注意，C语言没有正式的数学语义，而且C语言的某些部分是出了名的微妙，并没有定义得很好。我们通过将C的限制在该语言的一个定义良好的子集内来解决这个问题，对于这个子集我们有一个明确的语义。然而，这并不能保证我们为该子集假定的语义与编译器相同。下面将详细介绍。

我们想让内核的行为与规范一致，不允许出现于规范不同的行为。这就避免了通常用来攻击操作系统的操作，如栈溢出、空指针引用、代码注入或控制流劫持等。

编译验证（Translation validation）

一个没有bug的C内核是很棒的，但是我们仍然受制于C编译器。这些编译器(我们使用GCC)本身就是有bug的大型程序。我们那完美的代码很有可能被编译成有bug的二进制文件。

编译器出bug还是小事，就怕编译器使坏，包含一个木马程序，在编译操作系统时构建后门。木马也可以入侵用来编译编译器的编译器，这样我们想自己编译编译器也没法避免木马。Ken Thompson在他的图灵奖演讲中解释了这一攻击⁸。

为了防止有缺陷的或恶意的编译器，我们另外验证由编译器和链接器生成的可执行二进制文件。具体来说，我们证明了二进制代码是C代码的正确翻译，因此二进制代码也符合抽象规范。

译注：

这部分过于学术化，基础知识见SAT与SMT。

这张图的意思大概是把C代码和编译后的二进制都转化为数学描述，看这两种数学描述功能是否相同。

与C代码的验证不同，这个证明脚本不是手写的，而是通过一个自动工具链完成的。它由几个阶段组成，如图3.2所示。在定理证明器中，处理器指令集(ISA)的形式化模型形式化了二进制；我们使用了RISC-V ISA的L3形式化和广泛测试的L3 Arm ISA形式化⁹。

然后，一个用HOL4定理证明程序编写的反汇编程序将这种低级表示转换为控制流的图语言表示。这个变换被证明是正确的。

通过Isabelle/HOL定理证明器中可证明正确的变换，将形式化的C程序转换为相同的图形语言。然后我们得到了同一个程序的不同表示，我们需要表明它们是等价的。这有点棘手，因为编译器对代码进行了优化。We apply a number of such transformations through rewrite rules on the graph-language representation of the C program (still in the theorem prover, and thus provably correct).

最后，我们得到了两个非常相似但不相同的程序，我们需要证明它们有相同的语义。从理论上讲，这相当于停机问题 (halting problem)，因此是无法解决的。在实践中，编译器所做的事情是确定的，这使问题易于处理。我们通过将程序分成小块扔给多个SMT解决程序来解决这个问题。如果其中一个可以证明所有对应的部分具有相同的语义，那么我们就知道这两个程序是等价的。

还需要注意的是，被证明符合形式化规范的C代码和二进制文件都具有相同的Isabelle/HOL形式。这意味着我们对C语义的假设脱离了证明所做的假设(This means that our assumptions on C semantics drop out of the assumptions made by the proofs.)。总之，这些证明不仅表明编译器没有引入bug，还证明其C子集的语义和我们定义的语义相同。

安全属性

图3.1还显示了抽象规范和高级安全属性(机密性、完整性和可用性)(这些通常被称为CIA属性)之间的证明。抽象规范实际上对安全很有用：在一个正确配置的系统中，内核将强制执行这些属性。

1. 保密性：必须显式地给予数据读权限，seL4才允许实体读取数据
2. 完整性：seL4不允许一个实体在没有被显式给予数据写权限的情况下修改数据
3. 可用性：seL4不允许一个实体阻止另一个实体使用已授权的资源

译：关于安全验证的补充说明，实在不会翻译了。

These proofs presently do not capture properties associated with time. Our confidentiality proofs rule out covert storage channels but presently not covert timing channels, which are used by such attacks as Spectre. Preventing timing channels is something we are working on [Heiser et al., 2019]. Similarly, the integrity and availability proofs presently do not cover timeliness, but our new MCS model [Lyons et al., 2018] is designed to cover those aspects (see Section 5.2).

证明假设

所有关于正确性的推理都基于假设，无论是正式的推理(如seL4)，还是非正式的推理(当有人思考为什么他们的程序可能是正确的)。每个程序都在某个上下文中执行，它的正确行为不可避免地依赖于对这个上下文中的一些假设。

机器检查形式推理的优点之一是，它迫使人们明确地做出这些假设。不可能做出未声明的假设，如果证据依赖于没有明确声明的假设，那么它们就不会成功。从这个意义上说，形式推理可以防止忘记假设，或者不清楚假设；这本身就是核查的一大好处。

对seL4的验证有三个假设：

1. **硬件按预期运行。**这应该是显而易见的。内核受底层硬件的支配，如果硬件有bug(或者更糟，有木马)，那么无论您运行的是经过验证的seL4还是任何未经验证的操作系统，都将失败。硬件验证超出了seL4的范围(以及TS的能力);其他人有研究这个的。

2. **规范是正确的。**这是一个困难的问题，因为没人知道现在的规范是否完美。当然，有总比没有强。
   可以通过证明有关规范的属性来降低这种风险，正如我们在安全性证明中所做的那样，安全性证明表明seL4能够强制执行某些安全性属性。这就把问题转移到了这些属性的说明上。它们比内核规范简单得多，减少了误解的风险。
   但数学和物理之间总是存在着鸿沟，任何推理都无法完全消除这一点。形式推理的好处是，你确切地知道差距是什么

3. **定理证明器是正确的。**这听起来像是一个严重的问题，因为定理证明本身就是一个庞大而复杂的程序。然而，在现实中，这是三个假设中最不值得关注的。因为Isabelle/HOL定理证明器有一个小核心(10 kSLOC)，用来检查所有与逻辑公理相悖的证明。这个核心已经从广泛的形式推理领域中检查了许多大大小小的证明，所以它包含正确性关键错误的可能性是非常小的。

   译注：我觉得这种套娃证明无穷尽的思想就是古欧洲哲学的精髓了；与我国天人合一的哲学明显不同。

证明进度

seL4已经或正在被多个架构验证：Arm、x86和RISC-V。他们的验证进度各不相同，有的正在研究，有的就是缺钱搞。详情请参考seL4项目状态页面。

CAmkES组件框架

CAmkES is a component framework that allows you to reason about a system architecturally, i.e. as a collection of sandboxed components with defined communication channels. Figure 3.3 shows the main abstractions.

不会翻译

组件用方框表示。它们表示由seL4封装的程序、代码和数据。

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-pseUjkf0-1635304626737)(https://i.loli.net/2021/05/21/T9RBGFlIVgOqvD7.png)]

接口定义了如何调用一个组件，或者如何调用其他组件。接口要么被导入(调用另一个组件的接口)，要么被导出(能够被另一个导入的组件的接口调用)，共享内存接口除外，它是对称的。

连接器将同类型的输入输出接口连接起来。CAmkES中的连接器总是一对一的。但是通过添加将单输入复制成多输出的组件实现广播或多播功能。

CAmkES系统是用一种正式的体系结构描述语言(CAmkES ADL)指定的，它包含对组件、它们的接口和连接它们的连接器的精确描述。CAmkES对系统设计者的承诺是，ADL中指定的(如图3.3所示)就是可能产生的交互。特别地，它承诺除了图中所示的交互之外，没有其他交互的可能。

当然，这个承诺依赖于seL4，ADL表示必须映射到低级seL4对象和对它们的访问权限。这就是CAmkES机制所实现的，如图3.4所示。

在图的顶部展示了ADL中所描述的结构。这是一个相当简单的系统，由4个本机组件和一个包含两个驱动的虚拟机组件。Linux虚拟机只能通过crypto组件连接到其他组件，这就保证了虚拟机只能访问加密的链接，不会泄露数据。

即使是这个简单的系统也会映射成百上千各seL4对象，CAmkES为我们降低了开发复杂度。

对于sel4级的描述，我们有另一种正式的语言，称为CapDL(能力分配语言)。系统设计者永远不需要处理CapDL，它是一个纯粹的内部表示。CAmkES框架包含一个编译器，它自动将CAmkES ADL转换为CapDL，由左向下的方框箭头表示。图左侧的框给出了CapDL中描述的seL4对象的简化表示。

CapDL规范是系统中访问权限的精确表示，也是seL4强制执行的。这意味着一旦系统进入CapDL规范描述的状态，它就保证按照CAmkES ADL规范描述的行为，因此体系结构级别的描述足以进一步推理安全属性(therefore the architecture-level description is sufficient for further reasoning about security properties. )。

因此，我们需要确保系统启动到CapDL规范所描述的状态。我们通过第二个箭头实现了这一点：我们从CapDL生成启动代码，一旦seL4自身启动，就控制并生成规范引用的所有seL4对象，包括描述活动组件的对象，在初始化代码执行的最后，可以证明系统处于CapDL规范所描述的状态，因此也处于ADL规范所表示的状态。

第三个箭头表示从ADL规范生成的组件之间的胶水代码。通过连接器发送数据需要调用seL4系统调用，这些系统调用的细节被CAmkES隐藏。胶水代码使用了这些系统调用。例如，RPC连接器将一个远程过程调用封装成了普通函数调用。

在撰写本文时，关于CAmkES和CapDL的证明还没有完成，但离完成很近了。

还请注意，所提到的验证工作都没有处理定时通道造成的的信息泄漏。这是一个尚未解决的重大问题，但我们就快搞定了。

4 能力

我们在第一章中遇到了一些功能，注意到它们是访问令牌。现在我们将更详细地研究这个概念。

什么是能力

如图4.1所示，一个能力是一个对象引用；它类似于指针(能力的实现通常称为胖指针)。能力是不可变的指针，指向内核中对应权限类型的对象。

除了指针之外，能力还对访问权限进行编码。在基于功能的系统(如seL4)中，调用功能是对系统对象执行操作的唯一方法。

例如，一个操作可能是调用组件中的函数。嵌在该功能中的对象引用指向该对象的接口，并表达调用该函数的权利。(The capability may or may not at the same time convey the right to pass another capability along as a function argument (delegating to the component the right to use the object referenced by the capability argument) )

这是CAmkES抽象级别的高级描述。事实上，在CAmkES里，能力本身被封装了。

在底层，连接器由端点对象表示，客户端组件需要具有调用权限的能力。

正是这种细粒度的、面向对象的特性使得能力成为面向安全系统的访问控制机制。最小化每个组件的能力，这是最低特权原则所要求的。

请注意，能力的这个概念与Linux所称的能力强大得多，后者实际上是具有系统调用粒度的访问控制列表(acl)。与所有ACL模式一样，Linux功能也存在令人困惑的问题，这是许多安全漏洞的根源，下一节将对此进行解释。seL4的能力没有这个问题。

seL4能力也不容易受到该引文¹⁰中描述的攻击；这种攻击适用于直接在硬件中实现的功能，而seL4的能力由内核实现。

有10种类型的seL4对象，它们都由能力引用：

**端点Endpoints **用于执行受保护的函数调用

**应答对象Reply Objects **表示来自受保护过程调用的返回路径

**地址空间Address Spaces **提供了沙箱(硬件页表的封装)

**节点Cnodes **存储表示组件访问权限的能力

**线程控制块Thread Control Blocks **表示线程

**调度上下文Scheduling Contexts **表示在处理器上使用一个时间片的权利

**通知Notifications **是同步对象(类似于信号量)

**帧Frames **表示可以映射到地址空间的物理内存

**中断对象Interrupt objects **提供对中断处理的访问

空类型Untypes未使用的(自由的)物理内存，可以转换为任何其他类型

为什么要使用能力

细粒度访问控制

能力提供细粒度的访问控制，符合最小权限安全原则(也称为最小权限原则POLA)。这与访问控制列表(acl)这种更传统的访问控制模型形成了对比，后者在主流系统(如Linux或Windows)中使用，但也在商业系统(如INTEGRITY或PikeOS)中使用。

要理解其区别，首先看访问控制在Linux中是如何工作的：文件(文件访问权限控制具有代表性)具有一组访问模式位。其中一组位决定了它的所有者可以对文件执行什么操作，另一组位代表了用户组中每个成员允许的操作，最后的一组位是授予其他人的默认权限。这是一个面向用户的方案，以用户身份区分权限。用户对权限设置相同的文件享有相同权限。

这是一种非常粗粒度的访问控制形式。一个典型的场景是，用户希望用一个不受信任的程序(比如从互联网上下载)处理一个特定的文件，但希望阻止该程序访问该用户的其他文件。在Linux中没有优雅的方法来做到这一点，人们想出了一些笨重的解决方案，比如chroot，容器等。

有了能力，这个问题很容易解决，因为能力提供了面向对象的访问控制形式。具体来说，当且仅当请求操作的程序拥有对应能力时，内核才会允许操作继续进行。在限制场景中，不受信任的应用程序只能访问被赋予权限的文件。因此Alice调用程序，将一个能力交给程序允许读取的一个文件，再加上一个能力让他可以把输出内容写到另一个文件里，这个程序不能访问任何其他事物——这就是最小权限。

中介与授权Interposition and delegation

能力还有很多特性。一个是中介访问的能力，这是不透明对象引用的结果。如果Alice被赋予了一个对象的能力，她不知道这个对象到底是什么，她所能做的就是调用对象上的方法。

例如，系统设计者可能假装给Alice的能力指向一个文件，而实际上它指向一个通往安全监视器的通道，安全监视器持有实际能力。监视器可以检查Alice请求的操作，如果合法Alice执行文件操作，不合法则忽略请求。监视器有效地虚拟化了文件。

中介不仅仅可以用来做安全检查；该方法可用于包过滤、信息流跟踪等。调试器可以透明地插入和虚拟化对象调用。它甚至可以懒加载一个对象：Alice调用该对象时，对象才会被创建。

能力的另一个优点是，它们支持安全有效的权限授权。如果Alice想让Bob访问她的一个对象，她可以为该对象创建(在seL4中叫mint)一个新能力，并将其交给Bob。然后Bob就可以使用该能力来操作对象，而不需要还给Alice。(相反，如果Alice想要保持对这个过程的控制，它可以使用上一段讲的中介技术。)

新能力的权利可能会减少；Alice可以只给Bob只读权限。Alice可以在任何时候撤销Bob的访问权，方法是摧毁她交给Bob的派生能力。

授权功能很强大并且在ACL系统中无法轻松且安全地完成。一个典型使用授权的例子是设置自主管理资源的子系统。当系统启动时，初始进程拥有对系统中所有资源的权限(除了内核本身使用的少量且固定的资源)。然后，这个初始资源管理器可以通过创建新的进程(子资源管理器)，并赋予他们互不相交的权限，来分割出不同子系统。

然后子系统可以自主地(不参考原始管理器)控制它们的资源子集，同时不相互干扰。只有当他们想要改变原始资源分配时才需要访问初始管理器。

周围权限和困惑的副手

acl有一个无法解决的问题，通常称为混淆代理。让我们来看一个C编译器。它接受一个C源文件并产生一个输出文件，文件名作为参数传递。要运行编译器，用户Alice必须对编译器具有执行权限，如图4.2所示。

假设编译器还在系统级日志文件中创建了一个用于审计目的的条目。日志文件对普通用户是不可访问的，因此编译器必须以提升的权限执行，以便写入日志文件(传统上通过将其设置为setuid程序来完成)。

如果Alice是恶意的，她可以欺骗编译器去做它不应该做的事情。例如，Alice可以在调用编译器时指定密码文件作为输出文件。除非编译器非常小心地编写以避免任何潜在的滥用，否则它将只打开输出文件(密码文件)，并使用已编译的目标代码覆盖它。Alice编写一个程序，使新生成的密码文件赋予她不应该拥有的特权，这并不需要很多技巧。

这里的基本问题是，当编译器打开它的输出文件进行写入时，操作系统通过查看编译器的用户ID来确定访问的有效性，以确定它是否有访问该对象的权限。由编译器决定操作是否有效，使编译器成为系统TCB的一部分，这意味着必须完全信任它，以便在所有情况下做正确的事情。

ACL系统可以采用一些防御措施来减轻特定的问题,例如,确保密码文件和日志文件在不同安全域(这不会阻止爱丽丝痛击日志文件)。这就导致了通常的攻击和防御的军备竞赛。

这种混淆是由环境权限(ambient authority)引起的：操作的有效性由代理(编译器)的安全状态决定，在本例中代理是代表Alice。为了适当的安全性，访问必须由Alice的安全状态决定。这意味着命名(对文件的引用)和权限(对文件执行操作的权利)必须耦合在一起，这一原则称为没有权限就不指定。如果是这种情况，那么编译器将使用指定的权限(来自Alice)调用指定的对象(输出文件)，这样Alice就不会再混淆代理了。

这正是能力系统所做的。在这样的系统中，Alice需要拥有三种能力：执行编译器的能力、读输入文件的能力和写输出文件的写能力。她使用执行能力调用编译器，并将另外两个能力作为参数传递。然后，当编译器打开输出文件时，它使用Alice提供的能力进行操作。编译器使用一个独立的能力来打开日志文件，使日志和编译输出分开。特别是，Alice不可能欺骗编译器写入一个她自己无法访问的文件。

解决“困惑的副手问题”是能力的杀手级应用，因为这个问题无法用acl解决。因此，下次有人试图向你出售一个安全的操作系统时，不仅要问他们是否有操作系统的正确性证明，还要问它是否使用了基于能力的访问控制。如果这两个问题的答案都是否定的，那么你就得到了假货(原文snake oil 蛇油指假的万金油)。

5 支持硬实时系统

seL4被设计为一个保护模式的实时操作系统。这意味着，与经典的RTOSes不同，seL4结合了实时能力和内存保护，以确保安全性，并部分支持混合关键系统。

一般实时支持

seL4有一个简单的、基于优先级的调度策略，易于理解和分析，这是硬实时系统的核心需求。内核将自己永远不会调整优先级，因此用户是控制者。

另一个需求是有限中断延迟。与L4微内核家族的大多数成员一样，seL4在内核模式下执行时禁用中断。这个设计决策极大地简化了内核的设计和实现，因为内核(在一个单核处理器上)不需要并发控制。否则，seL4的正式验证是不可行的，但该设计也使优异的平均情况性能成为可能。

人们普遍认为，为了保持较低的中断延迟，实时操作系统必须是可抢占的(除了短的临界部分)。虽然对于在简单微控制器上运行的传统非保护模式RTOSes是正确的，但在保护模式系统上并不对，如seL4。因为当运行在一个启用了内存保护的强大微处理器上时，进入内核、切换上下文和退出内核的时间非常长，不比seL4系统调用少多少。就中断延迟而言，可抢占设计几乎没有什么好处，但复杂性方面的成本将非常高，使得可抢占设计不合理。

只要所有系统调用都很短就行。在seL4中系统调用都很短，但也有例外。特别是撤销一个能力可能是一个耗时的操作。seL4处理这种情况的方法是将这些操作拆分为短的子操作，使他可以被中断，被打断的操作可以在中断完成后接着执行。

这种方法被称为增量一致性。每个子操作将内核从一个一致状态转换为另一个一致状态。该操作的结构是这样的：在中止之后，可以重新启动该操作，而无需重复中止之前成功的子操作。内核在每个子操作之后检查挂起的中断。如果有，它将中止当前操作，此时中断将强制重新进入内核，由内核处理中断。当完成时，原始系统调用将重新启动，然后从它被中止的地方继续执行，以确保进展。

我们对seL4进行了完整而合理的最坏情况执行时间(WCET)分析，这是唯一有记录的保护模式OS的最坏情况执行时间分析¹¹¹²。这意味着我们已经得到了所有系统调用延迟的可证明的硬上界，以及最坏情况下的中断延迟。

这种WCET分析是支持硬实时系统的先决条件，也是使seL4在竞争中脱颖而出的特性。虽然已经对不受保护的RTOSes进行了完整和可靠的WCET分析，但保护模式系统的行业标准方法是将内核置于高负载下，测量延迟，采用观察到的最坏的延迟，并添加一个安全系数。不能保证这种方法得到的界是安全的，而且它不适合安全关键系统(safety-critical systems)。

我们为Arm v6处理器做了seL4的WCET分析。由于Arm不再提供指令的最坏情况延迟所需的信息，而英特尔也从未为其架构提供这些信息，该系统从此陷入停顿。然而，随着开源RISC-V处理器的出现，我们将能够重新进行这一分析。

5.2 混合关键系统

什么是混合关键系统

关键是一个来自安全领域的术语，与组件故障的严重程度有关。例如，航空电子标准对故障进行了分类，从对车辆安全没有影响到灾难性故障(造成人员伤亡)。组件越关键，所需的保证就越广泛(也越昂贵)，因此有强烈的动机保持低关键(there is a strong incentive for keeping criticalities low. )。

混合关键系统(MCS)由不同关键的组分(相互作用)组成。它的核心安全要求是一个组件的故障不能影响到任何更关键的组件，从而确保关键组件独立于不那么关键的组件

传统上，关键系统的每个功能都使用专用的微控制器，即电气隔离。随着功能的增长，这种方法导致处理器(及其封装和布线)的激增，从而导致空间、重量和功率(SWaP)问题，而这正是MCS的目标。

这类似于在同一个系统中同时拥有受信任和不受信任组件的组件，在这两种情况下，操作系统的核心需求都是强隔离。安全领域的挑战在于，安全性不仅依赖于功能正确性，还依赖于及时性：关键组件通常有实时需求，这意味着它们必须在截止时间前对事件做出响应。

传统MCS

传统的MCS操作系统完全隔离部件的时间和空间，一种称为严格时间和空间划分(TSP)的方法，以ARINC 653航空电子标准ARINC¹³为例。这意味着每个组件被静态地分配一个固定的内存区域，并且分区根据预先确定的调度顺序和固定的时间片执行。

TSP方法保证隔离，但有严重的缺点。最明显的一个是资源利用不足。每个实时组件必须能够在它的时间片内完成它的工作，所以时间片必须至少是组件的最坏情况执行时间。组件的WCET可以比通常的执行时间大几个数量级，因为它必须考虑到异常情况。

此外，确定WCET的安全边界通常是棘手的。对于关键组件，必须非常保守地说服持怀疑态度的认证机构，这通常会导致估值较大。这意味着处理器通常没有得到充分利用。但是，由于严格的分区，空闲时间不能被其他组件使用，因此利用率不佳是一个固有的问题。基本上，通过保留间隙实现强隔离，TSP资源使用率较差。

TSP的另一个大缺点是中断延迟本身就很高。以图5.1为例，它可能表示一个(高度简化的)自动驾驶汽车。关键部件是一个控制回路，它每5毫秒执行一次，处理传感器数据并向执行器发送命令。它的WCET，也就是时间片，是3毫秒。车辆还与一个地面站通信，它可以更新路径点。因为系统以5毫秒的时间运行，这是可以处理网络中断的延迟时间，极大地限制了网络吞吐量和对外部事件的响应能力。

seL4的MCS

MCS的核心挑战是操作系统必须提供强大的资源隔离，但是TSP过于简单(因此不灵活)。就空间资源而言，seL4已经有了一个灵活、强大且可证明安全的模型：对象能力(见第4章)。接下来讨论时间资源：对处理器的访问也由能力控制。

用于处理器时间的seL4能力称为调度上下文能力。组件只有在拥有这样的能力时才能获得处理器时间，并且它可以使用的处理器时间量被编码在该能力中。这类似于空间对象的访问权限的工作方式。

在传统的seL4中(就像在它之前的大多数L4内核中一样)，线程有两个主要的调度参数：优先级和时间片，它们决定对处理器的访问。

优先级决定了线程何时可以执行，如果没有更高优先级的可运行线程，它可以运行。时间片决定内核在抢占线程之前允许线程运行多长时间(除非它在被一个更高优先级的线程成为可运行线程之前被抢占)。当时间片耗尽时，调度器将再次选择优先级最高的可运行线程(可能是刚刚被抢占的线程)，并在优先级级别中使用循环策略。

seL4的MCS版本将时间片替换为调度上下文对象的能力，该对象执行类似的功能，但以更精确的方式执行隔离：调度上下文包含两个主要属性。(1)时间预算，类似于旧的时间片，并限制线程可以执行的时间。(2)一个时间段，它决定了预算可以被使用的频率：无论优先级如何，在该时间段内他都会被分到自己时间预算那么长的处理器时间。

调度上下文支持推理一个线程可以消耗多少时间，还有多少时间剩余。可用于防止高优先级线程独占处理器。

应用于上面的例子，这意味着我们可以给(不太关键的)设备驱动程序一个比(关键的)控制组件更高的优先级。这允许驱动程序抢占控制，提高响应速度。但是时间预算将阻止驱动程序过度使用CPU。例如，我们给控制器一个3ms的预算(它的WCET)和一个5ms的周期(对应于它运行的频率)。我们给高优先级驱动3µs预算，周期为10µs，这意味着它在任何情况下都不能消耗超过总处理器时间的30%，但可以足够频繁地执行以确保良好的响应性。重要的是，我们可以保证控制器(它需要的可用处理器时间不超过60%)有足够的时间满足截止时间。

通过不考虑驱动程序的行为而保证关键截止日期，将控制与不受信任的驱动程序隔离。特别是，驱动不需要被认证为安全关键。

seL4的时间能力模型解决了MCS的许多其他挑战，超出了本白皮书的范围，有兴趣的读者可阅读这篇文章¹⁴。可以说，在所有关键操作系统中，seL4提供了最先进和最灵活的MCS支持。

6 安全性能全都要

性能一直是L4家族的标志，seL4也不例外。我们构建seL4是为了实际应用，我们的目标是相对于我们之前拥有的最快的内核而言，IPC性能损失不超过10%。结果是，seL4最终比这些内核还快。

它的性能胜过任何其他微内核。这是一种很难证明的说法，因为竞争对手通常会将他们的性能数据保密(出于非常好的理由!)

然而，我们会利用一切机会，公开宣布这一业绩。如果有人不同意，他们需要出示证据。我们还通过一些非正式渠道了解到，其他系统的IPC性能往往比seL4慢2倍到慢得多，通常大约是seL4的10倍。

有几个独立的性能对比验证了我们的优越性。

这篇文章¹⁵比较三个开源系统的性能，seL4, Fiasco.OC和Zircon 。它发现seL4 IPC成本比内核进入、地址空间切换和内核退出的硬件限制大约高出10% 20%。Fiasco.OC比seL4慢2倍以上(接近硬件极限的3倍)，Zircon的速度几乎是seL4的9倍。

这篇文章¹⁶比较了CertiKOS和seL4的性能，在CertiKOS中实现双向IPC花了3820个运行周期，而在seL4中花了1830个周期。然而，事实证明，sel4bench (seL4基准测试套件)在处理x86上的计时器时存在一个bug，导致了夸大的延迟。正确的seL4性能值大约是720个循环，比CertiKOS快5倍以上。另外CertiKOS提供特性非常有限，也没有基于能力的安全性。

7 实际生产和渐进式改造

一般情况

当计划使用seL4的安全特性时，第一步应该是确定需要保护的关键资产。目标是将可信计算基础TCB最小化，并使其尽可能模块化，使每个模块都成为受sel4保护的CAmkES组件。

另一个重要的准备工作是检查平台上seL4的可用性和验证状态。显然，seL4的卖点就是经过形式化验证。然而，即使在未验证的平台上，它也比其他操作系统更安全。但是要牢记，没有验证就没有完全的安全保证。如果您使用的内核没有为您的平台进行验证，或者您魔改了内核，那出了事您一定不要怪我们。

您还需要评估seL4的基础软件生态是否满足您的目的。如果不是，那么这就是社区可以帮助你的地方。有一些公司专门为seL4提供支持。此外，如果您自己开发了任何通常组件，您应该认真考虑在适当的开源许可下与社区共享它们。助人者人恒助之。

改造现有系统

在现实世界中，大多数seL4的部署都不会在本地(native)运行所有内容，有可能以虚拟机的方式运行在seL4上。通常，有一些重要的遗留组件移植起来会很昂贵，因为它们可能依赖目前seL4不支持服务。此外，通常情况下，本地运行这些遗留堆栈不会带来什么安全性或安全性收益。

使用seL4的虚拟化能力通常是一种实用的方法，第2.3节给出了一些示例。

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-Ob6NrEdy-1635304626741)(https://i.loli.net/2021/05/22/WdCq1MHYB9xwf5Q.png)]

典型的方法是我们所谓的“渐进式改造”，这是当时DARPA项目主任约翰·朗奇伯里创造的术语。如图7.1所示，通常首先将整个现有软件堆栈放入在seL4上运行的虚拟机中。显然，这个步骤在安全性和安全性方面没有任何价值，它只增加了非常小的开销。它的重要意义在于，它提供了模块化的开端。

一个很好的例子是我们的HACMS项目合作伙伴对波音ULB自动直升机进行的网络改造。最初的系统运行在Linux上，在第一步中，团队将seL4放在了下面。

下一步出现了两个组件:特别不受信任的摄像头软件被转移到同样运行Linux的另一个虚拟机，两个Linux虚拟机通过CAmkES通道通信。同时，网络堆栈从VM中取出并转换为原生CAmkES组件，也与主VM通信。

最后一步是将所有其他关键模块以及(不可信的)GPS软件放入单独的CAmkES组件中，移除原来的主VM。最后的系统由许多运行sel4本机代码的CAmkES组件和一个只运行Linux和摄像软件的单个VM组成。

结果是，虽然最初的系统很容易被DARPA雇佣的专业渗透测试人员侵入，但最终状态是高度弹性的。攻击者可以破坏Linux系统并对其为所欲为，但无法突破并破坏系统的其他部分。这个团队有足够的信心证明是在飞行中攻击。(The team was confident enough to demonstrate an attack in-flight)

总结

seL4是世界上第一个经过形式化验证的OS内核。

虽然到目前为止有其他经过验证的内核，seL4仍然是最先进的。它有最全面的验证过程¹⁷。它也是唯一的基于能力的OS验证，它有最先进的实时性支持。我们的持续研究使得seL4在安全导向内核中始终处于领先水平。例如，我们对通过定时通道泄露信息的系统性和原则性预防¹⁸。

除了这种技术上的领先地位，seL4在实际应用方面仍然远远领先于其他人：我们从一开始就为现实应用设计seL4，而几乎所有其他经过验证的内核都是学术玩具，离现实应用还很远。事实上，我们只知道另一个(最近)验证过的系统实际上是可部署的(尽管在更有限的场景中)。

seL4在生产中的应用得益与两大目标：性能上不妥协(第6章)以及旨在支持最广泛应用场景的安全策略，后者通过基于能力的访问控制实现(第4章)。

seL4参与实际生产的10年经验，显然帮助我们完善和改进了系统，但我很自豪地说，轻微的、增量的改变就足够了。唯一的例外是MCS支持(第5.2节)，这需要对模型及其实现进行相当重大的改变，但时间的特权管理是我们在最初设计时已经计划去做的事情。¹⁹。

希望这份白皮书能让您对seL4有一个大体的认识，让您知道可以用它做什么，重要的是，让您知道为什么想要使用它。我希望这将帮助您成为seL4社区的活跃成员，包括加入和参与seL4基金会。

我希望这份文件能够不断发展，我也很期待得到反馈。但最重要的是，我很想听听您部署seL4的经验。

致谢

我非常感谢我收到的关于本白皮书早期版本的反馈，这有助于改进它。TS的以下成员对草稿进行了评论：Curtis Millar, Gerwin Klein, Ihor Kuz, June Andronick, Liz Willer, Luke Mondy, Michael Norrish和Zoltan Kocsis。

此外，我还收到了来自社区成员Ben Leslie和Davor Ocelic的评论。

Kim Pastor 在创立基金会品牌方面做了很好的工作。

参考文献

---

1. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, et al. seL4: Formal verification of an OS kernel. In ACM Symposium on Operating Systems Principles, pages 207–220, Big Sky, MT, US, October 2009. URL https://ts.data61.csiro.au/publications/nicta_full_text/1852.pdf ↩︎

2. Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1):2:1–2:70, February 2014. URL https://ts.data61.csiro.au/publications/nicta_full_text/7371.pdf. ↩︎

3. Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury, and Gernot Heiser. Timing analysis of a protected operating system kernel. In IEEE Real-Time Systems Symposium, pages 339–348, Vienna, Austria, November 2011. IEEE Computer Society. URL https://ts.data61.csiro.au/publications/nicta_full_text/4863.pdf. ↩︎

4. Thomas Sewell, Felix Kam, and Gernot Heiser. High-assurance timing analysis for a high-assurance real-time OS. Real-Time Systems, 53:812–853, September 2017. URL https://ts.data61.csiro.au/publications/csiro_full_text//Sewell_KH_17.pdf. ↩︎

5. Anna Lyons, Kent McLeod, Hesham Almatary, and Gernot Heiser. Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time. In EuroSys Conference, Porto, Portugal, April 2018. ACM. URL https://ts.data61.csiro.au/publications/csiro_full_text//Lyons_MAH_18.pdf. ↩︎

6. Simon Biggs, Damon Lee, and Gernot Heiser. The jury is in: Monolithic OS design is flawed. In Asia-Pacific Workshop on Systems (APSys), Korea, August 2018. ACM SIGOPS. URL https://ts.data61.csiro.au/publications/csiro_full_text//Biggs_LH_18.pdf. ↩︎

7. Simon Biggs, Damon Lee, and Gernot Heiser. The jury is in: Monolithic OS design is flawed. In Asia-Pacific Workshop on Systems (APSys), Korea, August 2018. ACM SIGOPS. URL https://ts.data61.csiro.au/publications/csiro_full_text//Biggs_LH_18.pdf. ↩︎

8. Ken Thompson. Reflections on trusting trust: Turing award lecture. Communications of the ACM, 27(8):761–763, August 1984. ↩︎

9. Anthony Fox and Magnus Myreen. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In Proceedings of the 1st International Conference on Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 243–258, Edinburgh, UK, July 2010. Springer. ↩︎

10. William Earl Boebert. On the inability of an unmodified capability machine to enforce the–property. In 7th DoD/NBS Computer Security Conference, pages 291–293, September 1984. ↩︎

11. Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury, and Gernot Heiser. Timing analysis of a protected operating system kernel. In IEEE Real-Time Systems Symposium, pages 339–348, Vienna, Austria, November 2011. IEEE Computer Society. URL https://ts.data61.csiro.au/publications/nicta_full_text/4863.pdf. ↩︎

12. Thomas Sewell, Felix Kam, and Gernot Heiser. Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis. In IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April 2016. URL https://ts.data61.csiro.au/publications/nicta_full_text/9118.pdf. ↩︎

13. ARINC. Avionics Application Software Standard Interface. ARINC, November 2012. ARINC Standard 653. ↩︎

14. Anna Lyons, Kent McLeod, Hesham Almatary, and Gernot Heiser. Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time. In EuroSys Conference, Porto, Portugal, April 2018. ACM. URL https://ts.data61.csiro.au/publications/csiro_full_text//Lyons_MAH_18.pdf. ↩︎

15. Zeyu Mi, Dingji Li, Zihan Yang, Xinran Wang, and Haibo Chen. SkyBridge: Fast and secure inter-process communication for microkernels. In EuroSys Conference, March 2019 ↩︎

16. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In USENIX Symposium on Operating Systems Design and Implementation, pages 653–669, Savannah, GA, US, November 2016. USENIX Association. ↩︎

17. Gernot Heiser. 10 years seL4: Still the best, still getting better, August 2019. URL https://microkerneldude.wordpress.com/2019/08/06/10-years-sel4-still-the-best-still-getting-better/. Blog post. ↩︎

18. Qian Ge, Yuval Yarom, Tom Chothia, and Gernot Heiser. Time protection: the missing OS abstraction. In EuroSys Conference, Dresden, Germany, March 2019. ACM. URL https://ts.data61.csiro.au/publications/csiro_full_text//Ge_YCH_19.pdf ↩︎

19. Gernot Heiser and Kevin Elphinstone. L4 microkernels: The lessons from 20 years of research and deployment. ACM Transactions on Computer Systems, 34(1):1:1–1:29, April 2016. URL https://ts.data61.csiro.au/publications/nicta_full_text/8988.pdf ↩︎