Kani：为 Rust 打造的有界模型检查器——从 Bug 发现到正确性保证

本文介绍 Kani，一个针对 Rust 的开源模型检查器，通过将 MIR 编译到 CBMC 引擎，自动验证不安全代码、功能正确性与运行时恐慌的缺失，并提供契约与存根以实现无界验证。

背景：Rust 的安全承诺与验证缺口

Rust 的所有权类型系统是其最核心的卖点：它在编译时通过借用检查器（Borrow Checker）确保内存安全，消除了空指针解引用、缓冲区溢出、释放后使用等常见内存错误。然而，Rust 的安全承诺只覆盖了“Safe Rust”代码。在实际工程中，我们不可避免地需要编写或依赖 unsafe 代码块——例如直接操作裸指针、调用 FFI（外部函数接口）、实现底层数据结构或与硬件交互。在这些代码中，编译器不再提供安全保证。

更关键的是，即便对于 Safe Rust，编译器的静态检查也无法覆盖所有重要的正确性属性：

• 功能正确性：程序是否按照预期逻辑运行？例如，一个排序函数是否真的返回了有序序列？
• 运行时恐慌（panic）的缺失：unwrap()、索引越界、整数溢出等操作可能在运行时触发恐慌，导致程序崩溃。
• 不安全操作的健全性：例如，从裸指针构造引用时是否满足别名规则？

这些问题在编译时是“正交”的——它们与类型系统的推理无关，因此传统编译器不会报错。这就需要一种更强大的静态分析工具：模型检查器（Model Checker）。

Kani 是什么？

Kani 是一个开源的、针对 Rust 的模型检查器，由 Amazon Web Services（AWS）的研究团队开发，并被接受于 2026 年 IEEE/ACM 国际自动化软件工程会议（ASE 2026）的工业展示环节。它的目标是将 有界模型检查（Bounded Model Checking, BMC） 从简单的 Bug 发现提升到正确性保证的层次。

简单来说，Kani 能够自动验证 Rust 程序在给定输入边界下是否满足某些安全属性，并且不需要用户编写任何额外的注解（annotation）即可检查一组全面的安全属性。当需要超越有界验证时，Kani 提供了一套规格语言（specification language），包括函数契约、循环契约、量词和函数存根，帮助用户将验证范围从有限扩展至无限。

核心工作原理：从 MIR 到 CBMC

Kani 的工作流程可以概括为三个步骤：

1. 编译到 MIR：Rust 编译器将源代码编译为中级中间表示（Mid-level Intermediate Representation, MIR）。MIR 是 Rust 编译器内部的一种低级、类型化、控制流清晰的 IR，非常适合进行静态分析和转换。

2. 生成验证条件：Kani 将用户编写的“证明框架（proof harness）”——类似于测试用例，但使用符号变量而非具体值——从 MIR 编译成 CBMC（C Bounded Model Checker）的位精确验证引擎（bit-precise verification engine）。CBMC 本身是一个成熟的 C/C++ 程序模型检查器，能够处理位级运算、指针算术和内存模型。

3. 符号执行与 SMT 求解：CBMC 对生成的中间表示进行符号执行，将所有可能的执行路径编码为 SAT/SMT（可满足性模理论）公式，然后使用后端求解器（如 MiniSat、Z3）检查是否存在违反属性的路径。如果存在，Kani 会生成一个反例（counterexample），帮助开发者定位问题。

Kani 默认检查的安全属性包括：

• 数组越界访问
• 空指针解引用
• 除零错误
• 整数溢出（在调试模式下）
• 无效的枚举变体访问
• 恐慌安全（panic safety）
• 不安全代码中的内存安全（如裸指针引用有效性）

所有这些检查都不需要用户编写任何注解——你只需要提供一个带有 #[kani::proof] 属性的函数，Kani 就会自动分析该函数及其调用的所有代码。

从有界到无界：规格语言的力量

有界模型检查的局限性在于它只能验证有限深度的路径（例如，循环展开到固定次数）。对于许多实际程序，这已经足够发现大量 Bug，但无法提供“对于所有可能的输入，程序都正确”的保证。

Kani 通过提供以下规格语言来突破这一限制：

• 函数契约（Function Contracts）：使用 #[kani::requires] 和 #[kani::ensures] 注解来定义前置条件和后置条件。例如，你可以声明一个排序函数的输入数组长度必须大于 0，并且输出数组必须是有序的。Kani 会验证函数实现是否满足这些契约，并且在调用点检查契约是否被满足。

• 循环契约（Loop Contracts）：通过 #[kani::loop_invariant] 指定循环不变量，帮助 Kani 证明循环在所有迭代中的正确性，从而避免无限展开。

• 量词（Quantifiers）：支持 forall 和 exists 表达式，用于描述集合性质。例如，“对于所有索引 i，输出数组的第 i 个元素小于第 i+1 个元素”。

• 函数存根（Function Stubbing）：允许用户用简化的模型替换复杂的外部函数（例如系统调用、硬件驱动）。这在验证大型项目时至关重要，因为你可以隔离出需要验证的核心逻辑，而将外部依赖抽象为契约化的存根。

这些机制共同使得 Kani 能够对无界的程序进行验证——例如，证明一个递归函数对所有输入都终止，或者一个无限循环的服务器程序不会出现内存泄漏。

工业案例：从恐慌自由到功能正确性

论文中报告了在工业 Rust 项目上的案例研究，其中 Kani 的契约升级了验证的层次：

• 初始状态：团队通常使用 Kani 检查“恐慌自由”（panic-freedom），即确保代码不会在运行时崩溃。这已经很有价值，但并不能保证代码逻辑正确。
• 引入契约后：通过添加函数契约，团队能够验证功能正确性——例如，一个加密库的加密函数是否真正实现了 AES 算法，或者一个网络协议的解析器是否严格遵守规范。

在案例研究中，Kani 发现了 6 个此前未知的 Bug。这些 Bug 可能存在于安全的 Rust 代码中，但由不正确的逻辑或对不安全代码的误用引发。值得注意的是，这些 Bug 在传统的测试中未被发现，因为测试只能覆盖有限的输入空间，而 Kani 的符号执行能够探索更广泛的路径。

大规模生产环境中的 CI 集成

Kani 最令人印象深刻的一点是它的可扩展性。论文提到，在 Rust 标准库的验证活动（Rust standard library verification campaign） 中，Kani 被集成到持续集成（CI）流水线中，每次代码变更都会运行 超过 16,000 个验证框架（harnesses）。

这 16,000 个 harness 覆盖了标准库中的关键模块（如 Vec、HashMap、String、slice 等），确保每次提交都不会引入新的恐慌路径或违反契约。这种规模表明 Kani 不仅是一个研究原型，而是一个经过实战检验的工业级工具。

与其他 Rust 验证工具的比较

在 Rust 生态系统中，还有其他一些验证工具，例如：

• Prusti：基于分离逻辑（Separation Logic），通过用户提供的注解进行验证，侧重于所有权和借用规则的形式化。
• Creusot：将 Rust 代码翻译到 Why3 验证平台，支持丰富的规格语言，但需要用户掌握 Why3 的证明机制。
• MIRAI：一个抽象解释器，用于检测整数溢出、恐慌等常见问题，但不如 Kani 深入。
• Rust's built-in #[cfg(test)]：单元测试，只能覆盖有限的具体输入。

Kani 的独特优势在于：

1. 零注解起步：对于恐慌自由检查，用户只需一个 #[kani::proof] 注解，无需额外规格。
2. 位精确语义：直接处理底层位级运算，适合嵌入式系统、加密算法等需要精确位操作的领域。
3. 工业级规模：已经证明可以处理数万个 harness 的 CI 流水线。
4. 与 CBMC 的结合：继承了 CBMC 数十年的工程积累，包括对指针、动态内存分配和并发模型的成熟支持。

局限与未来方向

尽管 Kani 很强大，但它并非万能：

• 有界性：即使使用契约，某些属性（如完全无界的内存安全）可能需要更复杂的归纳证明，而 Kani 的自动化程度有限。
• 性能：对于大型代码库，符号执行可能面临路径爆炸问题。16,000 个 harness 的运行时间可能较长（论文未给出具体数据，但通常需要数分钟到数小时）。
• 用户学习曲线：虽然基本使用简单，但编写正确的契约（尤其是循环不变量和量词）需要一定的形式化方法知识。

未来的改进方向可能包括：更好的反例可视化、对并发和异步代码的支持、以及更高效的求解器集成。

总结

Kani 是 Rust 生态系统中一个里程碑式的工具。它填补了编译时检查与运行时测试之间的空白，使得开发者能够以合理的成本获得更高层次的正确性保证。对于任何编写或依赖 unsafe 代码的 Rust 项目——尤其是系统软件、嵌入式固件、加密库和网络协议实现——Kani 都是一个值得纳入 CI 流程的利器。

正如论文标题所示，Kani 不仅是一个 Bug 查找器，更是一个模型检查器：它能够对程序的行为进行数学建模，并在有限或无限的输入空间中验证其正确性。对于追求高可靠性的 Rust 项目来说，这可能是从“看起来能跑”到“数学上正确”的关键一步。

原文链接：https://arxiv.org/abs/2607.01504