Page 195 - 《软件学报》2025年第8期
P. 195
3618 软件学报 2025 年第 36 卷第 8 期
修复的, 表明其有效性. 该研究未来计划将 Stacked Borrows 与 RustBelt 中的 Rust 形式化类型系统相结合, 以验证
所有安全的 Rust 程序是否都遵循 Stacked Borrows 规则. Stacked Borrows 模型的长期发展目标是成为 Rust 官方语
义的一部分, 这需要与 Rust 社区和开发团队保持紧密合作, 根据实际需求不断调整模型. 这不仅将增强 Rust 语言
的安全性和可靠性, 也将为编译器优化提供坚实的理论基础.
4 面向 Rust 程序的自动化验证工作
自动化程序验证研究的主要目标是基于程序验证相关理论 (如霍尔逻辑, 分离逻辑等), 利用自动化验证工具
实现自动推理, 证明程序的部分或完全正确性, 即程序在运行时满足特定规范. 自动化验证工具能够自动构建证明
和检查过程, 不会暴露底层复杂的形式逻辑, 允许用户在编程语言的抽象级别上工作. 现有的 Rust 自动化验证工
具依据它们所依赖的验证技术, 分为半自动化程序验证方法、模型检测方法和定理证明方法. 每种方法有各自的
优势及适用的应用场景. 总结来说, 半自动化验证器以模块化的方式高效验证程序功能准确性等复杂性质. 这些验
证器利用 Rust 类型系统提供的安全保证来简化推理过程. 然而, 它们在同时支持 unsafe 代码方面面临挑战. 定理
证明器采用浅嵌入技术, 在其他语言中以纯函数式代码的形式规范描述 Rust 的一个子集, 并利用该语言的后端工
具链进行后续证明. 该方面避免了显式描述程序内存布局, 但目前仅限于验证 Rust 安全代码, 且在语言转换过程
中缺乏正确性保证. 模型检查器通过将 Rust 程序转换为类似 C 的表示形式, 并借助已有 C 内存模型支持验证低
级内存模型的 unsafe 代码和并发代码. 但这种方法缺乏灵活性, 仅限于验证基本属性, 且不能精确描述 Rust 生命
周期等自身语言特性. 表 2 中更细粒度地列举了不同 Rust 自动化程序验证工具的特点. 值得注意的是, 虽然一些
专注于 Rust 语义的研究也开发了相应的自动化程序分析工具, 但这些工具的主要目的并不在于自动程序验证, 本
文已将这些工作列入了第 3 节, 在此不再赘述. 在介绍这些工具前, 本节先主要围绕分离逻辑介绍一些基础概念.
Rust 语言独特的类型系统和所有权规则提供了类似分离逻辑的表达能力, 为程序验证提供了新的解决方案. 理解
这些概念对于掌握 Rust 的自动化验证工具至关重要, 同时也为如何有效利用这些工具提供了理论基础.
表 2 Rust 自动化程序验证研究工作总结对比
支持语言特性
验证技术 研究工作 中间语言 数据结构 验证性质 借用
Closure Unsafe 并发 Trait
(1) (2) (3) (4)
[33]
Prusti Viper MIR 功能正确性 ● ○ ○ ● ● ● － ○
[34]
Verus 无 HIR 功能正确性 ● ◐ ◐ ● ● ○ － －
[35]
Creusot WhyML MIR 功能正确性 ● ○ ○ ● ● ● ● －
半自动化
RustHorn [36] CHC MIR 功能正确性 ○ ○ ○ ○ ● ● － －
[37]
VeriFast C AST MIR 类型安全 ○ ● ○ ○ ● － － －
[16]
Gillian-Rust GIL － 功能正确性, 类型安全 ○ ● ○ ● ◐ ◐ － －
Crust [38] C-like AST 内存安全 ○ ● ○ ○ ● － － －
SMACK [39] Boogie LLVM IR 内存安全, 功能正确性 ● ● ○ ● ● － － －
模型检测 Kani [40] C-like MIR 内存安全, 功能正确性 ● ● ○ ● ● ● － －
Loom [41] C AST 并发安全 － ○ ● ○ ● － － －
TrustPN [42] Petri-Net MIR 并发安全 － ○ ● ○ ● － － －
[43]
Electrolysis Lean MIR 功能正确性 ● ○ ○ ● ◐ ○ ○ ○
定理证明
Aeneas [44] LLBC MIR 功能正确性 ○ ○ ○ ○ ● ● ◐ ●
注: ●: 支持; ○: 不支持; ◐: 部分支持, 例如Gillian-Rust只支持可变引用而不支持不可变引用. －: 没有显式说明. 各类借用形式:
(1) 常见的借用, (2) 返回借用(return borrows), (3) 嵌套借用 (nested borrows), (4) 两阶段借用 (two-phase borrows)
4.1 分离逻辑与 Rust 所有权系统
分离逻辑 (separation logic) [45] 是对霍尔逻辑 (Hoare logic) 的一种扩展. Hoare 逻辑 [46] 是一套基于公理语义的程
