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

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

证 Rust 程序时, 用户在 Rust 程序中注释 VeriFast 支持的分离逻辑公式信息以描述前置条件和后置条件, 提供引理
或幽灵指令 (ghost command) 辅助验证. 目前的 VeriFastRust 前端有一些限制, 除了自动化程度有限需要用户辅助
证明过程外, 它不支持多态等特性, 并且只专注于验证语义类型安全性而非功能正确性.
同样针对 unsafe 代码, Ayoun 等人 [16] 提出了一种混合方法, 将 Rust 程序的安全和不安全部分交由两个不同的
工具进行类型安全性和功能正确性验证. 其中, 安全部分由 Creusot 处理, 不安全部分由该研究提出的 Gillian-Rust
处理. Gillian-Rust 是基于 Gillian [50] 参数化组合 (parametric compositional) 的符号执行平台, 嵌入了 RustBelt 的生命
周期逻辑和 RustHornBelt 的参数预言, 并能够自动推导分离逻辑断言, 是首个验证 unsafe Rust 代码功能正确性的工
作. 此外, 相比 VeriFast, Gillian-Rust 提供用户友好的 API, 自动化程度更高. 为了描述 unsafe 代码的可能行为, Gillian-
Rust 扩展了 Gillian 的符号内存模型为布局无关的 Rust 内存模型, 并支持做指针运算和位级 (bit-level) 操作. 在验证
程序时, 用户注释 Creusot 规约语言 Pearlite 描述的规约, Gillian-Rust 自动将 unsafe 部分的规约编码为 Gillian-Rust
支持的规约语言 Gilsonite 并进行自动推理. 该研究使用 Gillian-Rust 自动验证了 Rust 标准库 LinkedList 模块中一
些双向指针列表的函数操作, 表明了该混合方法的有效性. 然而, Gillian-Rust 目前只是初步实现的原型工具, 还缺少
对很多 Rust 核心特性如共享引用的支持, 虽然文中表明此类扩展具有明确可行性, 只是工程性的工作.

4.3 定理证明方法
基于定理证明的形式验证将“系统满足其规约”这一论断作为逻辑命题, 通过一组推理规则对该命题开展证明.
该方法高度抽象, 具有强大的逻辑表达能力. 这里我们主要探讨交互式定理证明方式, 即在交互式定理证明器/证
明助手 (proof assistant) 中完成机械证明, 典型的工具包括 Coq [18] , Isabelle/HOL [51] 以及 Lean [52] 等. 基于定理证明的
方法验证 Rust 程序时, 利用 safe Rust 中对可变别名的限定, 自动转化其为某定理证明器语言描述的纯函数程序
(pure functional language), 进而利用现有的底层证明助手后端完成程序的进一步验证. 相比于上文提到的半自动程
序验证的方法, 该方法使用外在证明 (extrinsic proofs), 即所有的规范和证明工作都在证明助手中完成, 在 Rust 程
序中不需要添加注释. 而使用底层证明助手时可以以人工参与引导证明过程, 可以验证包括功能正确性在内的一
些复杂的性质. 其中, 将 Rust 语言嵌入到证明助手中包括浅嵌入 (shallow embedding) 和深嵌入 (deep embedding)
两种方式. 前者的实现相对简单, 直接将程序转成证明器自己的语言的项 (terms) 而不需要显式定义该语言的内部
语义, 但是表达能力相对有限, 也不能验证语义正确性相关的性质. 后者显式建模该语言的精准语义, 并将程序描
述成这一模型所表达的形式, 这种方式更灵活, 能适应复杂的验证需求, 但具有一定难度. 早期 Rust 验证工作采用
浅嵌入的方式, 后面逐渐定义出 Rust 的纯函数式语义. 然而由于定理证明的方法目前实现的函数式转换依赖于
Rust 类型系统提供的所有权保证, 因此只能处理不包含 unsafe 区块的程序. 图 15 描述了利用定理证明方法进行
Rust 代码验证的典型步骤.

人工辅助证明
Rust 定理 嵌入 已有定理 +自动证明 程序满足/
Rust 程序 中间表示
证明器 证明器 不满足规约
图 15 定理证明方法验证流程

早期的验证工具包括 Ullrich 等人 [43] 提出的 Electrolysis, 它将经过了编译器检查的 MIR 形式的 safe 程序翻译
为纯 lambda 演算, 以浅嵌入的形式描述成 Lean 语言的纯函数 (pure function), 并在后续基于 Lean 证明助手 [52] 验
证功能正确性, 为 Rust 程序验证提供了新的视角. 该方法信任借用检查器提供的内存安全保证, 因此主要检查程
序功能正确性. Electrolysis 通过透镜 (lenses) 模拟可变借用, 但因此带来了一些严格的限制, 例如, 函数只能返回对
它们第一个参数的借用. 此外, 由于 Electrolysis 没有建立 Rust 的形式模型, 因此没有证明其语义正确性. 它更像是
一个实用的“转译器”而不是编译器; 例如, Electrolysis 将 traits 映射到类型类 (type classes), 因为在高层次上它们的
工作方式相似. 实验中验证了二叉树搜索程序的功能正确性, 表明该方法的有效性.
Ho 等人 [44] 实现了针对 Rust 的新型定理证明器 Aeneas. 类似于 Electrolysis, Aeneas 将 safe Rust 程序转换成某
函数式语言描述的状态-错误单子 (state-error monad) 形式的函数程序, 并通过现有的底层证明助手后端进行后续