CertiKOS — 把整个并发内核拆成 30 多层每层都被 Coq 证过

是什么

CertiKOS 是一个整个内核都被定理证明器机器证明过的并发操作系统，由耶鲁 FLINT 组（Gu、Shao、Chen 等人）做出。日常类比：像盖摩天大楼——你不可能一次画一张图证整栋楼不会塌；CertiKOS 的做法是把楼拆成 30 多层，每层独立画图、独立请人验收、再证明”一层叠一层之后整栋还成立”。

整个内核（叫 mC2 / mCertiKOS）只有约 6500 行 C 和汇编，但配套的 Coq 证明大约 20 万行。它在 8 核 x86 上跑得动 shell、ping、httpd 这些真实程序。这是历史上第一个端到端机器证明的并发内核——比它更早的 seL4（NICTA 2009）只证了顺序执行版。

放回更大的图景：从 1970 年代 Hoare 逻辑到 2009 年 seL4 再到 2016 年 CertiKOS，OS 形式化验证走了 40 年；CertiKOS 的贡献是让”分层验证 + 并发”这两块同时工作。

为什么重要

不理解 CertiKOS，下面这些事都没法解释：

为什么”内核 bug 一个能让整台机器沦陷”还没让形式化验证全面普及——证明成本曾经是天文数字，CertiKOS 给了一条可行路径
为什么”分层抽象”是整个软件工程的核心招式——CertiKOS 把它推到了每层都有数学定义 + 数学证明的极限
为什么并发证明比顺序难 10 倍——多线程交错让状态空间爆炸，CertiKOS 用 CCAL（并发认证抽象层）把它压回可证范围
为什么 OSDI 2016 把 Best Paper 给了它——它解决了 OS 验证圈卡了 10 年的问题：怎么把”证一个内核”做成”证 30 个小模块”

核心要点

CertiKOS 的方法学可以拆成 三件事：

Deep specification（深规约）：每层写一份”完整到上层不必再看下层实现”的接口契约。类比：你用洗衣机，不用懂电机怎么转——只要”放衣服按按钮，洗完拿出来”这份说明书够准确。深规约就是要把这份说明书写到不漏任何行为。
Certified Abstraction Layers（认证抽象层 CAL）：把内核切 30 多层。最底是裸硬件、往上是中断、内存管理、进程、调度、IPC、文件系统……每层只调下一层的规约（不调实现），并附带一份 Coq 证明：本层实现满足本层规约。所有证明用纵向拼接最终得到”整个内核满足顶层规约”。
CCAL（并发版 CAL）：顺序版 CAL 不够用——多线程会交错。CCAL 加了”日志（log）+ 环境状态机”两件武器：每层用一份”如果别的线程做这些动作，我会怎样”的环境模型；下层的并发细节被吸进上层的环境模型，证明就退化成单线程推理。

三件事合起来，让”证一个并发内核”变成”证 30 多个小模块 + 证拼接成立”。

实践案例

案例 1：一层的接口长什么样

最底层叫 MBoot（裸机引导后），它给上层提供的”完整接口”包括：物理内存读写、页表寄存器、中断使能位等。再上一层 MAL（Memory Abstraction Layer）的规约长这样（伪 Coq）：

Definition palloc_spec (s: state) : option (state * Z) :=
  match find_free_page s with
  | Some i => Some (mark_used s i, i)
  | None => None
  end.

读法：拿状态 s，找空页 i，返回”标记 i 为已用后的新状态”和页号。MAL 的实现用一段 C 维护页表，再加一份 Coq 证明：这段 C 跑起来等价于上面这个数学函数。MAL 的上层（比如进程层）只看 palloc_spec，永远不看 C 代码。这就是”深规约”的力量——上下层完全解耦。

案例 2：30 多层叠起来怎么证

假设内核要证的顶层定理是 “fork() 后两个进程隔离”。证明链像这样：

顶层规约 (process isolation)
  ↓ 由 进程层 实现 + 证
进程层规约 (sched + mem + IPC)
  ↓ 由 内存层 + 调度层 实现 + 证
内存层规约 (paging) + 调度层规约 (round-robin)
  ↓ ......
最底层规约 (raw machine)
  ↓
真实硬件

每个箭头是一份独立 Coq 证明。Coq 的”模块化”机制保证：只要每条箭头都成立，端到端定理自动成立。这就是 CertiKOS 把 20 万行证明拆成可管理块的关键——任何一层改实现，只需重证它自己那一段。

案例 3：并发怎么没把证明搞炸

mC2 跑在 8 核上。如果朴素地把所有线程交错都列出来证，状态空间立刻爆炸——n 个线程各 k 步就是 (n·k)! 量级。CCAL 的招数是：每层把”别的线程的影响”封装成一个环境状态机。比如内存分配层在自己的规约里加一句”环境可能在我两步之间改 page table”，但怎么改已经被下层证明限制成了几种合法情况。

结果是：上层做证明时看到的世界还是单线程的——只是状态会”自己跳变”几下。这种”把并发吃进规约”的招数，和 Iris 程序逻辑（同年）思路相通，CCAL 是把它推到内核规模的工程化版本。

案例 4：信任边界在哪里

CertiKOS 的端到端定理大致是：“如果 Coq 内核没 bug、CompCert 没 bug、x86 ISA 公理化无误、汇编器和 BIOS 没 bug，那么 mC2 二进制运行起来满足顶层规约。” 这一长串”如果”就是信任基——大约几万行第三方代码加几页硬件公理。CertiKOS 不消灭信任基，它把信任基从”几百万行内核 + 编译器 + OS”压到”几万行底层基础”。这就是工程上的真正进步：信任基越小，被攻破的概率越低。

踩过的坑

“证明完了就一定对” 是误解：CertiKOS 信任基包括 Coq 内核、CompCert、汇编器、链接器、硬件 ISA 模型。任何一个错了，定理仍然不保证机器码正确。这一点和 CompCert 一样诚实但容易被忽略。
写规约比写实现难：每层 deep spec 通常比该层 C 代码还长——因为要把所有边界情况精确化。新手以为”证明慢”，其实是”想清楚慢”。开发节奏从”先写代码再调试”变成”先想清楚再写代码再证明”，这种心智切换比学 Coq 语法还难。
改一行 C 可能要重证 5000 行 Coq：层与层之间紧耦合在规约上，改实现 OK，改规约会触发上层一连串重证。所以 CertiKOS 的”分层”是给证明用的，不是给开发速度用的——选择层数和层边界本身就是设计决策。
不支持完整 POSIX：mC2 是一个研究内核，syscall 数量、文件系统、网络栈都是简化版。不能直接拿去替代 Linux。商业化的认证内核（如 seL4）是另一条工程化更深的路。
硬件模型自己也是一份规约：x86 内存模型、中断时序、TLB 行为都被写成 Coq 公理。如果公理写错了（比如忽略了某个 TLB 边界情形），定理在数学上仍然成立，但对真实硬件不成立。这是形式化方法最难的边界——数学和物理之间的接缝。

适用 vs 不适用场景

适用：

安全关键场景（航空、卫星、加密设备 hypervisor）需要内核级形式化保证
研究并发证明、分层验证方法学
给学界提供”端到端可证内核”的参考实现，配合 CompCert 形成”源码到机器码全栈证明”

不适用：

通用 OS 替代（Linux/Windows/macOS）——功能、性能、生态都差太远
快速迭代的产品内核——证明成本压垮开发速度
不愿建立 Coq + CompCert + 汇编器信任链的团队——信任基太大
把它当”更安全的 Linux”卖——它是研究 artifact，不是发行版

历史小故事（可跳过）

2009 年：澳大利亚 NICTA 团队完成 seL4——第一个机器证明的微内核（Isabelle/HOL，仅顺序版）
2010 年代初：耶鲁 FLINT 组（Zhong Shao 主导）开始思考”怎么把 seL4 那种大块证明做成可组合的”
2015 年：Ronghui Gu 等在 POPL 发表 CAL（认证抽象层）的理论框架
2016 年：OSDI 论文发表，端到端 mC2 + CCAL，拿下 Best Paper
2017-2020：陆续做出 CertiKOS-hyp（hypervisor 版本）、用更精细的并发方法 push-pull 等
2020 年代：FLINT 后续工作进入 hardware-software co-verification 和 GDPR 级数据合规验证

这是一条”理论先行（CAL POPL 2015）→ 工程落地（OSDI 2016）→ 拓展应用”的典型学术路径。

学到什么

大问题靠拆——20 万行证明不是一次写出来的，是 30 多个小证明拼出来的；这种”分层 + 模块化”的招数和软件工程里的依赖倒置原则其实是一回事，只是 CertiKOS 把它推到了”接口可数学验证”的极限
接口比实现重要——deep specification 把接口写到完整，上下层就可以独立工作；任何一层换实现，上层不必动一行
并发证明的关键是”把别人的影响装进自己的状态机”——CCAL 和 Iris 同时给出了答案，思路相通但落地形态不同
形式化验证是”诚实工程学”：CertiKOS 的论文反复列出”什么没证、信任谁”——这是科学态度，不是缺陷；任何号称”完全证明”却不画信任边界的方案都该警惕
理论喂工程要 7 年：从 2009 年 seL4 到 2016 年 CertiKOS，从顺序到并发花了一代人；从 POPL 2015 的 CAL 到 OSDI 2016 的端到端落地也用了一年——大块工程不可能一蹴而就

关联

compcert —— CertiKOS 的 C 代码经 CompCert 编译，二者拼起来才能从 C 一路证到机器码
calculus-of-constructions —— Coq 的理论根基，CertiKOS 的所有证明都是 CIC 项
hoare-logic —— 程序证明的祖师爷，deep spec 沿用其前后条件思想
iris-2015 —— 同年并发程序逻辑，CCAL 在内核规模实现了相通思路
dafny-2010 —— 对照路线：自动化求解器 vs CertiKOS 的交互式证明
boogie-2005 —— 中间验证语言路线，是 Dafny 等系统的后端
frama-c-2012 —— 直接对 C 做契约式验证，是另一种”先 C 后证”的工程路径
acl2-2000 —— 老牌定理证明器，硬件验证传统强项

反向链接

acl2-2000 —— ACL2 — 用纯 Lisp 当数学对象，机器证明工业级硬件正确
calculus-of-constructions —— Calculus of Constructions — 让程序和数学证明共用一种语言
compcert —— CompCert — 每条优化都被数学证明保持语义的 C 编译器
exokernel-1995 —— Exokernel — 把抽象推到用户态的极致设计
frama-c-2012 —— Frama-C — 一个开源平台把 C 程序的多种验证方法拼到一起
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
hydra-1974 —— HYDRA — 用 capability 把整个内核重做成对象 + 票据
hyperkernel-2017 —— Hyperkernel — 让 SMT 求解器一键验证操作系统内核
iris-2015 —— Iris 2015 — 把并发推理拆成 monoid + invariant 两块积木
l4-1995 —— L4 — Liedtke 用 12KB 内核反驳”微内核必然慢”
multics-1965 —— MULTICS 1965 — 把计算机做成像电力一样的公共服务
the-os-1968 —— THE 1968 — Dijkstra 用分层 + 信号量造出第一个可证明的 OS