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

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

Verus [34] 是首个利用 Rust 语言本身作为规范和证明语言的 Rust 验证器. 该方法使得 Verus 具有较高的验证效
率和更好的用户体验. 一方面, Verus 将带有注释的 Rust 程序直接自动转化为 SMT 求解器的输入来检查证明的正
确性, 而不需要先转化成某中间语言. 另一方面, 用户用 Rust 写规范 (spec) 和必要的辅助证明 (proof), 如循环不变
式, Verus 能够巧妙地利用 Rust 的线性类型和所有权检查来辅助 proof 的构建. Verus 引入 mode system 管理 Rust
写的 spec、proof 以及可执行代码, 确保对 spec mode 的规约程序做类型检查和终止性检查, 对 proof mode 的证明
程序做类型检查, 借用检查和终止性检查, 并只编译 Rust 可执行代码. 图 14 的例子中体现了使用 Verus 验证斐波
纳契数列函数功能正确性过程中的 3 种 mode. 与 Prusti 相比, Verus 信任 Rust 的类型检查器和借用检查器提供的
信息, 因此不需要使用分离逻辑.

1 spec fn fib_spec(input: nat) -> nat { proof fn lemma_fibo_is_monotonic(i: nat, j: nat) {
2 // We need to ensure something like `fixpoint` requires(i <= j);
3 functions terminates. ensures(fib_spec(i) <= fib_spec(j));
4 decreases(input); decreases(j - i);
5 match input { // specific proof goes here.
6 0 | 1 => input, }
7 _ => fib_spec(input − 1) + fib_spec(input −
8 2), fn fib(input: u64) -> u64{
9 } ensures(|result: u64| result == fib_spec(n));
10 } /// `fib`: implementation code goes here.
11 }
图 14 Verus 程序验证例子

除了支持更多的安全 Rust 特性外, Verus 的一大亮点是它支持一些传统上需要 unsafe 代码的验证, 为 Rust 程
序的验证提供了一种新的视角和方法. 在 Rust 中, 将某个特性标记为“unsafe”实际上意味着开发者需要承担起安
全使用该特性的责任, 这是 Rust 编译器所无法强制检查的. 而不安全的代码实际上可以被视为“条件性安全”, 即
只要满足一定的条件就是安全的. 基于这个思路, 该研究的理念是通过 Verus 验证 Rust 编译器无法检查的条件,
从而提供这样的安全保证. 为此, Verus 引入新的、遵循 Rust 唯一所有权原则的线性对象 (linear object). 为了避免
增加额外的数据负担影响程序的性能, 这些新对象还被设计为幽灵对象 (ghost objects), 即这些对象仅在验证过程
中可见, 帮助构建验证条件, 但对最终编译的程序没有直接影响. 以指针操作为例, Verus 允许定义一个幽灵对象,
代表“在给定位置读写内存的权利”. Rust 的类型系统保证了这个对象的唯一所有权, 而 Verus 则确保在程序访问
指针指向的数据时, 这一权利是被妥善管理的. 这种双重保障机制可以保证程序的内存访问是安全的, 没有数据竞
争的风险. 在验证双向链表这类复杂的数据结构时, 不仅按照常规方式组织节点和指针, 还会引入一组额外的幽灵
对象代表了访问节点的权利. 通过添加 Verus 的注释, 用户可以精确地描述这些幽灵对象与链表结构之间的关系.
通过此方式能够利用幽灵对象来安全地遍历链表, 而且通过数学证明来确保这一过程的正确性. 换句话说, 实际
上 Verus 不直接验证原始指针, 而是提供包含线性幽灵权限变量的抽象原始指针 API, 并提供额外的检查保证调
用该 API 代码的正确性实现. 除了针对非安全原始指针, Verus 还把这一理念用到了对内部可变性代码和并发代
码的验证上. 通过这种方式, Verus 扩展了 Rust 的能力, 允许开发者在编写高效代码的同时, 享受到严格的安全保
证, 从而在安全与性能之间找到了一个平衡点. 实验中在一系列示例上展示 Verus 如何通过幽灵对象和注释来验
证包括操作指针的代码 (一个基于异或的双向链表)、具有内部可变性的代码和并发代码. Verus 也存在局限性, 例
如, 由于 Verus 不支持函数返回可变引用, 因此不能验证如图 12 的例子.
Foroushaani 等人 [49] 扩展了 VeriFast [37] 模块化符号执行 (MSE) 算法, 提供了 Verifast 工具对 Rust 前端的支持,
是首个支持验证 unsafe Rust 代码片段语义类型安全的工作. 该工作将 RustBelt 对 Rust 类型的语义编码到 VeriFast
中, 验证输入程序即使有 unsafe 代码也不会导致未定义行为, 即程序不会访问未分配的内存或包含数据竞争. 验