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

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

的程序验证. 不同的是, Aeneas 设计了 Rust 以所有权为中心的函数式操作语义, 并使用基于借用 (loan) 的方式对
程序进行了借用检查, 而没有相信 Rust 编译器的检查结果. 具体来说, Aeneas 提出了语法类似 MIR 的低级借用演
算 (low-level borrow calculus, LLBC), 并赋予其纯粹的函数式的操作语义. 该语义是基于值的, 因此没有内存、地
址或指针算术的概念, 减轻了证明过程中复杂的内存的推理. 进一步地, Aeneas 将 LLBC 转为纯 lambda 演算, 允
许用户通过指定的定理证明器验证程序. Aeneas 目前提供了对 F*和 Coq 的支持, 后续计划扩展到 Lean, HOL4
等. 为处理函数返回借用这一复杂情况, Aeneas 使用类似于 Creusot 中预言的方法, 通过反向函数 (backward function)
来重构借用结束后返回给原始对象的值. 如, 图 12 的例子会被 Aeneas 自动转为图 16 所示 F*函数式表示. 文章通
过实验结果表明, Aeneas 可以验证一个低级的、可调整大小的哈希表的功能性正确性.

let inc_max_fwd : result unit =
1 let take_max_fwd (t : Type) (x : t) (y : t) : result t =
val <-- if x>=y then true else false;
2 if x>=y then Return x else Return y
i <-- take_max_fwd i32 1 2;
3
z <-- i32_add i 1;
4 let take_max_back (t : Type) (b : bool) (x : t) (y : t) (ret : t) :
massert (z = 3); (* monadic assert *)
5 result (t & t) =
6 if b then Return (ret, y) else Return (x, ret) (x0, y0) <-- take_max_back i32 val 1 2 z;
7 } massert (x0 = 1);
8 massert (y0 = 3);
9 Return ()
图 16 Aeneas 程序验证例子

4.4 模型检测方法
模型检测方法将验证对象抽象成一个形式化的状态机模型, 并使用状态空间搜索的方法遍历该模型, 以此检
查模型是否满足特定规约. 模型检测方法容易实现验证过程的机器完全自动化, 且当系统性质未被满足时可给出
反例轨迹, 帮助用户定位错误位置. 但该技术只能对有限状态进行验证, 且存在状态空间爆炸问题. 因此, 该方法对
于复杂性较高、规模较大程序的验证存在局限性. 为了缓解该问题, 有界模型检测 (bounded model checking) 通过
限制程序执行情况的搜索空间, 如限制循环或递归的深度, 在牺牲一定准确性的情况下提升模型检测的效率. 此
外, 由于并发程序交替执行时, 每一步都可以由两个程序中的任意一个进行, 使得其可能的执行顺序远不止一种,
导致模型检测方法在处理并发问题时效率低下. 为了缓解该问题, 无状态模型检测 (stateless model checking) 不直
接追踪程序状态的变化, 而是通过特殊的调度程序遍历所有并发执行调度情况, 从而对并发程序所有可能的执行
进行搜索. 图 17 描述了利用模型检测方法进行 Rust 代码验证的典型步骤.

程序满足/
不满足规约
用户写验证用例 Rust 模型 编译 已有模型
Rust 程序 中间表示 状态机模型 SMT 求解器
检查器 检查器
程序不满足
规约的反例

图 17 模型检测方法验证流程

Toman 等人结合穷举测试用例生成和有界模型检测技术提出 Crust [38] , 验证 unsafe Rust 代码的内存安全, 并
判断 Rust 指针别名的使用是否违反不变量. Crust 以某库模块为输入, 使用基于测试序列生成的方式自动构造调
用了目标模块中关键函数的一系列驱动函数. Crust 将这些驱动函数和 Rust 库代码共同编译为 C 中间表示, 使用
针对 C 语言的有界模型检测器 CBMC [53] 来验证每个被检测函数的内存安全属性. 为了测试 Crust 的有效性, 该研
究选择了向量 (vector), 切片 (slice) 和环形缓冲区 (ring buffer) 这 3 个内部调用了 unsafe 代码块的 Rust 标准库模
块, 在其中手动引入两个内存错误, 实验结果表明 Crust 能够发现引入的两个内存错误.