Page 71 - 《软件学报》2025年第8期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(8):3494−3511 [doi: 10.13328/j.cnki.jos.007347] [CSTR: 32375.14.jos.007347] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
GhostFunc: 一种针对 Rust 操作系统内核的验证方法

何 韬, 董 威, 文艳军

(国防科技大学 计算机学院, 湖南 长沙 410073)
通信作者: 董威, E-mail: wdong@nudt.edu.cn

摘 要: 操作系统是软件的基础平台, 操作系统内核的安全性往往影响重大. Rust 是逐渐兴起的内存安全语言, 具
有生命周期、所有权、借用检查、RAII 等安全机制, 使用 Rust 语言构建内核逐渐成为当前热门的研究方向. 但目
前使用 Rust 构建的系统多包含部分 unsafe 代码段, 无法从根本上保证语言层面的安全性, 因而针对 unsafe 代码段
的验证对于保证 Rust 构建的内核正确可靠尤为重要. 以某使用 Rust 构建的微内核为对象, 提出 GhostFunc 的 safe
和 unsafe 代码段组合验证方法, 将两类代码段采用不同层级的抽象, 使用 GhostFunc 进行组合验证. 针对任务管理
λ Rust 形式化 Arc<T> 等 unsafe 代码段, 并给出形式化 GhostFunc 的具体实现, 完成此方法的验证
与调度模块, 基于
实例. 所有验证工作基于定理证明的方法, 在 Coq 中采用 Iris 分离逻辑框架完成正确性的验证.
关键词: 形式化验证; 操作系统内核; 分离逻辑; Rust; 定理证明
中图法分类号: TP311

中文引用格式: 何韬, 董威, 文艳军. GhostFunc: 一种针对Rust操作系统内核的验证方法. 软件学报, 2025, 36(8): 3494–3511. http://
www.jos.org.cn/1000-9825/7347.htm
英文引用格式: He T, Dong W, Wen YJ. GhostFunc: Verification Method for Rust Operating System Kernel. Ruan Jian Xue
Bao/Journal of Software, 2025, 36(8): 3494–3511 (in Chinese). http://www.jos.org.cn/1000-9825/7347.htm

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

操作系统是计算系统的基础平台, 操作系统安全性是现代操作系统中至关重要的一个方面. 它不仅保护用户
数据免受未经授权的访问和恶意软件的威胁, 还确保系统的稳定性和可靠性. 此外, 安全的操作系统还能减少系统
崩溃和性能问题, 提高整体生产效率和用户信任度. 因此, 操作系统的安全性是维持数字生态系统健康和安全的

* 基金项目: 国家自然科学基金 (U2341212)
本文由“形式化方法与应用”专题特约编辑陈明帅研究员、田聪教授、熊英飞副教授推荐.
收稿时间: 2024-08-25; 修改时间: 2024-10-14; 采用时间: 2024-11-26; jos 在线出版时间: 2024-12-10
CNKI 网络首发时间: 2025-03-27