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

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

Baranowski 等人 [39] 扩展了 SMACK 工具对 Rust 的支持. SMACK 以 LLVM IR 程序为输入, 并将该程序依次
转为 Boogie 代码、SMT 输入的验证条件, 最终调用 SMT 求解器进行求解, 具有较好的通用性. 该工作扩展了
SMACK 对 rustc 生成的一些 Rust 特有 LLVM IR 代码的支持, 并借助已有工具链实现 Rust 程序的验证. 由于
SMACK 可以复用其 C 模型, 因此支持 Rust 对 C 的跨语言调用. 实验表明 SMACK 能够处理一些 Rust 关键语言
特性, 如 trait, closure, 并支持内存安全验证, 例如 unsafe Rust 中 C 分配的数组不会导致缓冲区溢出 (buffer
overflow) 或内存泄漏 (memory leak).
Loom [41] 是常用的并发验证器. Loom 会根据 C11 内存模型规定的有效的执行方式, 对输入程序可能的并发执
行进行排列组合, 探索各种可能执行排列的方法并检查是否出现并发错误. Loom 使用状态简化 (state-reduction)
技术来避免组合爆炸的情况. 然而, Loom 这样可靠的状态无关模型检查工具 (sound stateless model checker) 在可
扩展性方面还不够, 即使是相对较小的测试也涉及数万个原子步骤的交织执行 (interleaved execution) [14] .
同样针对并发问题, Zhang 等人 [42] 提出了并行 Rust 程序检测工具 TRustPN. 它通过一系列转换规则自动将
MIR 形式的程序转换为 Petri 网模型, 然后分析由双重锁定 (double lock) 和读写冲突 (read-write conflict) 等引起的
死锁问题. TRustPN 在转换输入程序时主要提取 MIR 中与死锁问题相关的锁定 (lock)、解锁 (unlock)、生成
(spawn) 和加入 (join) 等语句, 可以省略无关的 Rust 代码, 从而扩大处理代码的规模.

5 基于自动化工具的 Rust 程序验证成果及使用建议
Rust 语言以其在系统级安全编程领域的卓越性能和可靠性, 正逐渐成为重写和开发软件系统的首选 [55–57] . 谷
歌的报告指出, 自从 Android 系统引入 Rust 进行关键部分的重写, 内存安全问题得到了极大的缓解, 其比例由
76% 大幅下降至 25% [58] , 表明 Rust 语言的内存安全特性为软件系统提供了一种内在的安全保障. 本文进一步提
出, 通过结合 Rust 编程和形式化验证的方法, 能够为软件系统的安全性和可靠性提供双重保障, 为软件系统开发
带来新的机遇. 一方面, 相较传统非安全编程语言, Rust 所有权模型和借用检查机制提供的安全保障简化了程序验
证的推理过程, 另一方面, 通过融合严谨的形式化验证方法, 不仅能够证明软件系统的功能正确性等复杂特性, 还
能够为与不安全 Rust 代码的交互过程提供严格的限制. 本节将列举近年来针对 Rust 软件系统形式化验证的实例,
展示其在实际开发中的应用情况和带来的益处. 一些工程实践中 Rust 验证的应用实例由于缺乏公开的学术论文
和开源代码, 难以全面掌握这些工作的细节, 因此本文不对其进行详细讨论. 本节最后将综合分析验证案例, 并结
合作者对验证工具的实际使用经验, 提出工具选择建议供用户参考. 随着 Rust 语言和相关验证工具链的不断成熟,
在未来应该可以看到更多类似的工作.

5.1 针对 Rust 系统的自动化验证
RedLeaf [59] 是基于 Rust 编程语言隔离的微内核架构操作系统, 首次提出利用 Rust 的性质对 Rust 操作系统进
行高效的形式化验证. RedLeaf 开发基于 SMACK 校验器、Boogie 中间验证语言和 Z3 SMT 求解器的验证工具链,
提供 Floyd-Hoare 风格的模块化验证, 要求开发人员以前置条件、后置条件和循环不变式的形式手动为程序标注
过程合约. 基于 Rust 所有权系统, 框架规则可以根据函数签名自动推导, 可变引用不会互相别名, 验证工具链可利
用这些信息减少用户需要标注的堆不变式, 并通过将程序堆建模从传统的字节数组替换为一组有类型的变量, 以
提高验证效率和可扩展性. 该研究作为先导性工作提出通过 Rust 的所有权系统减轻传统验证器的负担, 但是并没
有给出验证需要的工作量.
Brun 等人 [60] 指出, 尽管现在有不少经过验证的操作系统, 但这些系统的规约并不能与应用程序的验证结合起
来, 给出一个端到端验证的高性能软件栈. 他们根据在操作系统上运行的应用程序的行为定义操作系统的高级规
约, 并将其分为两类: 操作系统提供的执行模型 (反映内存和 CPU 的虚拟化); 支持的系统调用 (网络、文件系统以
及并发原语). 然后基于 Verus 对一个 Rust 开源操作系统 NrOS [61] 的页表管理模块进行了功能正确性验证. 他们设
计了描述硬件环境的硬件规约和描述映射、解映射和地址解析行为的高级规约, 然后证明, 在预定硬件环境中运
行, 页表实现可以精化高级规约.