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

张卓若 等: 面向 Rust 语言的形式化验证方法研究综述 3629

的双射映射性质, 该工作主要基于 Rust 类型状态特性实现资源访问控制, 并描述成编译期间检查的不变式, 而仅
对不能使用该方法描述的部分进行了半自动化验证. 在 SquirrelFS 中 [64] , 同样利用了 Rust 语言的类型状态特性实
现编译时检查. 此外, 该工作使用 Alloy 建模语言对 SquirrelFS 文件系统在设计层建模, 并确保 Rust 类型状态模型
与 Alloy 模型在设计上的一致性, 同时在 Alloy 中运用模型检查的方法验证了高层性质. 蚂蚁集团近期公布的“星
绽”操作系统中 [74] , 除了使用形式化验证外, 还通过模糊测试对安全的 Rust 代码部分进行测试, 以有效发现未处理
的 panic.
(2) 综合使用多种形式化工具: 鉴于 Rust 语言的验证工具尚处于发展初期, 支持的功能特性有限, 一些 Rust 程
序验证案例中会对现有工具进行扩展以满足特定的验证需求. 例如, 在 Kubernetes 管理控制器的验证中 [75] , 通过
扩展 Verus 并结合 TLA+来支持活性 (liveness) 验证, 这要求用户对该工具有深入了解. 相对地, 有些研究可能会采
用不同的工具来验证程序的不同属性. 例如“星绽”操作系统中, 利用 Verus 对内存管理系统进行建模和验证, 证明
了代码正确实现了内存映射和页面管理等功能. 同时, 该工作没有扩展 Verus, 而是直接使用 TLA+验证了星绽中
的并发原语, 确保了并发的安全性 (safety) 和活性 (liveness). 亚马逊在验证 S3 云对象存储服务并发执行情况时,
利用 Loom 可靠地检查小型但关键的并发代码的所有可能交错情况, 例如自定义的并发原语; 利用 Shuttle 随机检
查那些 Loom 无法扩展到的大型测试场景中的交错情况.
(3) 单一形式化工具的选择建议: 从文档维护、社区活跃度、工具易用性及特性支持度等方面考虑, 作者建议
用户优先选择 Verus、Kani 和 Prusti. 相比之下, 一些形式化工具尚未开源 (如 Gillian-Rust, TRustPN), 或仍处于科
研探索阶段而支持的功能特性不足 (如 VeriFast), 或没有后期的维护和扩展 (如 Electrolysis, Crust, SMACK), 或没
有稳定版本和清晰的指导手册 (如 Creusot). 这些研究工作虽然在 Rust 形式化验证领域提供了很好的借鉴和启发
意义, 但不适合直接用于实际工程项目的验证. Verus、Prusti 和 Kani 这 3 个工具在近年来均有实际的验证案例,
且文档维护和使用体验方面表现较好. 其中, Prusti 仅支持 safe Rust 的验证, 且在验证速度上较慢, 但在 safe Rust
特性的支持上有自己的优势 (如 Verus 不支持如图 12 函数返回可变引用的情况). Kani 和 Verus 均支持 unsafe
Rust 程序的验证, 但前者支持范围更小 (如图 6 的例子, Verus 不支持验证变量直接取地址的情况, 而 Kani 则可验
证并发现指针访问越界的问题) 且可能需要修改源代码以使用自己的库 (如抽象原始指针 API), 而 Kani 则受到循
环展开次数约束等限制, 且仅支持插桩简单的验证条件, 不能像半自动化工具一样提供灵活的模块化功能正确性
验证 (如图 19 的对比). 如后文第 7 节所述, 并发程序的验证是有挑战性的工作, Loom 和 Verus 提供了一定程度的
支持.

6 Rust 形式化验证的技术挑战

现有的 Rust 验证工作已取得一些进展和研究成果, 但仍然面临以下技术挑战.
(1) 目前, Rust 语言尚未完全标准化, Rust 社区尚未形成一份统一精准的规范文档. 这意味着, 对于 Rust 应该
实现哪些功能以及 Rust 编译器应展现怎样的行为, 目前还没有一个明确的定义. 这与 C 和 C++等已经过标准化过
程的编程语言形成对比. C 语言的发展历程中, 从最初的 ANSI C (即 C89) 到后续的 ISO C (C90)、C95、C99、
C11 乃至 C17, 每一个版本都伴随着国际认可的标准文档, 确保了不同编译器和平台上编程体验的一致性. Rust 的
这种状况对 Rust 的形式化验证领域产生了显著的影响.
首先, 缺乏一个统一的规范文档使得无法对 Rust 的操作语义和内存模型进行完全精确的形式化描述. 当前一
些验证工作的做法是将 Rust 编译为 C 类似的表示, 直接使用 C 原有的内存模型以绕过该问题然而, Rust 有一些
C 没有的新特性, 例如非常规模数类型 (exotically-sized types) 如零大小类型 (zero-sized types) 以及多态性等. 再加
上后文展开的 Rust 编译器利基优化技术, 这些特性使得直接应用 C 语言验证工具中现有内存模型变得复杂且具
有挑战性. 一些工作通过转化 Rust 为纯函数式的表示, 避免显式描述内存模型, 但该方法目前仅限于 safe Rust 子
集. 还有一些工作, 如 RustBelt, 引入 Rust 模型语言 (而非真实的 Rust 语言) 并描述其操作语义, 同时使用简化的内
存模型表示. 这种方法在理论上提供了对 Rust 语言核心概念的理解, 但不能直接用于处理真实 Rust 程序.