| 摘要: |
| 操作系统是软件的基础平台, 操作系统内核的安全性往往影响重大. Rust是逐渐兴起的内存安全语言, 具有生命周期、所有权、借用检查、RAII等安全机制, 使用Rust语言构建内核逐渐成为当前热门的研究方向. 但目前使用Rust构建的系统多包含部分unsafe代码段, 无法从根本上保证语言层面的安全性, 因而针对unsafe代码段的验证对于保证Rust构建的内核正确可靠尤为重要. 以某使用Rust构建的微内核为对象, 提出GhostFunc的safe和unsafe代码段组合验证方法, 将两类代码段采用不同层级的抽象, 使用GhostFunc进行组合验证. 针对任务管理与调度模块, 基于$ {\lambda _{{\text{Rust}}}} $形式化Arc<T> 等unsafe代码段, 并给出形式化GhostFunc的具体实现, 完成此方法的验证实例. 所有验证工作基于定理证明的方法, 在Coq中采用Iris分离逻辑框架完成正确性的验证. |
| 关键词: 形式化验证 操作系统内核 分离逻辑 Rust 定理证明 |
| DOI：10.13328/j.cnki.jos.007347 |
| 分类号:TP311 |
| 基金项目:国家自然科学基金(U2341212) |
|
| GhostFunc: Verification Method for Rust Operating System Kernel |
|
HE Tao, DONG Wei, WEN Yan-Jun
|
|
College of Computer Science and Technology, National University of Defense Technology, Changsha 410073, China
|
| Abstract: |
| The operating system serves as the foundational platform for software, and the security of its kernel is often of paramount importance. Rust, a memory-safe programming language that has steadily gained popularity, incorporates safety mechanisms such as lifetimes, ownership, borrowing checks, and RAII. Using Rust to build kernels has emerged as a prominent area of research. However, systems built with Rust often include some unsafe code segments, which prevent the language from offering comprehensive safety guarantees at the language level. As a result, verifying these unsafe code segments is essential to ensuring the correctness and reliability of Rust-based kernels. This study proposes a method for combining the safe and unsafe code segments, called GhostFunc, to verify a microkernel constructed with Rust. Different levels of abstraction are applied to the two types of code segments, and GhostFunc is used for combined verification. Focusing on the task management and scheduling module, this study formalizes unsafe code segments such as Arc<T> using λRust and presents the formal implementation of GhostFunc. An example verification of this method is also provided. All verification efforts are based on theorem proving, and correctness is validated in Coq using the Iris separation logic framework. |
| Key words: formal verification operating system kernel separation logic Rust theorem proving |
