seL4 背景知识

1 seL4 演变

1.1 微内核

微内核发展到目前为止经历了三代, 这里做一些归纳。参考《现代操作系统: 原理与实现》中操作系统结构一章, 关于微内核架构发展的介绍。

• 第一代微内核设计将许多内核态功能放到用户态, Mach 微内核是第一代微内核的代表。
• 第二代微内核设计将对 IPC 优化并实现非常小的内核(最小化原则), L4 被认为是第二代微内核的代表。
• 第三代微内核设计将对内核 安全性 进行增强, 例如 seL4 的实现 Capability 机制和形式化证明方法等。

1.2 L4 家族

L4 是一个非常小的高性能微内核家族, 由 Jochen Liedtke 在 90 年代早期开发的第一个 L4 微内核演变而来。L4 微内核家族的版本变迁描述从这个图像源找到, 参考 L4_microkernel_family

从 1993 年到 2013 年的 L4 微内核家族树。黑色箭头表示代码, 绿色箭头表示 ABI 继承。

1.3 seL4 内核

• 2006 年, 对于 seL4 是一个开始。
• 2009 年, seL4 完成了功能正确性的正式证明。
• 2014 年 7 月 29 日, seL4 开源发布。

2 seL4 概念

• seL4 是 L4 微内核家族的一员, 是世界上最先进、最可靠的操作系统内核 。它的特别之处是使用形式化证明(安全性), 而且不对性能造成影响(高性能)。
• seL4 是内核, 内核是操作系统的核心组件。
• seL4 构建的 Project , 列举一些官方的开源实现, 例如 verification, seL4test, seL4bench, CAmkES, x86 Camkes VMM

3 seL4 上手

• 跟着 seL4 官方教程 , 结合实验例子和源码, 一步一步学习和分析包括 seL4 的系统。
• 参考 seL4 说明手册 , 是更加权威的介绍。
• 使用 seL4 开源工程, 开发调试。
• 了解 seL4 的构建系统, 关于 seL4 构建系统 。

4 seL4 价值

• 学习的角度, 微内核, 轻量级, 教程全
• 商业角度, 安全, 高性能