论文导读 ｜ 使用 Kani 验证 Rust 中的 trait 对象

“

原文为2022年5月发布的论文《Verifying Dynamic Trait Objects in Rust》^[1] 。 注意，本文不是对该论文的全文翻译，而是论文关键摘要总结，仅供学习使用。

该论文是康奈尔大学和亚马逊工程师合作编写的，本文主要介绍开源的 Kani Rust verifier^[2] 验证工具如何使用 MIR 表示的语义trait信息进行验证。该团队在调研 500 个下载次数最多的 Rust 库中发现，有 37% 使用表示动态调用的 dyn 关键字，而动态调度隐式调用达到70%（rustc编译时至少有70%包含一个vtable）。Kani 是第一个用于 Rust 的符号建模检查工具，提供了用于动态 trait 对象的开源验证方法。

Kani 简介

虽然 Rust 语言类型系统可以检查大多数内存安全问题，但仍然有很多执行错误的方法。因此，亚马逊（AWS 推动）和康奈尔大学的合作构建了开源工具 Kani ，用于对 Rust 程序进行健全、位精确的符号分析，主要目标是能无缝集成到 Rust 大型现有项目中。目前 kani 已经被集成到了开源的 Firecraker 虚拟机监视器组件上，Firecraker 为 AWS 的 Lambda 和 Fargate 提供虚拟化。

该团队在实现 Kani 的过程中，发现一个意想不到的挑战，就是对动态 trait 对象的方法表进行建模。默认情况下，  trait 方法调用是通过泛型限定的方式静态分发，即单态化。但是，开发者也可以使用 dyn 关键字来获得动态表达能力，即使用 trait对象。Rust 的闭包和匿名函数也可以通过 trait 对象动态调度（因为它们都实现了 FnOnce/FnMut/Fn）。

因为 Rust 生态库中大量使用 trait 对象，所以 kani 的目标就包括了对 Rust 标准库和 crate 提供全面支持。Kani 是目前唯一一个针对 Rust MIR 并且可以推理动态 trait 对象和动态闭包符号的模型检查工具。Kani 作为 Rust 编译器后端而实现，该编译器后端使用成熟的工业强度模型检查工具 「C 有界模型检查器（CBMC）^[3]」作为验证引擎。Kani 将 Rust MIR 翻译为 GOTO-C（CBMC 类 C 的中间语言）。可以使用 Cargo 对单个rust 文件或 crate 来调用 Kani 。Kani 可以检查用户添加的断言、算术溢出、越界内存访问和无效指针，对于 Unsafe Rust 尤其有用。但默认情况下， Kani 使用断言方式运行。

Rust trait 概述

trait 静态分发（单态化）

泛型限定

trait 通常通过泛型限定进行静态分发，比如：

trait Countable { 
 fn count(&self) -> usize; 
}


impl Countable for Vec { 
 fn count(&self) -> usize { 
  self.len() 
 } 
} 

impl Countable for Bucket { 
 fn count(&self) -> usize { 
  self.item_count 
 } 
}

fn print_count(obj: T) { 
 print!("Count = {}", obj.count()); 
}

上面定义的泛型函数 print_count 在 MIR 层面就会被单态化为具体类型的函数：

fn print_count_vec_i8(obj: Vec) { 
 print!("Count = {}", obj.count::>()); 
} 

fn print_count_bucket(obj: Bucket) { 
 print!("Count = {}", obj.count::()); 
}

闭包单态化

此外，闭包也可以作为 trait 限定：

fn price<T: Fn(f32)->f32>(cost: f32, with_tax: T) 2 -> f32 { 
 with_tax(cost) 
}

fn main(){
    let tax_rate = 1.1; 
 price(5., |a| a * tax_rate); // Price is: 5.5 
 price(5., |a| a + 2.);
}

上面两个调用闭包的代码 Rust 也会对其单态化：

fn see_price_closure@main:1(cost: f32) -> f32 { 
 closure@main:1([closure@main:1], cost)  // 这里要存储 cost
} 

fn see_price_closure@main:2(cost: f32) -> f32 ... // 这里不需要存储 cost

单态化成本

单态化可以提升性能，但是会增加编译文件大小和编译时间。

trait 动态分发（trait 对象）

为了权衡运行时效率和改进代码大小和编译时间，开发人员可以使用 trait 对象来进行动态分发（避免单态化）。

trait Countable { 
 fn count(&self) -> usize; 
}

// `&dyn Countable` trait对象，动态分发
fn print_count(obj: &dyn Countable) { 
 print!("Count = {}", obj.count()); 
}

当调用 print_count 时，编译器不会为每个具体类型创建一个新函数，而是使用一个 print_count 实例和可以表示所有实现 Countable 的对象实例。

trait 对象由一个胖指针表示，这个胖指针包含了一个指向对象本身（数据）的指针和一个指向其实现方法的虚表（Vtable）的指针。

因为 Vtable 需要跳转到动态计算的地址，所以它们可能会在安全攻击中被利用，因此它们的精确实现具有隐患。虽然 Rust 的非正式规范中没有指出 Vtable 的布局，但 MIR 提供了用于构建特定形式 Vtable 的实用函数。Kani 参考了 LLVM 后端中 Vtable 的特定布局。

“

在 LLVM 后端中，Vtable 中包含着对象元数据（数据的大小和对齐方式），以及每个方法实现的函数指针。每个 vtable 中都包含一个指向具体类型的 drop（析构函数）方法实现的函数指针。

// 上面 print_count 函数等价于
fn print_count(obj: &dyn Countable) {
 print!("Count = {}", 
  *(obj.vtable.count)(obj.vtable.data)
 ); 
}

// 当使用 as 强转具体类型为 trait 对象时
// 该 trait 对象的胖指针就会包含一个指向 Bucket 的指针和指向 Vtable 的指针
print_count(&Bucket::new(1) as &dyn Countable);

Kani 对 trait 对象验证的方式

因为 GOTO-C 没有对 trait 对象 的原生支持，所以 Kani 在实现的时候，只能遵循 LLVM 后端的 Vtable 实现来保持 trait 对象的语义。但 Kani 生成的 Vtable 对象是 GOTO-C 结构。

Kani 在实现 trait 对象验证的过程中遇到了下面的一些问题：

• 不同trait 但可能存在同名的方法，会造成歧义。 Kani 使用 MIR Api 返回的 vtable_entries 来解决此问题，MIR 保留了大部分 Rust 类型的语义信息，这些丰富的类型信息提供了帮助。
• Rust 目前不支持 trait upcasting （需要更改底层 vtable 实现，目前这个工作正在进行中），即将 trait 对象向上转换为它的 suptertrait 的 trait对象。但是对于 auto trait 来说可以进行强转，Kani 最初忽略了这一点。
• Rust 的借用检查器和动态分发之间有一些微妙的联系。闭包解糖之后实际对应三种类型的方法签名（FnOnce(self)/FnMut(&mut self)/Fn(&self)），但是 Kani 当初只围绕 self 进行验证。

与其他语言无关的验证工具相比，Kani 的优势是可以利用 Rust 的语义提高验证的完整性和性能。

AWS  EC2 应用案例： Firecracker

在对 Firecracker 进行验证过程中一个巨大挑战是代码中使用了很多 std::io::Error trait 对象（错误处理），这让 CBMC 符号执行引擎无法在四小时内完成任务。Kane 实现了一种「基于 trait 的函数指针限制」模式，将该过程加速了 15 倍。

相关测试代码见：icse22ae-kani^[4]

其他类型工具比较

• CRUST，一个类似于 Rust 的有界模型检查器，也使用 CBMC 工具作为验证后端。但是 CRUST 明确不支持 trait对象，并且不再积极开发。
• Prusti，一个建立在 Viper 验证基础设施上的 Rust 编译器插件，同 Kani 一样，Prusti 也通过 MIR 类型信息改进验证结果。Prusti 的类型注释语言比 Kani 更具表现力，包括支持循环不变量，允许验证 Kani 目前无法验证的程序。但是 Prusti 对 Unsafe 的代码支持有限，并且不支持 trait 对象。
• Crux-MIR，使用 Galois 的 Crucible 验证器，同样基于 MIR 。它可以通过 &dyn 指针引用验证动态分发的简单情况，但不支持 Box<dyn T>和动态闭包对象（如 &dyn Fn()）。
• MIRAI （facebook 开源）是一个 MIR 抽象解释器，不提供健全性验证。
• 其他一些基于 LLVM IR 的验证工具，伴随着无法理解 Rust 类型级别语义的缺陷。
• SMACK 工具链
• RVT（来自 Google Research）

小结

Kani 是致力于提供在大型 Rust 项目中部署验证，本论文介绍了 Kani 如何支持 trait 对象的验证，并且展示了如何基于 MIR 中的类型信息将验证速度提升了 15 倍。

目前 Kani 正在积极开发中，Kani 的主要更改记录在 RFC Book^[5]中。目前支持相当数量的 Rust 语言特性，但不是全部（比如还不支持并发）。请参阅Rust feature support^[6]以获取支持特性的详细列表。Kani 每两周发布一次。作为每个版本的一部分，Kani 将与最近的 Rust Nightly 版本同步。

如需进一步了解 Kani 的应用，可以参考延伸阅读。

延伸阅读

• https://whileydave.com/2021/10/26/test-driving-the-rust-model-checker-rmc/
• https://model-checking.github.io/kani/

参考资料

[1]

《Verifying Dynamic Trait Objects in Rust》: https://www.cs.cornell.edu/~avh/dyn-trait-icse-seip-2022-preprint.pdf

[2]

Kani Rust verifier: https://github.com/model-checking/kani

[3]

C 有界模型检查器（CBMC）: https://www.cprover.org/cbmc/

[4]

icse22ae-kani: https://github.com/avanhatt/icse22ae-kani

[5]

RFC Book: https://model-checking.github.io/kani/rfc

[6]

Rust feature support: https://model-checking.github.io/kani/rust-feature-support.html