1 seL4 演变 1.1 微内核 微内核发展到目前为止经历了三代, 这里做一些归纳。参考《现代操作系统: 原理与实现》中操作系统结构一章, 关于微内核架构发展的介绍。 第一代微内核设计将许多内核态功能放到用户态, Mach 微内核是第一代微内核的代表。第二代微内核设计将对 IPC 优化并实现非常小的内核(最小化原则), L4 被认为是第二代微内核的代表。第三代微内核设计将对内核 安全性 进

内核内存分配 seL4微内核不会动态地为内核对象分配内存,相反,必须从应用程序控制的内存区域,通过未分配内存能力显式地创建对象。也就是: 为了创建新对象,应用程序必须要有明确的授权(通过这些未分配内存能力)。对象一旦创建就会消耗固定数量的内存。 这些机制可以用于精确控制特定数量物理内存对应用程序的可用性,包括能够强制隔离应用程序或设备之间的物理内存访问。除了硬件专用的以外,内核本身不要求任何

General Dynamics C4 Systems和NICTA宣布开源Secure Embedded L4（seL4）微内核，源代码托管在GitHub上，采用的是GPLv2许可证。seL4是世界上第一个形式证明安全增强的通用操作系统内核，开发者宣称它是第一种没有漏洞的软件，能防止系统崩溃或恶意攻击。 From: http://www.solidot.org/story?sid=40536