Atmosphere：用 Rust 开发并经 Verus 验证的微内核
来源标题：Atmosphere Verified Operating System
Atmosphere 是一个用 Rust 开发、经 Verus 验证功能正确性的全功能微内核，设计上类似 L4 系列微内核。它把设备驱动、网络栈、文件系统等大部分内核功能推到用户态，仅保留地址空间、页表、粗粒度内存管理和线程等最小机制。为简化验证，该内核目前采用大锁同步。
以下正文由 AI 翻译自 Hacker News 最新（原文版权归原站所有），可能存在偏差，重要内容请以原文为准。
Atmosphere 是一个用 Rust 开发、并用 Verus 进行验证的全功能微内核。在概念上，Atmosphere 与 L4 系列微内核相似。Atmosphere 将大部分内核功能推到用户空间，例如设备驱动、网络栈、文件系统等。该微内核只支持一组最小机制，用于实现地址空间、页表、粗粒度内存管理和执行线程，这些机制与地址空间一起实现了进程的抽象。每个进程都有一个页表以及一组可调度的线程。Atmosphere 允许线程通过一组系统调用控制其虚拟地址空间的布局，这些系统调用支持映射和取消映射页面，以及通过通信端点从其他线程接收页面。为简化验证，目前 Atmosphere 依赖大锁同步机制。
我们所有代码都用 Rust 开发，并证明其功能正确性，即用 Verus（一个类似 Dafny 的 Rust 自动化验证引擎）证明代码精化了一个高层规约。与先前工作类似，我们精心设计内核以将验证复杂度控制在可控范围内。尽管如此，Verus 仍允许我们实现链表等典型内核数据结构、支持经过验证的内存分配、开发关于页表的证明等。
Verus 与 Rust 的结合显著减少了验证工作量。平均而言，我们的代码证明与代码之比为 7.5:1，明显低于先前方法。此外，Rust 和 Verus 使我们能够对一个接口丰富、概念上类似经典 L4 系列微内核的微内核进行推理。
Xiangdong Chen, Zhaofeng Li, Jerry Zhang, Vikram Narayanan, Anton Burtsev. Atmosphere: Practical Verified Kernels with Rust and Verus. In Proceedings of the 1st ACM Symposium on Operating Systems Principles (SOSP 2025), October 2025. (Slides)
Xiangdong Chen, Zhaofeng Li, Sylvia (Lukas) Mesicek, Vikram Narayanan and Anton Burtsev. Atmosphere: Towards Practical Verified Kernels in Rust. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV 2023), October 2023.
正文由 探How 从来源站点 RSS 同步，内容未经改写；遇到排版缺失或需要图片、视频时请以原文为准。