seL4：被证明的微内核

破除误解#

它证明的是：在明确写下的假设下，C 实现相对于抽象规格是功能正确的精化。规格覆盖范围内的一类运行时错误——空指针、缓冲区越界、未定义的内核状态转换——被排除。驱动、用户程序、启动代码、设备、编译器（在二进制证明出现之前）和硬件模型之外的物理芯片，都不在定理里。把“内核实现符合模型”读成“整台机器不会出错”，是把结论的主语换掉了。

误解二：capability 就是 Unix 的文件描述符再加一层权限位。

seL4 的 capability 是内核里不可伪造的权限令牌：谁持有它、能对哪个内核对象做什么，本身就是状态的一部分。权限可以衰减、派生、回收；撤销一棵派生树，意味着下游所有副本一起失效。文件描述符是某个进程打开表里的一项，内核并不把“全局权限拓扑”当成一等对象来维护。把两者等同，会看不见 seL4 真正在管的那张图。

误解三：证明一次之后，改内核只是普通的补丁流程。

证明是代码的影子。改一个调度器字段、改一条 IPC 慢路径，往往要重做一串引理。seL4 后来能演进，是因为团队把规格、可执行 Haskell 原型、C 实现和证明脚本当成同一份产品来养，而不是因为证明让以后的修改变免费。

微内核为什么必须小#

seL4 走的是 L4 路线。Jochen Liedtke 在 1995 年的 SOSP 论文里论证过：微内核慢，往往不是因为“切成小块”这件事本身，而是因为 IPC 路径被写得太肥、地址空间切换付了不该付的税。L4 把内核收成地址空间、线程、IPC 和中断。文件系统、驱动、网络栈全部赶到用户态。

NICTA 的 L4 分支从 1990 年代的 L3/L4 经验里长出来。Kevin Elphinstone 与 Gernot Heiser 后来在 2013 年的回顾里写得很直白：二十年里真正留下来的，不是某一次性能数字，而是“内核必须小到能被说完”这条纪律。seL4 把这条纪律推到了逻辑终点——小，不是为了好看，是为了让规格写得完、让证明检查器跑得完。

用户态看到的世界因此很贫瘠。没有 POSIX 系统调用表，没有 fork 那种隐含复制整份地址空间的原语。要映射一页内存，必须持有对应的 paging capability；要发一条消息，必须持有 endpoint 上的发送权。接口贫瘠是隔离的价格，也是证明的前提：内核若提供几百个入口，规格会先写不完。

三层精化：规格、原型、C#

证明的骨架是一条精化链。最上面是抽象规格：内核对象、系统调用、失败时如何失败。中间一度是可执行的 Haskell 原型，用来跑测试、对齐语义，让“规格说的”和“人以为规格说的”先在可运行的代码上碰面。最下面是手工写成、为验证而约束过的 C——禁止不少会让语义含糊的写法，好让 C 到规格的对应能被说清楚。

每一层都要证明：下层能做的可观察行为，上层都允许。于是“功能正确”不是一句评语，而是两两之间的精化定理。检查器不会读你的意图，它只检查推理步骤有没有跳。跳了，定理过不去；没跳，只说明你写下的那句话被证了。

2013 年，Thomas Sewell、Magnus Myreen 和 Klein 在 PLDI 上补了翻译验证：把编译后的二进制和 C 语义对齐，从而把当时的 GCC 从可信计算基里挪出去。内核的 C 文本被证明，不等于目标板上的机器码被证明。这一步之前，编译器仍是一个必须信任的大口子。这一步之后，口子变窄了，但没有消失——汇编、启动代码、硬件模型仍在外面。

精化还有一个容易被忽略的方向：失败也必须被规格写进去。系统调用可以拒绝、可以返回错误、可以在资源耗尽时停住。如果规格只写“成功时做什么”，实现就可以在失败路径上任意行事而仍满足精化。seL4 把失败当作一等行为来证，这比只证“高兴路径”贵得多，也正是测试覆盖率最爱漏掉的地方。

Capability：权限变成内核对象#

典型对象包括线程控制块、capability 空间（CNode）、页表、endpoint（同步 IPC）、notification，以及未分配的 untyped 内存。没有 capability，用户态连“请内核改一页页表”都说不出口。完整性说的是：没有写权限的 capability，就不能改别人的状态。信息流与保密性是另一条定理，Toby Murray 等人在 2013 年的 Oakland 会议上给出，而且对调度、缓存、时间通道另有假设。

回收是这套模型的利齿。revoke 沿着派生树把下游权限剪掉，对应的对象可以重新变成 untyped。这不是 POSIX 的“关掉 fd”，而是一次全局的权限回收。证明要保证：回收之后，残留引用不能再当权限用。少了这一步，capability 只是换了个名字的访问控制列表。

untyped 内存把物理内存变成可分割、可重新类型化的资源。一块未分配内存可以被 retype 成页、CNode 或线程控制块；回收后再变回 untyped。这强迫系统设计者把“谁拥有哪一段物理内存”写成显式的树，而不是靠一个全局分配器的善意。证明关心的正是这棵树：派生边在，权限在；边断了，权限就必须不在。

capability 派生还可以衰减。持有一个较宽的权限，可以造出只读、只发、只收的后代，不能反过来加宽。这和类型系统里的子类型方向相反：这里允许的是收缩，不是扩张。形式化的好处是，衰减规则一旦写进规格，检查器会拦住所有“悄悄加权限”的捷径。

证明账单：什么被写下，什么仍靠运维#

把 seL4 的保证写成运维能用的边界，比复述“已验证”有用：

账单的第一项是规格风险：定理相对于规格为真，规格漏掉的场景不会让检查器报警。第二项是维护成本：人年不是沉没成本，而是随代码一起滚动的固定开销。第三项是接口贫瘠：POSIX 应用不能直接搬进来；隔离强，生态小。第四项是时间：功能正确不自动给出实时保证。最坏执行时间是另一次分析，而且对流水线和缓存模型敏感。

Bernard Blackham、Yao Shi 与 Heiser 等人在 RTSS 与 EuroSys 上做过 seL4 的最坏执行时间工作。那是另一份模型、另一组假设，不是功能精化的推论。有人把“被证明的内核”听成“延迟有界的内核”，这是把两个定理的标签贴到了同一份二进制上。

设备直通是另一条硬边界。若外设可以做 DMA，而系统没有 IOMMU 把总线访问关进允许的物理页，设备就可以在内核证明范围之外写内存。定理不会因此变假——它从未把这块总线写进去。部署高保证系统的人必须把这条假设当成配置约束，而不是当成内核自己会处理的特性。

2020 年 4 月，seL4 Foundation 在 Linux Foundation 下成立，证明产物、规格和参考手册按发布版本归档。这解决的是治理问题：一份靠人年堆出来的证明，如果没有持续的机构接住，三年后就会变成不可复现的文物。机构接住了，也不等于每一块开发板、每一次交叉编译都自动继承旧定理。换架构、换编译器版本、打开一个新的内核配置，通常意味着再付一次证明账单。

所以 seL4 适合的位置很窄也很硬：高保证隔离层、分离内核、需要把特权入口收到 IPC 门上的系统。它不是 Linux 的替代品。谁要在上面跑容器编排，仍要把庞大的用户态重新纳入可信计算基——证明不会跟着容器镜像一起分发。

混合关键度调度（MCS）是后来另付的一笔证明。实时线程的时间预算、超时和通知被写进内核之后，功能精化要重新覆盖这些路径。它让无人机、汽车和分离式虚拟化可以用同一份内核同时跑关键任务和普通任务，但那是新定理，不是 2009 年那份精化的免费推论。

IPC 性能是微内核活下来的另一半故事。Liedtke 的论点是：只要把快捷路径写瘦，跨地址空间发一条消息可以接近函数调用。seL4 把这条路径写进了被证明的 C，并在 ARM 上给出过与当时最快 L4 同量级的数字。证明没有自动让 IPC 变快；快是手工写出来的，证明只保证这条快路径仍然遵守规格。运维若在用户态堆了多层服务，每一次往返仍要付一次内核入口，隔离的形状会把延迟乘上去。

时间通道是完整性定理明确没买的东西。缓存颜色、刷缓存、确定性调度可以缩小通道，但那是另一组论文和另一组假设。有人把“信息流被证明”听成“侧信道不存在”，会在多租户部署里把定理用到它从未覆盖的物理层。正确的读法是：定理排除的是能力模型里的非法读，不是示波器上的相关。

证明停住之后，系统还要谁来信#

把 seL4 部署进产品，信任计算基不会 magically 缩到那 8700 行 C。启动加载器、设备树、时钟源、以及把能力授给第一个用户态任务的 bootstrap 代码，都在定理外面。团队通常用隔离来补：把未证明的代码关进自己的地址空间，只给最小能力。这能缩小事故半径，但不能把事故变成“定理保证不会发生”。

用户态的 CAmkES 一类组件框架，是在证明内核之上再搭一层架构纪律：组件之间只通过被授予的 endpoint 说话。它提高的是工程一致性，不是新的内核定理。评审仍要问：这个驱动持有哪些能力、撤销之后是否还有残留映射、中断是否能变成对别的组件的拒绝服务。

所以读 seL4 最有用的姿势不是收集“已验证”徽章，而是带着一张清单走：功能精化覆盖哪一版配置、二进制证明对应当时哪条工具链、完整性与信息流各假设了什么、时间通道和 DMA 被写进哪一份运维约束。清单上的空格，就是账单。

能力空间本身也是一张要付费的图。每个线程控制块指向自己的 CNode，查找一条能力可能要走多层槽位。为了让证明写得完，查找规则被写得很死：没有“顺便在全局表里搜一下”这种捷径。工程上这意味着启动配置必须把能力图铺对，铺错不会在运行时被内核好心纠正，因为内核根本没有那份全局视野。这既是隔离，也是运维必须把初始能力布局当成代码来审的原因。

跨域连接#

• 证明：seL4 把“正确”从测试覆盖率改写成精化定理，于是读者必须问证明的是哪一句、相对于哪份规格、假设写在哪。机器检查排除的是推理步骤里的跳跃，不是规格与现实之间的裂缝。运维能用的结论因此永远带着前提：换架构、换编译器、把驱动放进内核，定理都不会自动搬家。测试抽的是样本，定理切的是整类非法状态；两者回答的问题本来就不同，不能用其中一个的成功去冒充另一个。
• 范畴论：精化链是一串保持可观察行为的箭头：规格到原型、原型到 C、C 到二进制。每一箭都要证明合成后仍指向同一类行为。范畴语言在这里不是装饰，它提醒你：对象换了（C 文本变成机器码），若没有函子式的对应，上层定理不能当下层事实用。翻译验证做的正是补上这枚函子；缺了它，精化在编译器门口就断了。
• 国家能力：形式化内核像一种极强的制度能力——把暴力（特权指令）关进少数可审计的入口，并留下书面证据。代价与国家能力文献里的观察同构：把强制力收紧，需要持续的专业官僚（证明工程师）和昂贵的文书（引理）。能力不是一次立法完成的，停发证明维护，隔离承诺就会退化成普通微内核。基金会接住证明产物，相当于给这套强制力配上可延续的行政机构。
• 组合数学：内核状态空间是对象、capability 与派生边的组合。测试只能抽样本；定理要把非法组合整类切掉。组合爆炸正是测试在这里失败的原因：权限拓扑的边一多，手工用例覆盖的是稀疏截面，不是那张图。衰减与回收进一步把组合从“静态清单”变成“带时间的树”，需要证明的是整棵树的闭合性质，而不是某几个叶子碰巧合法。

参考文献#

• Klein, G. et al. seL4: Formal Verification of an OS Kernel. ACM SOSP, 2009.
• Klein, G. et al. Comprehensive Formal Verification of an OS Microkernel. Communications of the ACM 57(6), 2014.
• Sewell, T., Myreen, M. O., Klein, G. Translation Validation for a Verified OS Kernel. ACM PLDI, 2013.
• Sewell, T. et al. seL4 Enforces Integrity. International Conference on Interactive Theorem Proving, 2011.
• Murray, T. et al. seL4: From General Purpose to a Proof of Information Flow Enforcement. IEEE Symposium on Security and Privacy, 2013.
• Elphinstone, K. & Heiser, G. From L3 to seL4: What Have We Learnt in 20 Years of L4 Microkernels? ACM SOSP, 2013.
• Blackham, B., Shi, Y., Chattopadhyay, S., Chou, A., Heiser, G. Timing Analysis of a Protected Operating System Kernel. IEEE RTSS, 2011.
• The seL4 Foundation. seL4 Reference Manual 与对应发布版本的 Verified Configuration 说明, 2020 年起。

延伸阅读#

• Heiser, G. et al. The seL4 Microkernel: An Introduction. Data61 / seL4 Foundation 公开讲义。
• Liedtke, J. On Micro-Kernel Construction. ACM SOSP, 1995.（L4 性能论证，seL4 的设计前史）
• Klein, G., Andronick, J. 等. CACM 2014 长文配套的证明架构图与可信计算基清单。