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

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

同样基于 CBMC, AWS 团队 [40] 提出 Rust 语言的有界模型检查器 Kani. 相比于 Crust, 除了验证包含 unsafe 代
码程序的内存安全性外, Kani 允许验证用户在 Rust 程序中自定义的验证条件, 并支持检测运行时 panic, 算数溢出
等未定义行为. 后续 Byrnes 等人还扩展了 Kani 对 trait 的支持 [54] . 用户使用 Kani 手动编写类似单元测试的验证用
例, Kani 求解器会遍历状态空间树以检查验证用例是否正确, 如果不正确将报告反例分支. 例如, 下面的代码示例
展示了 Kani 对数组越界访问的检查. 图 18 所示 Kani 验证用例示例中, #[kani::proof] 属性用于标记一个函数作为
证明框架 (proof harness); kani::any 的方式符号化地表示变量为所有可能的输入值, 并通过 assume 设置前置条件
约束. 该证明框架类似于测试框架, 特别是基于属性的 (property-based) 测试框架, 使得验证过程对开发者来说更
加自然熟悉. 由图 18 可见, 针对上文的例子, 用户不需要在 take_max 函数手动插桩对返回可变引用的限制条件,
Kani 就可以验证通过 inc_max 函数中的 assert 条件. 此外, Kani 还可以测试 unsafe 代码, 对于图 6 例子, Kani 会发
现指针访问越界的解引用错误. 而相比之下, unsafe 代码可以绕过 Rust 基于属性的动态测试. 相比于早期的其他
模型检查器, Kani 覆盖更广泛的 Rust 特性, 是较为成熟的工业级工具, 已经广泛用于 Rust 标准库, Tokio, Firecracker
虚拟机监视器等多种真实程序的验证. 然而, Kani 也有很多局限. 首先, 它提供较为通用和简单的断言机制, 而其
他如 Prust 这类的工具则允许更精细的描述和验证特定的语言特性, 例如所有权和借用检查. 如图 19 的例子, 当所
有权从原对象 p 转移到 pp 时, 右边 Kani 在第 6 行 assert 声明的断言中不能再使用原对象 p, 因此会报错. 为了解
决这个问题, 开发者可以在调用 shift 的函数中引入中间变量暂存 p 的值, 再在调用 shift 后和返回的 pp 值作比较,
但该方法不够直观且增加了代码的复杂性. 相比之下, Prusti 后置条件中基于 old 关键字提供了一种更为方便的方
式来描述和验证所有权转移前后对象的状态. old(shift) 表示了 shift 函数执行前 (即所有权移动前) 的值, 使得可以
直观且精确地表达对象 p 和 pp 之间的关系, 实现函数功能正确性验证. 其次, 其执行的是有界模型检查而不是无
界验证, 由于循环展开次数有限, 得到的结果没有可靠性保证. 此外, Kani 将 Rust 程序编码成类似 C 的表示形式,
为每种结构实例化一个特定的布局并在该上下文中执行模型检查, 使得其不能描述布局敏感的 Rust 代码. 同时,
Kani 只能验证顺序执行的程序, 不能验证数据竞争等性质.

fn inc_max(mut a: i32, mut b: i32) -> bool { #[kani::proof]
1
{ fn main() {
2
let mc = take_max(&mut a, &mut b); let mut a = kani::any();
3
4 *mc += 1; let mut b = kani::any();
5 } kani::assume (a < i32::MAX);
6 let result = a!=b; kani::assume (b < i32::MAX);
let c = inc_max(a, b);
7 assert!(a!=b);
}
8 result}
图 18 Kani 验证例子 1

// Prusti code //Kani code
1 #[requires(u32::MAX - *p.x >= s)] fn shift (p: Point, s: u32) -> Point {
2 #[ensures(*result.x == old(*p.x) + old(s))]
let mut pp = p;
3 #[ensures(*result.y == old(*p.y))]
let x = pp.x; // p.x is moved out.
4 fn shift(p: Point, s: u32) -> Point {
pp.x = add(x, s); // x is moved into add,
5 let mut pp = p;
assert!(*pp.y==*p.y+s); // error: value used here after move
6 let x = pp.x; // p.x is moved out.
pp}
7 pp.x = add(x, s); // x is moved into add,
}
8 pp
9 }
图 19 Kani 验证例子 2