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

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

对值. 在创建一个新的可变借用&mut a 时, 我们对其最终状态 a o 进行了预言, 这就像是对程序未来状态的一次预
见. 在创建借用时, 我们并不立即确定 a o 的值. 我们用当前状态 a 和预言的借用结束后值 a o 来表示可变引用 ma,
形成一对值⟨a, a o ⟩. 当这个可变引用⟨a, a o ⟩ 的生命周期结束, 即所有权被释放时, 我们确立了 a o =a 的关系, 意味着最
终状态 a o 被设定为那个特定时刻的当前状态 a——这一过程称为预言决议 (prophecy resolution). 随后, 这一决议
可以被有效地“传递”回原始的所有者, 从而明确告知借用结束后对象的确切状态. RustHorn 的这一核心概念, 为
Rust 程序提供了一种用一阶逻辑形式来描述的方法, 使得程序验证更加高效和直观. 例如, 图 13 的左边 Rust 代
码 (和图 12 同样的函数) 会被 RustHorn 转成右边的一阶逻辑公式表示, 并验证程序满足第 6 行断言. 在 max_mut
函数中, 第 2 行被 drop 的引用 (如第 1 个分支的 mb) 其值就被决定了 (如相应的 mb.b o =mb.b). 而另一个被返回的
引用, 会在第 5 行被 mc 继续修改.

1 #[ensures(*result >= old(*ma) && *result >= old(*mb))]
2 #[ensures(*result == old(*ma) || *result == old(*mb))]
3 #[after_expiry(if old(*ma >= *mb) { (*ma == before_expiry(*result) && *mb == old(*mb))}
4 else {(*ma == old(*ma) && *mb == before_expiry(*result))})]
5 fn take_max<'a>(ma: &'a mut i32, mb: &'a mut i32) -> &'a mut i32 {
6 if *ma >= *mb { ma } else { mb }
7 }
8 #[requires(a < i32::MAX && b < i32::MAX)]
9 #[ensures(result == true)]
10 fn inc_max(mut a: i32, mut b: i32) -> bool {
11 { let mc = take_max(&mut a, &mut b); // borrow a and b
12 *mc += 1; // end of borrow}
13 a != b
14 }
图 12 Prusti 程序验证例子

1 fn take_max<'a>(ma: &'a mut i32, mb: &'a mut i32) ->
2 &'a mut i32 {if *ma >= *mb { ma } else { mb } }
3 fn inc_max(mut a: Box<i32>, mut b: Box<i32>) {
4 {let mc = take_max(&mut a, &mut b);
5 *mc += 1;
6 assert!( *a != *b); }
7 }

图 13 RustHorn 程序验证例子

RustHorn 实现了一个原型验证器, 针对 Rust 子集进行了实现, 并通过初步实验确认了该方法的有效性, 但该工
具在表达能力和性能上具有较大的局限性. RustHorn 作者通过非机械化的证明, 证明了其逻辑编码对于原始 Rust 程
序内存的语义的可靠性. 随后, RustHornBelt 利用 RustBelt 框架, 机械化地证明了 RustHorn 风格逻辑编码的可靠性.
后续, Denis 等人 [35] 基于 RustHornBelt 提出的理论实现了 Creusot 工具. 类似于 RustHorn, Creusot 将 Rust 程
序转化为一阶逻辑 (FOL) 公式, 使用 RustHorn 风格的预言 (prophecy-based) 处理可变引用. 此外, Creusot 引入了
一个用于描述功能正确性等规范的注释语言 Pearlite, 并通过良好的规范设计提供了对 trait 验证的支持. Creusot
以带有规范注释的 Rust 程序作为输入, 转化为后端引擎 Why3 的中间表示并生成验证条件, 使用 SMT 求解器进
行验证.