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

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

this study summarizes exemplary cases of verified Rust programs, demonstrating the significant impact of formal verification in ensuring
program correctness and providing practical tool usage recommendations for developers. Finally, it discusses the key challenges in the field
and outlines promising directions for future research, including the verification of unsafe Rust code, concurrent code verification,
trustworthy compilation, and large model-driven formal verification. This study aims to establish a strong security foundation for the Rust
community and foster the broader adoption of formal verification methods in Rust development.
Key words: formal method; Rust language; program verification; formal semantics; memory safety

1 引 言

Rust 语言作为新一代安全高性能系统级编程语言, 旨在解决 C/C++等传统底层编程语言在内存安全和并发性
方面的挑战. 它通过引入所有权模型, 实现了一种静态的自动内存管理机制, 同时结合函数式编程范式与强多态类
型系统等先进语言特性, 不仅确保了内存和并发安全, 同时也达到了高效的执行性能, 满足了构建底层基础软件的
需求. Rust 通过编译时的检查自动管理内存安全, 有效预防了空指针解引用、悬挂指针和内存泄漏等常见问题.
在 Rust 中, 每个值都拥有一个明确的唯一所有者, 当该所有者超出作用域时, 值会被自动清理. 此外, 借用规则保
证了在任何给定时间, 要么只有一个可变引用存在, 要么可以有多个不可变引用, 但两者不会同时存在. 上述的设
计哲学避免了数据竞争, 为并发编程提供了天然保障. 与 C/C++的手动内存管理相比, Rust 的所有权系统实现了自
动化的内存管理, 同时避免了 Java 垃圾回收机制可能带来的性能开销, 实现了接近系统级语言的性能表现. 因此,
Rust 已被广泛应用于基础软件的构建, 包括操作系统内核 [1] 、文件系统 [2] 、云服务 [3] 、数据库 [4] 、Web 浏览器 [5] 、
网络协议栈 [6] 以及区块链技术 [7] 等多个领域, 证明了其在现代系统级编程中的实用性和可靠性.
然而, Rust 并不是绝对安全的. Rust 允许开发者通过 unsafe 代码块来执行解引用裸指针等底层操作以及跨语
言调用等. Unsafe 代码的使用引入了潜在的风险, 它意味着绕过了 Rust 编译器强制性的内存安全检查, 将这部分
代码的正确性交由开发者自行保证. 在复杂的系统编程任务中, 人为错误几乎不可避免, 很可能导致安全漏洞的产
生. Xu 等人 [8] 收集了 186 个 Rust 相关的 CVE, 总结出 Rust 中 3 类典型内存安全问题, 指出都与 unsafe 特性的使
用有关. Mergendahl 等人 [9] 揭示了 Rust 通过 unsafe FFI 与 C 代码的交互会引入新的攻击变体. 此外, 尽管 Rust 的
安全性得到了社区和学术界的广泛认可, 但一些研究也揭示了即使是在 Rust 中也存在安全漏洞. 例如, 根据
system-pclub [10] 的研究, Rust 库中仍然发现了一些内存安全和线程安全缺陷. 这些缺陷的存在表明, 尽管 Rust 的安
全机制显著降低了编程错误的发生概率, 但并不能完全消除所有错误. 为应对这些安全问题, Rust 提供了运行时检
测工具, 能够检测缓冲区溢出、除零等问题. 此外, Rust 在其调试构建模式中提供了更多的漏洞检测功能, 包括对
双锁 (double lock) 和整数溢出的检测. 然而, 这些动态检测机制只能捕获有限范围的问题. 虽然 Rust 使用 LLVM
作为其后端, 许多为 C/C++设计的静态和动态漏洞检测技术也可应用于 Rust, 但 Rust 的新语言特性和库可能会引
发新类型的漏洞. 近年来, 针对 Rust 的静态分析器得到了发展, 但这些工具在实际应用中存在较高的误报率 [11] . 例
如, SafeDrop [12] 在分析大规模程序时的误报率可能高达 94%–97%.
因此, 在 Rust 语言的安全性增强方面, 基于形式化验证的研究工作已有显著成效. 形式化验证方法可基于数
理逻辑基础对程序和系统进行精确建模和严格证明, 从而保证 Rust 程序的正确性和安全性. 一方面是针对 Rust
形式化语义的研究工作, 构建精准清晰的语义模型, 基于该语义模型可以证明遵循 Rust 所有权、借用检查和生
命周期规则的程序确实满足内存安全性和线程安全性. 例如, RustBelt [13] 项目利用其语义模型和证明, 在 Rust 编
译器和标准库的实现中发现并修复了安全问题. 另一方面是 Rust 程序的自动化验证工作, 借助 Rust 自动化验证
工具能够自动构建证明和检查过程, 帮助用户确保其 Rust 实现的程序是安全且正确的. 例如, AWS 通过采用轻
量级形式化验证方法, 对其 Amazon S3 云对象存储服务中 Rust 实现的键值存储节点进行了功能正确性验证 [14] ,
成功拦截 16 个潜在问题, 防止其进入生产环境. 此外, 形式化验证方法在增强 unsafe Rust 代码的安全性上也有显
著成果 [13,15,16] .
虽然已有研究在特定领域有一定进展, 但目前尚缺乏从系统性的角度对 Rust 形式化验证工作的全面分析.
Rust 作为一种持续演进的新兴编程语言, 其多种语言特性都在不断完善. 比如借用规则这一核心机制近年来的发展