软件学报

作者：何韬，董威，文艳军

单位：何韬，国防科技大学 计算机学院, 湖南 长沙 41007311,董威，国防科技大学 计算机学院, 湖南 长沙 41007302,文艳军，国防科技大学 计算机学院, 湖南 长沙 41007303

关键词：形式化验证;操作系统内核;分离逻辑;Rust;定理证明

基金：国家自然科学基金(U2341212)

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

来源：2025年第8期

《软件学报》期刊编辑部

查看软件学报杂志2025年第8期