查看原文
其他

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

张汉东 觉学社 2022-11-06

原文为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(1as &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


您可能也对以下帖子感兴趣

文章有问题?点此查看未经处理的缓存