2026 年 8 月 21 日，一个数学证明让内核安全有了新标准
2026 年 8 月 21 日，Proofcraft 宣布 seL4 微内核的机密性（confidentiality）证明在 AArch64 上完成。这是最后一块拼图：功能正确性、完整性、机密性，三张形式化证明在同一款内核的 64 位 Arm 版本上全部齐了。全球范围内，这是第一个在主流商业架构上拿到完整安全证明栈的操作系统内核。
这件事的反常识之处在于：内核安全领域向来靠测试、靠 fuzzing、靠漏洞修补后打补丁。seL4 的做法是把内核行为写成数学规约，然后机器验证代码实现与规约一致。从此对于这款内核，「这段代码有没有信息泄漏」从工程猜测变成了可被核验的命题。
三张证明分别证了什么
seL4 的三张证明构成一个层次结构，每一层的边界清晰且不重叠。功能正确性（functional correctness）证明的是内核实现与形式化规约逐行一致，代码行为就是规约描述的行为，没有意外。完整性（integrity）证明的是应用程序无法在未获授权的情况下修改其他应用的数据。机密性（confidentiality）证明的是应用程序无法在未获授权的情况下获知其他应用的信息——这是本次补齐的最后一块。
三张证明组合后得到的结论是：在 AArch64 上运行 seL4 的系统，内核层面的安全隔离有完整的数学支撑。从汽车的安全关键域与信息娱乐域共享同一块 SoC，到工业控制器的硬实时任务与网络接口共存，这类混合关键性（mixed-criticality）场景正是 seL4 的核心应用域。有了这三张证明，系统设计师在安全分析文档里可以写进一条以前写不了的结论。
图：AArch64 证明状态总览，机密性标记为已完成。来源：Proofcraft
证明的边界被诚实地写进了文档
Proofcraft 官方的 assumptions 页面在本次发布后同步更新，明确说明：机密性证明基于二进制级硬件模型，该模型假设所有相关信息通道都被捕获。随即加了一句：「We know this not to be the case.」——他们知道这个假设在现实中并不成立。
具体而言，证明覆盖的是存储信息通道（storage channels），明确不覆盖时序侧信道（timing channels）。Hacker News 的讨论区里，第一条高赞评论就是「接下来肯定会有时序攻击把这个结论推翻」。技术澄清随即跟上：证明从没声称覆盖时序通道，所以时序攻击无法「推翻」这个证明——它在自己声明的范围内仍然成立，只是那个范围比有些人想象的小。
要把时序侧信道也纳入证明，需要软件与硬件设计（Verilog 级别）一起验证，且只对特定 core 有效。社区讨论给出了一个更务实的方向：用已知变时操作的清单（秘密依赖分支、秘密依赖数组索引、架构特定的除法运算等）配合 FaCT 类常时语言，在程序级做验证，大幅收窄暴露面。这条路比全硬件证明可行得多，但目前仍「nowhere near ready」。证明边界的诚实标注，恰恰是形式化方法成熟度的标志之一——含糊的声明才应该让人担心。
三个国家级机构同时付钱的信号
本次机密性证明的直接资助方是英国 NCSC（国家网络安全中心）。同期，DARPA PROVERS 项目在资助 seL4 的 MCS（混合关键性配置）在 RISC-V 上的验证工作，德国 Cyberagentur（联邦国防网络创新局）也在持续投入。三个主权国家的国家级机构并行出钱，投向同一个开源微内核的形式化验证工作。
这个信号可以从两个角度读。其一：形式化验证已经从学术论文走到了国防采购的决策层，证明本身的可信度经受住了严肃需求方的评估。其二：这些资助方代表的场景——国防、关键基础设施、高保障嵌入式系统——恰好是愿意为安全验证付出额外工程成本的买家。Arm 生态里能同时满足「64 位主流架构」和「有完整安全证明」这两个条件的内核，目前只有 seL4。
图：MCS 混合关键性配置在 RISC-V 上的验证状态图。来源：Proofcraft
从「测过了」到「证过了」，证书的有效范围是关键
seL4 的功能正确性证明最早完成于 2009 年，针对 ARMv6，是学术界里程碑。从那时到现在，证明的覆盖范围持续扩展：架构从 32 位 Arm 到 64 位、从 x86 到 RISC-V，配置从基础内核到 MCS，证明从功能正确性到完整性再到机密性。这条路推进了 17 年。
对于系统架构师而言，AArch64 完整证明栈的实际意义在于：这是第一次在主流移动与嵌入式 SoC 的主力架构上，内核安全隔离可以被放进正式安全论证文档而不需要附加「这是我们测试过的」的注脚。测试能发现已知的错误，证明覆盖了规约描述的所有情况——两者的区别，在安全论证的严格度要求越高时越关键。汽车功能安全（ISO 26262）、航空（DO-178C）、工业控制（IEC 62443）这些领域的认证机构，对「证明覆盖了什么、没覆盖什么」的问题比一般工程评审更敏感。seL4 现在给出的答案，在这些场景下比以前更完整，同时也更诚实。
内核安全的验收标准已经从「测过了」升级到「证过了」。这张证书的有效范围写得很清楚：存储信息通道，不含时序侧信道。能把边界说清楚的证明，比边界模糊的承诺更值得信任。
参考链接：
- Proofcraft 官方发布公告
- seL4 官方 assumptions 页面
- HN 讨论
