seL4 微内核

定义

seL4 是 L4 微内核家族的成员,由澳大利亚 NICTA(后并入 CSIRO Data61)开发,2009 年完成从抽象规格到 C 实现的完整形式化验证,是世界上第一个被数学证明功能正确的通用操作系统内核。

验证意义

研究团队用 Isabelle/HOL 证明了其 C 代码严格符合形式化规格,随后进一步证明了二进制码与源码的一致性以及完整性、保密性等安全属性——这意味着在验证假设范围内,seL4 不存在缓冲区溢出、空指针解引用等实现层缺陷。

设计

seL4 遵循 L4 传统:极小的内核(约一万行 C 代码)、高性能 IPC,并采用基于能力(capability)的访问控制统一管理所有内核资源授权。

应用

seL4 用于对安全性与可靠性要求极高的领域,如军用无人机(DARPA HACMS 项目)、汽车与航空电子、安全通信设备。项目现由 seL4 基金会维护,开源发布。