用 Rust 做单地址空间微内核,兼顾最小性与能力控制
safeL4: Rethinking Safe-Language-Based Single Address Space Microkernels
Zheyuan Xu, Xiaobei Zhang 等 10 人
基于语言隔离的单地址空间微内核能省掉硬件隔离开销,但难以保持最小性和细粒度的能力控制。safeL4 用低层抽象封装所有 unsafe 操作来保证最小性,并借助安全语言的对象能力,实现覆盖全部系统资源操作的 capability 系统。作者用 Rust 实现了原型。
参考价值用语言级隔离代替硬件隔离来降低开销,和用户态 eBPF 运行时靠 verifier 加运行时检查保证扩展安全是同一类权衡,安全边界的划分方式可以借鉴。
- 原语平均比 seL4 快 1.9×
- ASPLOS'27
- Rust / 安全语言
- 安全