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

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

变化, 从最初的词法生命周期 (lexical lifetime) 到非词法生命周期 (non-lexical lifetime, NLL), 再到最新的 Polonius
借用检查器, 使得形式化语义工作也随着 Rust 语言的发展而不断变化. 但目前缺乏对不同语义研究工作的系统性
对比分析. 此外, 现有的 Rust 验证工具多由不同团队独自开发, 缺少统一框架来比较它们的功能、支持的语言特
性和适用场景. 这影响了这些工具在实际开发流程中的集成和应用, 也限制了它们在技术创新上的相互促进. 因
此, 本文的工作旨在填补这一空白. 我们将首先从理论上系统性分析 Rust 语言特性, 然后从 Rust 语义研究的角度
探讨形式化验证如何增强 Rust 的安全性, 接着分类讨论了 Rust 程序的自动化验证方法及工具, 最后总结了当前
Rust 形式化验证工作存在的挑战和局限性, 并提出未来可能的改进方向. 本文的工作对于指导工具选择、促进技
术交流与创新, 以及推动形式化验证技术的发展具有重要意义. 特别说明的是, 本文系统性分析 Rust 语言的基于
所有权和借用检查的强大类型系统, 为形式化验证提供了新的视角. Rust 类型系统扩展了编程语言理论中线性类
型、仿射类型的概念, 形式化领域可以通过证明类型系统可靠性的方式来证明 Rust 类型安全和借用安全. Rust 在
语言层面上对指针别名实行了严格的规范, 内置了类似分离逻辑的思想. 多种 Rust 验证工具已经巧妙地利用其类
型系统提供的安全保证来简化程序证明的过程. 通过本文的工作, 我们希望为 Rust 社区提供一个更加坚实的安全
基础, 并为未来的研究指明方向, 推动形式化验证方法在 Rust 开发中的更广泛应用.
本文的核心议题聚焦于 Rust 语言的形式化验证技术. 该技术依赖于严格的数学逻辑和形式系统, 基于形式语
义和形式规约来描述系统的行为和属性, 将系统的分析和验证问题转化为逻辑推理问题或形式模型的判定问题,
并利用定理证明器、模型检查器等形式化工具来进行严格的证明, 确保系统的行为与预期一致. 相比之下, 尽管污
点分析、数据流分析、动态分析等常用程序分析方法在 Rust 的漏洞检测研究中占有重要地位, 但这些方法不强
制执行严格的形式验证, 可能存在误报或漏报问题. 因此, 这些程序分析技术超出了本文的讨论范围.
本文在第 2 节系统性分析 Rust 语言的特性, 包括以所有权和借用检查机制为核心的特性以及一些复杂特性,
并阐述 Rust 编译的过程. 第 3 节深入探讨针对 Rust 形式语义的研究与验证工作, 包括基于类型系统的语义研究
以及基于纯操作语义的语义研究. 第 4 节全面对比分析各类 Rust 自动化验证工具, 这些工具采用了多种验证方法,
包括半自动化程序验证方法、定理证明方法和模型检测方法. 第 5 节对已验证的 Rust 系统进行总结, 展示形式化
验证在确保 Rust 程序正确性方面的实际应用及效果, 并综合分析验证案例和实际使用经验, 提出工具选择建议供
用户参考. 第 6 节分析当前领域面临的多维度挑战, 这不仅需要验证人员的努力, 还需要与 Rust 社区和开发者的
共同协作. 第 7 节探讨值得进一步探索研究的发展方向, 包括对 unsafe Rust 代码的验证, 对并发代码的验证, Rust
可信编译以及大模型驱动的 Rust 形式化验证等.

2 Rust 语言特性概述

2.1 Rust 核心特性

2.1.1 所有权机制
所有权是 Rust 语言为安全高效使用内存而设计的语法机制. 大多数的编程语言都有管理内存的功能, C/C++
主要通过手动方式管理内存, 开发者需要手动的申请和释放内存资源, 但许多开发者没有及时释放内存的习惯, 所
以手动管理内存的方式常常造成资源浪费. 传统的自动内存管理语言通过垃圾回收机制管理内存对象的生命周
期, 典型代表有 Java、Python、Go 等. Java 语言编写的程序在虚拟机 (JVM) 中运行, JVM 具备自动回收内存资源
的功能. 但垃圾回收期间通常会造成程序短暂停顿而降低运行时效率, 所以实际使用中一般会通过 JVM 参数减小
垃圾回收的频率, 这样也会使程序占用较大的内存资源. 而 Rust 最具标志性的所有权模型通过编译时检查实现了
自动内存管理, 从而避免了运行时的内存管理开销和潜在的内存安全问题. 所有权模型的设计其根本而言是为了
管理堆上的数据, 所有权机制能跟踪代码的哪些部分正在使用堆上的哪些数据, 清理堆上未使用的数据以避免空
间不足.
Rust 的所有权模型有以下 3 条规则: (1) Rust 中的每一个值都有一个所有者 (owner); (2) 值在任一时刻有且只
有一个所有者; (3) 当所有者 (变量) 离开作用域 (scope), 这个值将被丢弃. 变量范围是变量的一个属性, 其代表变