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

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

都得益于 Rust 的类型系统提供的内在保证. Box 类型确保了其值具有唯一的所有权, 这意味着 segm.0 和 segm.1
不可能是指向同一内存位置的别名, 这验证了属性 (2) 和 (3). Rust 的类型系统还要求, 要修改一个内存位置必须
拥有对该位置的独占访问权, 这消除了对线程交互执行的担忧, 也免去了显式证明无数据竞争的需要, 这验证了属
性 (4). 因此, 程序员在验证时只需要关注属性 (1) 的功能正确性证明即可.

1 fn shift_x(p: &mut Point, s: i32) {p.x = p.x + s}
2 fn align (mut segm: (Box<Point>, Box<Point>)) -> (Box<Point>, Box<Point>) {
3 let end_x = (*segm.1).x;
4 shift_x(&mut segm.1, (*segm.0).x - end_x);
5 assert!((*segm.0).x == (*segm.1).x);
6 segm
7 }
图 10 Rust 简化程序验证的例子

4.2 半自动化程序验证方法

半自动化 (auto-active) 程序验证的方法要求开发人员在实现代码上编写证明注释 (annotation), 例如前置条件、
后置条件和循环不变式. 验证器将注释代码转换为验证条件, 并调用约束求解器检查其有效性. Rust 的半自动验证
工具利用 Rust 语言类型系统提供的保证大大简化编写 Rust 验证工具所需要的规范和验证过程, 能够支持验证超
出内存安全的正确性属性, 如功能正确性. 这些工具多实现为了 rustc 编译的一个插件, 在编译器对 Rust 程序做完
类型检查和借用检查后, 对程序进行额外性质, 如功能正确性的验证. 近年来 Rust 半自动程序验证器的开发取得
了显著进展. 早期的 Rust 半自动验证器多是基于已有工具扩展了前端, 要将 Rust 转到该工具所支持的中间语言
继而复用后面的工具链进行验证, 这种方法在表达能力上存在一定的局限性, 后期开发者们设计了专门针对 Rust
语言特性的验证器, 不需要适配到中间语言. 得益于灵活丰富的表达能力和易用性, 这些新兴工具在 Rust 程序验
证实践中得到了广泛的使用. 图 11 概述了利用半自动化程序验证方法进行 Rust 代码验证的典型步骤. 然而, 实际
执行过程中可能会根据具体情况有所差异. 例如, Verus 验证器 [34] 没有转换中间表示语言这一步骤.

用户标注前置条件、

后置条件等 验证条件
Rust 半自动 转换 生成 求解 程序满足/
Rust 程序 化验证工具 中间表示 已有验证器 验证条件 SMT 求解器 不满足规约
图 11 半自动化程序验证方法流程

早期的半自动化验证工具包括 Astrauskas 等人 [33] 基于 Viper 分离逻辑引擎 [48] 提出的 Prusti. Prusti 将注释的
Rust 程序自动翻译成 Viper 中间验证语言并以模块化的方式自动验证 Rust 程序的功能正确性. 验证结果会从
Viper 翻译回 Rust, 并利用 Rust 编译器自身的错误报告机制向用户报告. Prusti 利用 Rust 编译器的类型检查和借
用检查信息, 在 Viper 框架中自动合成 Rust 程序内存安全的核心证明. 该证明是为自动化量身定制的分离逻辑的
一个变体. Prusti 基于该核心证明重新验证了 Rust 的借用检查器强制执行的所有权属性. 用户可以通过在 Rust 语
言的抽象层次上提供规范以扩展核心证明, 从而验证丰富的功能属性. Prusti 遵循传统半自动化验证器模块式的验
证方式, 即关注每个函数调用前后的旧值和当前值, 分别约束函数执行前/后需要满足的条件. 此外, Rust 类型系统
的一个复杂之处在于可变借用的概念, 这为表达函数的后置条件带来了挑战. 如图 12 所示, 针对包含可变借用的
程序, Prusti 提出了一套保证 (pledges) 规范构造, 在处理返回可变引用的函数时, 还考虑引用生命周期结束时该引
用的值并定义该程序点需要满足的条件. Prusti 在几个广泛使用的 Rust 库中数千个函数上评估了其有效性.
RustHorn [36] 通过利用 Rust 类型系统提供的所有权保证, 用一阶逻辑 (FOL) 公式表达有状态的 Rust 代码的行
为, 不需要显示表示指针和内存状态, 使得这些公式的验证可以利用现成的自动化技术. RustHorn 采用预言变量
(prophecy variables) 巧妙地解决了借用状态的追踪问题, 即将可变引用表示为当前目标对象值和借用结束时的一