Creusot：为 Rust 代码提供形式化验证，确保逻辑正确性

背景

在软件工程中，尤其是对于系统级编程语言如 Rust，代码的正确性至关重要。虽然 Rust 的借用检查器（Borrow Checker）和类型系统已经极大地提高了内存安全性，防止了空指针解引用和数据竞争等常见错误，但它并不能证明代码在逻辑层面的正确性。例如，一个函数可能在语法和内存上完全安全，但在特定输入下仍可能产生错误的计算结果，或者未能满足特定的业务逻辑断言。

传统的测试方法（如单元测试）只能验证代码在已知用例下的行为，无法穷尽所有可能的输入路径，因此存在“测试盲区”。为了弥补这一缺陷，形式化验证（Formal Verification）应运而生。Creusot 正是在这一背景下诞生的一个针对 Rust 代码的演绎验证器（Deductive Verifier），旨在通过数学推导的方式，从逻辑上证明代码的正确性。

核心内容

Creusot 的核心功能是为 Rust 代码提供形式化验证，确保代码不仅内存安全，而且在逻辑上也是正确的。其工作原理和主要特性如下：

验证范围与能力

Creusot 主要验证以下三个方面：

1. 安全性（Safety）：确保代码不会发生 panic（恐慌/崩溃）、整数溢出或断言失败。
2. 逻辑正确性（Correctness）：通过添加注解（Annotations），用户可以进一步验证代码是否执行了预期的正确操作。这意味着开发者可以定义程序的“前置条件”和“后置条件”，Creusot 将证明代码在所有情况下都满足这些条件。

技术架构

Creusot 的工作流程基于翻译和自动化定理证明：

1. 代码翻译：Creusot 将 Rust 代码转换为一种中间验证语言，称为 Coma。
2. 平台集成：Coma 是 Why3 Platform 的一部分。Why3 是一个强大的框架，用于将程序验证问题转化为多种自动化定理证明器（Automated Theorem Provers）可处理的格式。
3. 半自动验证：用户利用 Why3 的强大功能，对生成的验证条件进行（半）自动化的 discharged（解除/证明）。这允许开发者结合自动化工具的强大能力与人工指导的灵活性来处理复杂的验证任务。

使用示例与测试套件

为了展示使用 Creusot 验证程序的实际效果，项目提供了一系列测试套件作为参考：

• Zeroing out a vector：清零向量操作。
• Binary search on Vectors：向量上的二分搜索算法。
• Sorting a vector：向量排序算法。
• IterMut：可变迭代器的验证。
• Normalizing If-Then-Else Expressions：If-Then-Else 表达式的规范化处理。

此外，项目还展示了更具挑战性的实际应用案例：

• CreuSAT：这是一个用 Rust 编写并通过 Creusot 进行验证的 SAT（布尔可满足性问题）求解器。该项目极大地考验了 Creusot 工具的极限，展示了其在“实战”（use in anger，指在生产环境中严格使用）场景下的能力。
• 目前还有另一个大型项目正在开发中。

安装与开发指南

对于希望使用或贡献代码的用户，Creusot 提供了明确的指引：

• 依赖环境：需要安装 rustup 以获取合适的 Rust 工具链，以及 opam（OCaml 的包管理器）。
• 安装步骤：克隆仓库后，进入 creusot 目录，运行 ./INSTALL 脚本进行安装，并通过 cargo creusot --help 验证安装是否成功。
• 更新与开发：开发者可以通过 git pull 更新源码，使用 opam update 更新包列表，并重新运行 ./INSTALL 来更新 Creusot。详细的开发者工作流请参考 CONTRIBUTING.md。

学术引用

如果需要在学术背景下引用 Creusot，建议参考其在 ICFEM'22 会议上发表的论文。

关键要点

• 超越内存安全：Creusot 不仅关注 Rust 的内存安全特性，更致力于通过演绎验证确保代码逻辑的正确性，防止逻辑错误和断言失败。
• Why3 生态集成：通过将其翻译为 Why3 平台的中间语言 Coma，Creusot 能够利用 Why3 成熟的半自动定理证明基础设施，降低了形式化验证的门槛。
• 注解驱动验证：用户需要通过添加注解来定义验证目标（如前置/后置条件），这使得验证过程更加灵活，能够针对特定的业务逻辑进行精确验证。
• 实战验证案例：通过验证 CreuSAT 这样一个复杂的 SAT 求解器，Creusot 证明了其在处理高复杂度、高可靠性要求软件时的可行性和有效性。
• 开源与社区支持：项目提供了详细的安装文档、测试用例以及 Zulip 聊天室和讨论论坛，方便用户获取帮助和交流。

意义与影响

Creusot 的出现对 Rust 生态系统及软件验证领域具有深远意义：

1. 提升关键软件的可信度：在金融、航空航天、操作系统内核等对错误零容忍的领域，传统的测试手段往往不足以提供足够的安全保障。Creusot 提供的形式化验证能力，为构建高可信系统提供了新的技术路径。
2. 降低形式化验证的门槛：形式化验证长期以来因其陡峭的学习曲线和复杂的数学背景而难以普及。Creusot 通过集成 Why3 平台，将复杂的验证过程转化为相对标准的“翻译+自动化证明”流程，使得更多 Rust 开发者能够接触到并利用形式化验证技术。
3. 推动 Rust 在安全关键领域的应用：随着 Rust 在系统编程领域的地位日益稳固，Creusot 这样的工具填补了 Rust 在逻辑正确性验证方面的空白，使其不仅适用于高性能应用，也更适合用于构建需要严格数学证明正确性的关键基础设施。
4. 促进“正确性由设计保证”的理念：通过鼓励开发者在编码阶段就通过注解定义程序的行为规范，Creusot 推动了“正确性由设计保证”（Correctness by Design）的工程实践，有助于在开发早期发现并修复逻辑缺陷，降低后期维护成本。

总之，Creusot 不仅是 Rust 语言的一个有用工具，更是将形式化验证技术带入主流开发实践的重要一步，为构建更可靠、更安全的软件系统提供了强有力的支持。