无 Bug 微内核 seL4 7.0.0 发布

  • Kevin Neaton
  • 谢丽

2017 年 11 月 6 日

话题:安全DevOps

微内核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

安全DevOps