Hyperkernel — 让 SMT 求解器一键验证操作系统内核

待复核

是什么

Hyperkernel 是华盛顿大学 Xi Wang 组做的一个能用 SMT 求解器一键自动验证的操作系统内核。日常类比：传统内核证明像盖楼时请数学家手算每根钢筋——比如 seL4 用 Isabelle/HOL 写了约 20 万行手工证明；Hyperkernel 反过来——先把楼设计成”机器能算的形状”，然后让 Z3 自己跑一遍说”行”或”不行”。

它从 MIT 教学内核 xv6 改写而来，内核实现约 7600 行 C/汇编，验证一次大约几分钟，不需要人工写交互式证明脚本。论文全篇核心信息：改设计比补证明聪明——传统内核 syscall 有不定循环、不限大小的数据结构，SMT 求解器算不动；只要把 syscall 设计成”步数有限、数据有界”，Z3 一次决策就能确认它满足规约。

放回大图景：从 1970 年代 Hoare 逻辑、2009 年 seL4（Isabelle 顺序证明）、2016 年 CertiKOS（Coq 并发证明）到 2017 年 Hyperkernel——OS 验证一直在卷”证明便宜”。Hyperkernel 把”便宜”推到极致：写代码的人不必懂 Coq。

为什么重要

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

为什么”机器证明操作系统”听上去高不可攀，2017 年突然就有 PhD 在校项目能跑——关键不在求解器变强，是问题被重新切了
为什么 Z3、CVC5 这些 SMT 求解器从约束求解领域慢慢渗透进系统软件——它们能处理”有限状态决策”问题，比 Coq 那种”人写每一步”的交互式证明门槛低 10 倍
为什么”finite interface”（有限接口）成了之后一系列系统验证项目的设计原则——Yggdrasil 文件系统、Serval 验证器都沿用这条路
为什么”先改设计再做验证”是工程美学胜于纯学术——它承认人有限、机器有限，数学只在它能赢的地方用

核心要点

Hyperkernel 把”自动验证”做成可能，靠 三件事：

有限接口（finite interface）设计原则：每个 syscall 不能有不定循环、不能分配不定大小数据。比如不再像 xv6 那样让 fork() 内部循环遍历整张页表，而是改成”一次复制固定页数”，多余分多次调用。这样每个 syscall 的状态变化只有有限分支，SMT 一遍就能决策。
Python 规约 + LLVM IR 验证：程序员用 Python 写状态机规约和声明式安全性质（接口对 Z3 友好）；内核用 C 实现，验证器在 LLVM IR 上做符号执行，再把两边一起编成 SMT 查询交给 Z3。不在 C 语义上硬建模，也不靠交互式证明助手。
两层规约一致性：用 SMT 同时证 (a) LLVM 实现 ≡ Python 状态机规约，(b) 状态机规约满足若干声明式安全性质（隔离、引用计数正确、调度安全等）。两层都靠同一个 Z3，没有 Coq/Isabelle 介入。

三件事合起来，让”证一个内核”从”博士生多年手写证明”变成”写规约 + 让 Z3 自动跑”。

实践案例

案例 1：xv6 vs Hyperkernel 同一 syscall 的差别

xv6 的 wait() 实现里有这种代码：

for(p = ptable.proc; p < &ptable.proc[NPROC]; p++) {
  if(p->parent == curproc) ...
}

朴素 SMT 处理不动循环——NPROC 是参数，循环展开次数不定。Hyperkernel 把同一逻辑改写成”调用方传 PID，内核检查这个 PID 的父进程是不是我”。循环消失了——syscall 变成”O(1) 步定长操作”。功能上少一点便利，验证上一切自动。

案例 2：Python 状态机规约长这样（示意）

def sys_fork(s, pid):
    if pid >= NPROC:
        return state_error(s, "EINVAL")
    if proc_used(s, pid):
        return state_error(s, "EEXIST")
    return state_spawn(s, pid, current_pid(s))

读法：拿当前抽象状态 s 和目标 PID，三种情况返回三种状态。每种情况都是有限运算。验证器把这段 Python 规约与对应 C 编译出的 LLVM IR 一起编码成 SMT，让 Z3 检查任何输入下两边结果都对应相等。

案例 3：Z3 真的能跑完吗

文中报告：约 7600 行 C/汇编的内核实现，全套验证（实现-规约等价 + 声明式性质）在普通服务器上大约几分钟跑完。没有人工交互式证明脚本——查询交给 Z3。这和 seL4 的约 20 万行手写 Isabelle 证明形成强对比。代价是：内核功能更小（没文件系统并发、没复杂调度），且必须严格按”有限接口”原则写。

案例 4：找到的真实 bug

Hyperkernel 验证过程中发现 xv6 原版有若干隔离漏洞——比如某些 syscall 路径下子进程能读到父进程残留页面。这类 bug 在测试里很难触发，但 SMT 探索全部状态时一步就找到。这是”自动验证”对工程的直接回报：不是装饰品，是能抓 bug 的工具。

踩过的坑

“自动”的代价是”功能受限”：Hyperkernel 内核是单核的、没并发文件系统、调度极简。它证明了一个简单内核，不是”证明了任意内核都能这样做”。要做更大的内核，“有限接口”约束就成了功能枷锁。
设计 vs 验证两端拉扯：原本 xv6 设计追求”代码短小有教学性”，Hyperkernel 改写后”代码更死板”。写得不好看的代码有时是为了机器能算——这种取舍每个项目要自己权衡。
信任基包括 Z3 + Python 规约解释 + LLVM 工具链：Z3 有过历史 bug；初始化与 glue 代码也未验证。如果工具链错了，定理仍数学上成立，但对真实硬件不成立。信任边界要老实画。
对并发完全没办法：Hyperkernel 是顺序内核。并发情况下”有限接口”原则失效——线程交错让状态空间爆炸。CertiKOS 用 CCAL 处理并发但要写手工证明；Hyperkernel 用自动求解但只跑顺序。两条路当时没人合并。
“验证 = 完全正确”是误读：Hyperkernel 证的是”实现满足给定规约”。如果规约本身漏掉某种安全性质（比如没要求侧信道隔离），那种攻击仍然存在。规约是人写的，人会漏。
SMT 求解时间会爆炸：finite interface 不是免疫卡——某些 syscall 改完仍可能让 Z3 跑很久甚至超时。工程功夫一半花在”调整规约和实现，让 Z3 跑得动”。

适用 vs 不适用场景

适用：

教学验证：把”内核 + SMT”作为学生入门形式化方法的活教材，门槛比 Coq 低很多
嵌入式 / 安全关键的小内核：功能受限可接受，自动验证的低成本回报极高
验证基础设施研究：作为”finite interface + SMT”路线的基线，对照 seL4、CertiKOS 看不同验证哲学

不适用：

通用 OS 替代——功能远不足以替代 Linux 或商业 RTOS
高并发 / 多核内核——SMT 自动化扛不动并发证明
不愿接受”接口设计被验证约束”的项目——Hyperkernel 的核心是设计妥协换取自动化
需要侧信道、时序攻击等非功能性安全保证的场景——SMT 不直接处理这些
算法/数据结构密集型内核子模块（复杂调度器、文件系统 B-tree）——finite interface 会把它们改得面目全非

历史小故事（可跳过）

2008 年：Z3 发布，SMT 求解器进入工业级（z3-2008）
2009 年：seL4 在 NICTA 完成——Isabelle/HOL 写的约 20 万行手工证明
2016 年：CertiKOS 用 Coq 证并发内核（certikos-2016）
2017 年：Hyperkernel SOSP 发表，提出 finite interface + Python 规约 + LLVM/Z3 路线
之后：同组后续工作（如 Serval，OSDI 2019）把自动化验证推到更多系统软件；finite interface 思路继续被沿用

这是一条”求解器进步（Z3）→ 接口可判定化（finite interface）→ 系统软件验证（Hyperkernel）“的清晰技术链。

学到什么

改问题比改工具聪明——SMT 算不动不定循环，那就把内核 syscall 改成定长；这种”先迁就工具，再用工具赢”的思维在系统设计里反复出现
自动化不是免费的——交给机器的代价是接口设计被约束、功能要砍、并发暂时让位
Python 规约 + LLVM IR + 一个求解器工程上简洁——把”工具栈高度”压低，才让小团队也跑得起来
“证明便宜”会改变研究和工程的边界——以前内核验证是少数大组的事，Hyperkernel 之后小团队也能尝试
诚实画信任边界——Z3 / Python / LLVM / 硬件 ISA 都是信任基；列出来比假装”完全正确”更有科学态度
同代不同哲学的两条路——CertiKOS（Coq 手证、并发可证）与 Hyperkernel（SMT 自动、暂限顺序）回答同一问题：怎么造一个”对的内核”

一句话区分类似工作

Hyperkernel：finite interface + SMT 自动 = 顺序内核、几分钟跑完、零手写交互证明
seL4：顺序内核 + Isabelle/HOL 手证 = 约 20 万行手写证明、工业部署最深
CertiKOS：并发内核 + Coq 分层证明 = 表达力强但工程量巨大
Dafny：通用程序 + SMT 自动 = 程序员级工具，不针对内核
Frama-C：C 程序契约 + 多种后端 = 工业级 C 验证平台，更通用

关联

z3-2008 —— Hyperkernel 的核心求解器，所有定理由 Z3 决策
certikos-2016 —— Coq 手写并发证明路线，与 Hyperkernel 形成对照
hoare-logic —— 程序证明祖师爷，规约-实现等价是其思想延伸
dafny-2010 —— 同样走 SMT 自动化路线，但目标是程序员不是内核
boogie-2005 —— SMT 后端中间语言，Dafny 等系统的基础
frama-c-2012 —— C 程序契约式验证，工程化更深的另一路线
nelson-oppen-1979 —— SMT 多理论组合的理论根基

反向链接

disco-1997 —— Disco — 让没改过的商用 OS 在 64 核大机器上一起跑
exokernel-1995 —— Exokernel — 把抽象推到用户态的极致设计
hydra-1974 —— HYDRA — 用 capability 把整个内核重做成对象 + 票据
kami-2017 —— Kami — 在 Coq 里造硬件并自动编译到 Verilog
l4-1995 —— L4 — Liedtke 用 12KB 内核反驳”微内核必然慢”
multics-1965 —— MULTICS 1965 — 把计算机做成像电力一样的公共服务
the-os-1968 —— THE 1968 — Dijkstra 用分层 + 信号量造出第一个可证明的 OS
xen-2003 —— Xen 2003 — 让操作系统配合虚拟化，性能直接接近原生