seL4微内核：简介 [PDF]
Hacker News 摘要原标题：The SeL4 Microkernel: An Introduction [pdf]
本文档是关于seL4微内核的介绍和概述。seL4被认为是安全和安全关键系统的首选操作系统内核，并适用于嵌入式及网络物理系统。文中讨论了seL4的确保和安全特性，以及其性能表现，并列出了常见的使用场景。
seL4是一个小型的操作系统微内核，最初开发于1990年代中期，属于L4微内核系列。与传统的单体内核操作系统（如Linux）不同，seL4将操作系统的核心功能最小化，使其具有更小的受信计算基础，从而减少了攻击面。seL4还具有虚拟化支持，可以运行完整的操作系统（例如Linux）作为虚拟机，这为系统服务提供了另一种配置方式。
文档详细介绍了seL4的验证过程，包括实现正确性证明和安全强制执行的相关内容。seL4是世界上首个在源代码级别具有机器验证功能的操作系统内核，其证明过程是当前已知最大、活跃维护的验证基础之一。
seL4采用了基于能力的访问控制机制，能力是可以精细控制的访问令牌，能支持最小权限原则，有助于增强系统的安全性。文中阐述了能力的工作原理和其在系统安全中的作用，并将其与传统的访问控制列表（ACL）进行了对比，强调了后者在易受混淆的副代理问题上的局限性。
在实时支持方面，seL4不仅具有普通的实时调度功能，还针对混合关键性系统提供了强大的支持。混合关键性系统通常由不同关键性组件组成，seL4确保了高关键性组件不受低关键性组件的影响。
文档对seL4的性能表现进行了描述，指出其在实际应用中不仅保持了高效的IPC（进程间通信）性能，还在安全和效率之间达成了良好的平衡。
实际部署过程中，seL4支持逐步的网络安全改造，允许保留现有的较大系统组件以降低成本及风险。文中提供了一些实现的示例和推行框架，帮助开发者以模块化的方式逐步构建和转型系统。
最后，文档强调了seL4作为兼顾安全与性能的现代操作系统内核在未来的研发方向，以及其在更广泛应用场景中的潜力。