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

3496 软件学报 2025 年第 36 卷第 8 期

操作系统. 在该项目中, 研究人员使用了 Spec#和 Boogie 等验证工具对操作系统的关键组件进行了形式化验证, 确
保了组件之间的接口契约. 这种契约式的验证方法提高了系统的可靠性, 并显著减少了运行时错误的发生.
下面介绍 Rust 程序的形式化验证方面已有的一部分工作.
Cui 等人 [10] 通过静态数据流分析检测 Rust 程序中的内存释放错误, 提高了内存安全性. Dai 等人 [11] 通过 Coq
定理证明器证明了 Rust 实现的页表在 Software Enclave Hypervisor 中的正确性. CRust 采用有界模型检测的技术
针对 Rust 中的不安全代码的内存安全性质进行验证 [12] . 主要的技术原理是使用工具将 Rust 程序翻译为 C 语言实
现的程序, 然后在 CBMC 工具 [13] 中进行验证. Prusti [14,15] 证明工具与 CRust 工具类似, 不同的是先使用 MIR 提供的
语言类型通过分离逻辑方式合成程序证明, 然后将 Rust 语言转换为一种中间语言 Silver, 并使用验证框架 Viper
中的符号执行工具进行验证. 该工作的不足之处是不支持闭包, 生命周期等特性的验证. RustBelt 是由来自 MPI-
SWS 的 Ralf Jung 主导的一个研究项目 [16−18] , 旨在对 Rust 语言的核心安全性进行形式化验证. RustBelt 使用了交
互式定理证明器 Coq, 通过 Iris 并发分离逻辑框架对 Rust 的类型系统和借用检查器进行了详细建模和验证. 通过
这项工作, 研究人员证明了 Rust 的核心语言特性, 如所有权和借用, 能够确保内存安全性和数据竞争的防止. 本文
对于 unsafe 代码的语义模型的建立参考了该项工作.
当前关于操作系统内核的基于定理证明器的验证中针对 C/C++构建的传统架构内核居多, 对于使用 Rust 构
建的新型架构内核验证的相关工作相对空白, 而针对 Rust 程序的验证, 特别是基于定理证明的形式化验证工作非
常少, RustBelt 项目虽然对 Rust 底层的安全机制进行了探索与验证, 但并没有应用到实际 Rust 构建的系统中.

2 基础知识

本文在交互式定理证明器 Coq 中利用 Iris 验证框架对某使用 Rust 构建的新型架构内核中任务管理和调度模
块的正确性进行验证. 下面对基本知识进行简要介绍.

2.1 定理证明器 Coq
Coq 是一个高级的交互式定理证明器 [19] , 它允许用户编写形式化证明, 这些证明可以由计算机检查以确保
它们的正确性. Coq 使用了一种名为“构造演算”的形式语言, 这是一个包含高阶逻辑的强类型函数式编程语言.
它广泛用于研究领域, 特别是在软件和硬件验证、形式化数学以及其他需要高可信度的场景中. Coq 的类型系
统支持 dependent types, 这意味着类型可以依赖于值. 这种能力极大地增强了语言的表达能力, 允许用户表达丰
富的逻辑和数据结构. Coq 基于构造主义逻辑, 这意味着它不接受经典逻辑中的排中律 (每个命题都是真或假
的) 和选择公理. 在 Coq 中, 证明某事存在相当于提供一个构造该事物的方法. Coq 包含一个证明助手, 帮助用户
通过一步一步的 tactics 来构建证明. 每个策略可以修改当前的证明状态或引入新的假设. Coq 支持模块化编程,
允许用户编写可重用的库和模块, 这些库和模块可以被不同的项目共享和使用. Coq 被用来验证软件程序的正
确性, 包括操作系统内核、编译器和其他关键系统. 例如, CompCert C 编译器 [20] 就是一个被证明为语义保持的
编译器, 采用 Coq 进行正确性验证. Coq 也被用于形式化数学证明, 包括著名的四色定理 [21] 和费马大定理 [22] 的
部分证明.

2.2 并发分离逻辑证明框架 Iris
Iris [23−25] 是用于构建高级并发程序验证的框架, 它在 Coq 定理证明器上实现. Iris 使用高阶分离逻辑, 提供强大
的抽象和模块化机制, 这使得它非常适合用来验证复杂的并发系统和软件. Iris 基于高阶分离逻辑, 能够处理可变
状态, 允许逻辑公式中包含资源的概念. 分离逻辑特别适合于并发和并行计算的情境, 因为它可以清晰地描述和推
理那些由多个线程或进程共享和修改的资源. Iris 的计支持高度模块化, 使得用户可以构建可复用的验证组件. 这
对于处理大规模软件系统特别重要, 因为它减少了验证工作的重复性, 并提高了代码的可维护性. Iris 能够处理动
态分配的资源, 用户可以在逻辑中动态地创建和销毁资源, 这对于处理复杂的动态行为至关重要. IPM (Iris proof
mode) 提供了一组定制的策略 (tactics), 这些策略专门针对 Iris 逻辑的特点进行了优化. 例如, 这里给出一个简单的
并发加法器在 IPM 中的证明过程. 首先定义加 1 和不变式以及需要证明的引理.