无Bug微内核seL4 7.0.0发布

Linux 微内核 CMake

摘要

高可靠性微内核seL4 7.0.0版本发布，提供了另外一种基于CMake的构建系统，支持源码树外构建和交互式配置。

正文

微内核seL4 7.0.0版本发布，提供了另外一种基于CMake的构建系统，支持源码树外构建和交互式配置。该版本还支持独立的ia32构建，并包含aarch64的详细文档。

seL4是一个高可靠性开源微内核，提供基于端到端验证的强隔离保障。实际上，这是说seL4代码库是无Bug的，当“验证假设”满足时，就发生指定的行为。正因如此，它已经被用于将运行在同一个处理器上的受信任组件和不受信任组件隔离。

seL4微内核由NICTA开发和维护，并通过了NICTA（现在是Data61的Trustworthy Systems Group）的正式验证，目前归General Dynamics C4 Systems（GDC4S）所有。2014年，“为了帮助每个人构建更可信赖（安全、无风险、可靠）的计算机系统”，NICTA和GDC4S决定开源seL4。

功能正确性初步验证是在2009年通过L4.verified项目完成的。该项目表明，代码正确地实现了正式的内核规范。后续对该内核的全面正式验证证明，该规范既能提供期望的高级安全属性，如“可用性、权限限制、完整性和保密性”，又能提供那些用于代码及二进制级别转译的属性。总的结果就是一个通用操作系统内核的首次端到端验证。值得注意的是，10多年来，该验证一直随着内核的发展而变化，成为在这种规模下前所未有的验证。

按照设计，虽然seL4内核有大量的验证工作，但它仍然保持着很高的性能，实际上，它已经促进了性能优化的实现。当前，验证提供的属性和不变量用于获悉内核的最坏情况执行时间（WCET），从而改进内核实现，进一步减少WCET。类似地，增加的“快速路径（fastpath）”在可能的时候会自动提升进程间通信（IPC）速度。后来，该验证经过了扩展，不管是否使用了快速路径，都可以验证内核行为是否符合规范。这项工作的结果就是一个速度、安全性、可靠性可证的内核，其应用领域包括国防、汽车、航空、医疗设备和工业自动化。

美国通过SBIR（小型企业创新研究）项目发放了超过230万美元奖金，用于资助那些与seL4相关的国防项目。在其中一个这样的项目中，SMACCM团队使用seL4构建了具有“非法入侵高度复原性”的无人机（UVV）。该团队使用seL4将运行非关键代码的虚拟化Linux实例和运行在同一块“任务板（mission board）”上的关键代码隔离开。在红队设法非法入侵时，蓝队仍然能够有效地操作基于seL4的系统。该系统最初开发时使用了一个普通的四轴飞行器，后来换成了由Boeing开发的“无人小鸟（ULB）”无人直升机。但是，seL4不限于国防承包商。由于支持Raspberry Pi 3，基于seL4开发安全、无风险、可靠的系统也在学生的研究范围内。

虽然seL4在安全操作系统开发领域最先进，但按照定义，它是最小的，不是一个像Linux这样的全功能操作系统，并没有包含所有为了提供使用便利的东西，比如，支持各种设备及简单的进程间通信。

开发和验证工作的当前状态来自经常更新的开发和验证路线图。常见问题的答案可以从项目的FAQ页查看。

查看英文原文：seL4 Bug-Free Microkernel 7.0.0