Kani：一款Rust模型检查器

# Kani：一个针对 Rust 的模型检查器  
来源：https://arxiv.org/html/2607.01504  

Rémi Delmas, Zyad Hassan, Qinheping Hu, Rahul Kumar, Felipe R\. Monteiro, Thanh Nguyen, Adrián Palacios, Celina Val  
Amazon Web Services  
Vancouver  
BC  
Canada,  
Michael Tautschnig  
Amazon Web Services  
Seattle  
WA  
USA  
Queen Mary University  
London  
United Kingdom,  
Justus Adam  
Brown University  
Providence  
RI  
USA,  
Daniel Schwartz\-Narbonne  
Datadog  
New York  
NY  
USA  
and  
Carolyn Zech  
Massachusetts Institute of Technology  
Cambridge  
MA  
USA  
\(2026\)  

###### 摘要。  
Rust 的所有权类型系统能在安全代码中防止内存错误，但某些理想属性仍然独立于编译过程：`unsafe` 操作（例如原始指针解引用）的健全性、函数正确性以及运行时恐慌的缺失。我们介绍了 Kani，一个开源的 Rust 模型检查器，它将有界模型检查从漏洞发现提升为对这些属性提供正确性保证。Kani 将 Rust 中级中间表示（MIR）中的证明脚手架编译到 CBMC 的位精确验证引擎中，无需用户注释即可自动检查一组全面的安全属性。为了将验证从有界扩展到无界，Kani 提供了一个规范语言，包括函数契约、循环契约、量词和函数桩代码。我们通过对工业 Rust 项目的案例研究证明了可行性，其中契约将验证从无恐慌提升到函数正确性，发现了六个先前未知的缺陷。Kani 在生产 CI 中大规模运行，在 Rust 标准库验证活动中每次代码更改验证超过 16,000 个脚手架。  

模型检查，Rust，形式验证，规范语言  

††会议：39th IEEE/ACM International Conference on Automated Software Engineering；2026年10月12-16日，德国慕尼黑  
††期刊年份：2026  
††版权：无  
††CCS：软件及其工程 软件验证与确认  
††CCS：软件及其工程 形式化软件验证  

## 1\. 引言  

Rust 已成为安全关键系统软件的首选语言，从嵌入式操作系统 (Levy et al., 2017 (https://arxiv.org/html/2607.01504#bib.bib7); Boos et al., 2020 (https://arxiv.org/html/2607.01504#bib.bib6)) 和加密协议 (Bhargavan et al., 2025b (https://arxiv.org/html/2607.01504#bib.bib5)) 到云基础设施 (Agache et al., 2020 (https://arxiv.org/html/2607.01504#bib.bib68))。其所有权类型系统能静态防止数据竞争和许多类内存错误 (Jung et al., 2017 (https://arxiv.org/html/2607.01504#bib.bib3))，但编译器无法证明三类正确性属性：(1) `unsafe` 操作的正确性（例如原始指针解引用、调用 `unsafe` 函数、访问可变静态变量、`unsafe` trait 实现和联合体字段访问），此时编译器仍强制执行借用检查和类型安全，但开发者负责确保这些操作所需的安全不变量 (Astrauskas et al., 2020 (https://arxiv.org/html/2607.01504#bib.bib62); Cui et al., 2024 (https://arxiv.org/html/2607.01504#bib.bib63))；(2) 函数正确性属性，例如算法正确性和协议符合性；以及 (3) 在恐慌不可取的上下文中，由 `unwrap()`、整数溢出和越界访问等操作导致的运行时恐慌的缺失。测试和模糊测试能暴露其中一些故障，但它们仅探索输入空间的有限样本，不提供完备性保证。  

针对 Rust 的演绎验证工具，包括 Prusti (Astrauskas et al., 2022 (https://arxiv.org/html/2607.01504#bib.bib34))、Creusot (Denis et al., 2022 (https://arxiv.org/html/2607.01504#bib.bib21)) 和 Verus (Lattuada et al., 2023 (https://arxiv.org/html/2607.01504#bib.bib67))，能证明丰富的函数属性。然而，它们需要大量的证明工程（例如分离逻辑或幽灵状态），这限制了在专业团队之外的采用 (Huang et al., 2026 (https://arxiv.org/html/2607.01504#bib.bib11))。而在另一个极端，像 Miri (Jung et al., 2026 (https://arxiv.org/html/2607.01504#bib.bib59)) 这样的动态工具能在运行时检测未定义行为，但无法证明其不存在。这两个极端之间存在差距：开发者需要一种验证方法，既能以高度自动化和低注释成本开始，又能随着验证需求的增长逐步扩展到更强的正确性保证。  

有界模型检查填补了这个差距中自动化的端。有界模型检查器对默认安全属性（例如算术溢出、除零、空指针解引用、断言违反）进行编码，并在一个界限内穷举检查，所需的手动证明构造极少。这使其成为验证的有效切入点：开发者编写类似于单元测试的证明脚手架，工具在界限内对所有输入证明属性。其局限性在于，有界分析本身无法保证超出展开深度的正确性。为了将模型检查从漏洞发现推向正确性证明，必须用规范构造来扩展该技术，从而在保持有界检查可访问的低注释开销的同时，实现无界推理。  

本文介绍了 Kani，一个开源的 Rust 模型检查器，实现了从有界分析到无界正确性保证的演进。Kani 建立在代码级模型检查方法论 (Chong et al., 2020 (https://arxiv.org/html/2607.01504#bib.bib18), 2021 (https://arxiv.org/html/2607.01504#bib.bib19)) 之上，该工作表明，使用 CBMC (Kroening and Tautschnig, 2014 (https://arxiv.org/html/2607.01504#bib.bib10)) 进行有界模型检查可以集成到工业 C 代码库的持续开发工作流中。Kani 将此方法论扩展到 Rust，操作于中级中间表示（MIR）以保留 Rust 特定的类型不变量，并添加了一个规范语言，包括函数契约、循环契约、量词和函数桩代码。这些构造允许开发者逐步注释其代码：Kani 首先在无注释的情况下证明默认安全属性，然后随着契约的添加，将同一验证引擎扩展到无界函数正确性证明。我们通过对 Hifitime 时间管理库的案例研究证明了该方法的可行性，其中添加契约以较低的规范开销将保证从无恐慌升级为函数正确性，并通过 AI 编程助手进行 AI 辅助的规范起草。  

Kani 在生产 CI 中大规模部署：证明脚手架在 Firecracker (Agache et al., 2020 (https://arxiv.org/html/2607.01504#bib.bib68))（AWS Lambda 和 AWS Fargate 背后的虚拟机监视器）、s2n-quic（亚马逊对 IETF QUIC 传输协议的 Rust 实现）、Hifitime (Rabotin, 2024 (https://arxiv.org/html/2607.01504#bib.bib70))（用于航空航天领域的时间管理库）以及 Rust 标准库验证活动 (Cook et al., 2026 (https://arxiv.org/html/2607.01504#bib.bib66))（每次代码更改验证超过 16,000 个脚手架）中对每次代码更改运行。  

我们做出以下贡献：  

1. \(1\) 我们在多个工业 Rust 项目上评估了 Kani，它发现了测试和模糊测试遗漏的十一个缺陷。通过对 Hifitime 库的详细案例研究，我们展示了基于契约的验证以较低的规范开销将 Kani 的默认安全检查扩展到无界函数正确性证明（§5 (https://arxiv.org/html/2607.01504#S5)）。  
2. \(2\) 我们形式化了 Kani 的规范语言，包括函数契约、循环契约、量词和函数桩代码，将语义建立在 Floyd-Hoare 逻辑基础上，并将它们连接到底层的有界模型检查引擎（§4 (https://arxiv.org/html/2607.01504#S4)）。  
3. \(3\) 我们介绍了 Kani 的架构、其 MIR 级别的设计以及它与 Rust 工具链的集成（§3 (https://arxiv.org/html/2607.01504#S3)）。  

## 2\. Kani 示例  

我们使用欧几里得最大公约数（GCD）算法及其在 Firecracker (Agache et al., 2020 (https://arxiv.org/html/2607.01504#bib.bib68)) 中的使用来说明 Kani 的验证工作流。Firecracker 是一个开源的虚拟机监视器，在轻量级微虚拟机中运行工作负载。Firecracker 为 AWS Lambda 和 AWS Fargate 提供动力，因此其 Rust 代码库的正确性是安全关键问题。GCD 函数在 Firecracker 的速率限制器中用于简化令牌桶补充比率，其迭代循环使其成为有界和无界验证的自然目标。  

### 2\.1\.有界验证  

考虑 Firecracker 的 `rate_limiter` 模块中的迭代 GCD 实现：  

```rust
fn gcd(x: u64, y: u64) -> u64 {
    let mut a = x;
    let mut b = y;
    while b != 0 {
        let t = b;
        b = a % b;
        a = t;
    }
    a
}
```

开发者可以编写一个 Kani *证明脚手架*，类似于单元测试但针对所有可能的输入，以验证 `gcd` 返回一个公约数：  

```rust
#[kani::proof]
#[kani::unwind(94)]
fn check_gcd() {
    let x: u64 = kani::any();
    let y: u64 = kani::any();
    kani::assume(x > 0 && y > 0);
    let d = gcd(x, y);
    assert!(d != 0 && x % d == 0 && y % d == 0);
}
```

调用 `kani::any()` 生成给定类型的非确定性值，而 `kani::assume` 约束输入空间。注意：不正确的假设（例如 `assume(false)`）会使证明空洞成立，因此必须像代码本身一样仔细审查假设。  

Kani 展开循环，将结果转换为 SSA 形式，并将所有断言编码为命题公式（§4\.1 (https://arxiv.org/html/2607.01504#S4.SS1)），然后使用 SAT 求解器进行检查。`#[kani::unwind(94)]` 注解设置循环展开界限。对于 64 位输入，欧几里得算法的最坏情况迭代次数为 93（小于 \(2^{64}\) 的最大斐波那契数是 \(F_{93}\)）；界限保守地设置为 94。如果界限不足，Kani 会报告一个*展开断言失败*，警告开发者验证结果在给定深度之外是未定的。即使界限足够，生成的公式也非常大：在我们的实验中，对完整 `u64` 范围的 GCD 进行有界验证在一小时超时内未终止。此外，该界限特定于 64 位整数；改变输入类型需要重新计算它。  

### 2\.2\.使用契约进行无界验证  

我们用函数契约（前置条件和后置条件）和循环契约（不变量和递减子句）来注释 `gcd`。循环契约通过归纳不变量抽象循环，消除对展开界限的依赖：  

```rust
#[kani::requires(x > 0 && y > 0)]
#[kani::ensures(|&result| result > 0)]
fn gcd(x: u64, y: u64) -> u64 {
    let mut a = x;
    let mut b = y;
    #[kani::loop_invariant(
        a > 0 &&
        kani::forall!(|d: u64 in (1, a.saturating_add(1))|
            d == 0 || ((x % d == 0 && y % d == 0) == (a % d == 0 && b % d == 0))
        )
    )]
    #[kani::loop_decreases(b)]
    while b != 0 {
        let t = b;
        b = a % b;
        a = t;
    }
    a
}
```

`requires` 子句声明前置条件：两个输入都必须是正数。`ensures` 子句声明后置条件：结果为正。在循环内部，`loop_invariant` 在所有迭代中主张两个属性：(1) `a` 保持为正数，以及 (2) 对于每个候选除数 `d`，`d` 整除原始输入 `(x, y)` 当且仅当它整除当前值 `(a, b)`，即公约数集合保持不变。`saturating_add` 在计算量词范围的上界时避免溢出。`loop_decreases` 子句指定 `b` 是一个良基的递减度量（因为 `a % b < b`）。由于模运算保持正数，验证在 Z3 中于 0.54 秒内通过所有 202 项检查，执行完整管道：量化的循环不变量、终止证明以及所有自动生成的安全检查。  

这个不变量不平凡：它需要在全称量化语句上进行非线性算术。在实践中，许多验证任务只需要简单的契约，Kani 无需任何注释即可自动检查这些契约。GCD 示例展示了当需要函数正确性时，Kani 规范语言的表达能力。  

##### 验证契约。  
一个专用的 `proof_for_contract` 脚手架通过 `kani::any()` 设置非确定性输入并调用 `gcd`；Kani 假设前置条件，执行函数，并断言后置条件。`#[kani::solver(z3)]` 属性选择 Z3 SMT 求解器，这是量化不变量所需的。循环不变量通过归纳验证（§4\.4 (https://arxiv.org/html/2607.01504#S4.SS4)）：循环体在单个 BMC 查询中恰好执行两次，无论输入大小如何。  

##### 失败时的表现。  
当后置条件被违反时，Kani 报告契约表达式和源代码位置。例如，Hifitime 的 `total_nanoseconds()` 中的符号错误（§5\.2 (https://arxiv.org/html/2607.01504#S5.SS2)）产生：  

```
Check 1: ... total_nanoseconds:: {closure#2} - Status: FAILURE
- Description: "|result| { *result == i128::from(self.centuries) * i128::from(NPC) + i128::from(self.nanoseconds) }"
VERIFICATION: - FAILED (0.26s)
```

##### 使用已验证的契约。  
一旦验证通过，该契约即可作为组合推理的可靠抽象。在 Firecracker 中，`TokenBucket::new` 调用 `gcd` 来简化令牌桶补充比率。使用 `#[kani::stub_verified(gcd)]`，脚手架将 `gcd` 替换为其契约：在调用点断言前置条件，并假设一个满足后置条件（`result > 0`）的非确定性返回值。无需展开循环，验证在几秒内完成，且对所有 64 位输入都使用可靠抽象。  

## 3\. 架构  

Kani 是一个开源的验证工具，与标准 Rust 工具链集成。可以通过 `cargo kani` 在 Cargo1 上调用（类似于 `cargo test`），也可以通过 `kani` 在单个 crate 上调用。内部，Kani 重用整个 `rustc` 前端，但替换代码生成后端：它不是通过 LLVM 发射机器码，而是将 Rust 程序翻译成 CBMC 可以模型检查的 GOTO 程序 (Kroening et al., 2023 (https://arxiv.org/html/2607.01504#bib.bib46))。  

一个关键设计决策是操作于 Rust 的中级中间表示（MIR）而不是 LLVM IR。MIR 保留了单态化后的类型信息、枚举判别式布局以及 Rust 的有效性不变量（例如，`bool` 是 0 或 1，`char` 是有效的 Unicode 标量），这些在 LLVM IR 中被丢弃。这使得 Kani 能够自动检查 Rust 特定的安全属性，并推理动态 trait 对象和闭包，这些在 LLVM 级别会被擦除 (Van Hattum et al., 2022 (https://arxiv.org/html/2607.01504#bib.bib2))。  

如图 1 所示，管道从 Rust 源代码流经 Kani 编译器到 CBMC 和 SAT/SMT 求解器，其中 `kani-driver` 编排每个阶段。  

（图 1 标题：Kani 验证管道。蓝色框是 Kani 组件；灰色框是外部工具；绿色是编排器。白色框表示输入/输出。虚线箭头表示编排控制流。）  

##### 编译。  
验证会话从 `cargo kani` 开始，它调用 `kani-driver`，即编排器（图 1 中的绿色框）。驱动调用 `kani-compiler`，它是一个 `rustc` 插件，在 MIR 生成后通过 `rustc_private` 接口连接到编译器。标准 `rustc` 前端执行解析、名称解析、类型检查、trait 解析和单态化，生成带类型的 MIR。然后 Kani 应用 MIR 到 MIR 的转换：可达性分析、契约和循环契约的插装。  

（以下部分未完整给出，但根据要求，我们只翻译提供的原文内容。）