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

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

来确保其安全性和正确性, 而不是依赖类型系统的可靠性证明. 例如, 可以证明在程序的任何执行时刻, 对特定内
存位置的有效可变访问不会与任何其他形式的访问冲突. 这种证明过程需要对操作语义进行深入分析, 并严格检
查程序状态的变化, 以确保所有安全性条件得到满足.
Wang 等人 [25] 基于 K 框架 (K-framework) 提出 Rust 子集的形式化可执行操作语义. K 是一个专门用于描述编
程语言语义的形式框架, 该研究在 K 中定义了第一个针对 Rust 的形式化可执行语义 KRust, 并借助 K 框架基于
KRust 定义的语义规则自动生成了 Rust 程序的解释器和验证工具. KRust 包括了 Rust 中所有的基本类型、基本
运算、复合数据类型、基本的控制流、函数等语法特征. 语义规则涵盖 Rust 的 3 个重要特性, 即所有权、借用和
生命周期. 实验中使用 Rust 官方编译器提供的测试集, 将该解释器执行 Rust 程序的结果和 Rust 编译器的结果进
行一致性对比测试, 发现了一个 Rust 编译器中的错误. 然而, 虽然 KRust 中有所有权、借用和生命周期的基本概
念, 但语义定义不够全面. 例如, 没有描述重借用的过程, 没有描述 unsafe 机制等. 此外, 由于 KRust 也是较早期的
工作, 也采用传统的词法生命周期推断.
Kan 等人 [26] 同样基于 K 框架提出了 Rust 可执行操作语义. 相比于 KRust, RustSEM 涵盖了 Rust 主要语言特
性的更大子集, 包括 unsafe 原始指针, 并发等特性, 并描述非词法生命周期. RustSEM 语义的核心是具有 OBS (所
有权和借用系统) 操作语义的内存模型. 该文章强调, 基于类型系统的验证工作将 OBS 形式化为语言层面
(language-level) 的类型约束, 只能用于在编译时保守地分析程序是否符合 OBS 不变量, 可能会拒绝动态执行时实
际正确的程序. 相比之下, RustSEM 在内存层面 (memory-level) 为 OBS 提供了操作语义, 能够在动态执行 Rust 程
序时自动化验证程序的运行时行为. RustSEM 中定义了多个 OBS 不变式, 例如, 生命周期包含不变式即, “如果 X
是 Y 的 (可变/不可变) 引用, 则 X 的生命周期应该始终在 Y 的生命周期之内, 以避免悬挂指针”, 并在程序做内存
访问操作的时候检查这些 OBS 不变式是否都被满足. RustSEM 提供动态检查器, 检测 Rust 程序的内存安全, 如所
有权和借用错误, 缓冲区溢出等问题. 此外, 该研究利用 K 框架自动生成了 RustSEM 验证器, 能基于 RustSEM 的
操作语义对 Rust 程序做符号执行推理, 如基于霍尔逻辑验证 unsafe 代码是否会导致未定义行为. 实验评估了
RustSEM 相对于 Rust 编译器的语义正确性, 并表明 RustSEM 能够检测出更多内存错误, 拒绝编译器允许通过的
错误程序. 然而, RustSEM 的内存模型较为抽象, 没有精准描述 Rust 的内存模型. 例如, 其内存模型没有反映值的
字节级表示, 并且不支持无界堆片段. 此外, RustSEM 主要检测内存相关的错误, 不能验证较复杂的功能正确性.
类型系统的价值不仅体现在它们为程序提供的安全性保障上, 更在于它们通过简化关键的程序分析过程, 助
力编译器生成效率更高的代码. 在 Rust 语言中, 类型系统对指针别名实行了严格的规范, 而 Rust 编译器团队的一
个核心目标就是利用这些别名信息来实施程序优化, 以重新排序内存访问操作. 然而, Rust 对 unsafe 代码的支持
带来了挑战, 因为程序员可以通过 unsafe 代码绕过编译器的常规检查, 从而违背别名规则. 为了在优化需求与
unsafe 代码的使用之间找到平衡点, 语言的设计必须提供一套清晰的规则. 这些规则要能够让编写 unsafe 代码的
开发者确信, 只要他们遵守规则, 即使在编译器执行各种优化的情况下, 他们的代码语义也能得到保留. Jung 等
人 [24] 提出了 Stacked Borrows 操作语义框架, 定义了 Rust 引用类型内存访问的别名规则, 并规定违反这些规则的
程序将具有未定义行为. 这样的设计意味着编译器在执行优化时, 可以忽略那些违反规则的程序. 该工作旨在利用
这些类型中编码的别名信息以实现过程内优化, 即允许编译器仅凭过程内推理, 就对未知代码和函数调用周围的
内存访问进行重新排序优化, 这些优化的有效性已通过 Coq 形式化验证. 该模型的创新之处在于, 它实现了 Rust
原有静态借用检查器的动态版本, 并将原有针对安全 Rust 代码段的借用检查逻辑扩展到整个语言, 即能够将分析
范围扩展至 unsafe 代码, 特别是那些操作原始指针的代码. 值得一提的是, 该工作没有像 Rust 静态借用检查器中
那样显式描述生命周期, 理由是编译器对生命周期的推理规则在不断演进, 从基于 AST 的结构式借用检查演变到
非结构式生命周期 (NLL) 再到 Polonius 项目, 而这不该影响对程序是否是有良好行为的 (well-behaved) 判断. 该
工作在不提及生命周期的情况下重新表述这一特性为, “引用的每次使用以及由其派生的所有内容都必须发生在
被引用对象 (referent) 的下一次使用之前”, 并将其定义为“栈原则 (stack principle)”. 该研究将此模型实现在 Miri
解释器中, 并通过该解释器运行了 Rust 标准库的大部分测试套件, 以验证模型能够兼容并支持现实世界中广泛存
在的 unsafe Rust 代码. Miri 的评估工作中 Stacked Borrows 发现的违规问题基本都是被 Rust 社区作为 bug 并后期