Coq-of-rust: Formal verification tool for Rust

Source | HN Comments

`coq-of-rust`是一个用于Rust代码的形式化验证工具，它将Rust程序翻译成Coq证明系统。通过该工具，开发者可以对代码进行数学证明，确保其在所有执行情况下都没有错误，包括避免panic和业务规则漏洞。该工具支持Rust的多种语言特性，并提供工作流程，包括翻译、改进、规范编写和证明。`coq-of-rust`旨在提高代码的可靠性，减少错误，并提供形式化验证服务。

Coq-of-rust：Rust 代码的形式化验证工具

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

即使 Rust 的类型系统可以避免许多错误，包括内存错误，代码仍然不能避免诸如意外 panic 或错误实现的业务规则等漏洞。更进一步的方法是数学上证明它是没有错误的：这被称为“形式化验证”，而这正是 coq-of-rust 所提供的！这是确保您的代码不包含错误或漏洞的唯一方法，即使是面对国家级别的攻击者 🧚 也能确保安全。

我们提供形式化验证即服务，包括规范设计和证明。➡️开始使用 🦸 ⬅️

coq-of-rust 的开发主要由 Aleph Zero Foundation 资助。我们感谢他们的支持！

示例

coq-of-rust 的核心是将 Rust 程序翻译成证明系统 Coq 🐓。一旦一些 Rust 代码被翻译成 Coq，就可以使用标准的证明技术进行验证。

这是一个 Rust 函数的例子:

fn add_one(x: u32) -> u32 {
  x + 1
}

运行 coq-of-rust，它在 Coq 中被翻译成:

Definition add_one (τ : list Ty.t) (α : list Value.t) : M :=
 match τ, α with
 | [], [ x ] =>
  ltac:(M.monadic
   (let x := M.alloc (| x |) in
   BinOp.Panic.add (| M.read (| x |), Value.Integer Integer.U32 1 |)))
 | _, _ => M.impossible
 end.

BinOp.Panic.add 等函数是我们提供的 Coq 中 Rust 的标准库的一部分。然后，我们可以在 Coq 中表达和验证代码的规范。

工作流程

以下是使用 coq-of-rust 的典型工作流程：

graph TB
  R[Rust code 🦀] -- coq-of-rust --> T[Translated code 🐓]
  T -- name resolutions --> L[Linked code 🐓]
  L -- refinement --> S[Simulations 🐓]
  S --> P
  SP[Specifications 🐓] --> P[Proofs 🐓]
  P -.-> X[100% reliable code! 🦄]

我们首先使用 coq-of-rust 将我们要验证的 Rust 代码自动翻译成 Coq 代码。最初的翻译结果非常冗长。我们会经过两个半自动的改进步骤，links 和 simulations，逐步使代码更适合进行形式化验证。

最后，我们编写规范 (specifications) 并证明 (prove) 我们的 Rust 程序在任何可能的用户输入 🔥 下都能满足这些规范。

典型的规范示例包括：

代码不能 panic。
这个巧妙的数据结构与其朴素版本等效，只是执行时间不同。
这个新版本引入了新的 endpoints 并且进行了大量的重构，它与之前的版本完全向后兼容。
数据不变性被正确地保留。
存储系统是可靠的，因为进出的东西是一样的（这通常意味着序列化/反序列化函数是互逆的）。
一旦正式表达，该实现的行为就如白皮书所描述的特殊情况一样。

有了这些，你几乎可以将你的错误和漏洞减少到零 🦸!

原理

形式化验证可以防止关键软件中的所有错误。

Rust 的类型系统已经提供了强大的保证来避免 C 或 Python 中存在的错误。我们仍然需要编写测试来验证业务规则或不存在 panic。测试是不完整的，因为它无法覆盖所有执行情况。

通过形式化验证，我们可以覆盖所有情况（代码 100% 没有错误！）。我们用代码的数学推理代替测试。您可以将其视为类型系统的扩展，但没有表达上的限制。

工具 coq-of-rust 将 Rust 程序翻译成经过实战检验的形式化验证系统 Coq，以使 Rust 程序 100% 安全 🚀。

先决条件

Rust
Coq (参见 coq-of-rust.opam)

安装和用户指南

构建教程提供了构建和安装 coq-of-rust 的详细说明，而用户教程介绍了 coq-of-rust 命令行界面和支持的选项列表。

语言特性

翻译工作在 Rust 的 THIR 中间表示级别进行。

我们支持 Rust Book by Examples 中 99% 的 Rust 示例。这包括：

基本控制结构（如 if 和 match）
循环 (while 和 for)
引用和可变性 (& 和 &mut)
闭包
panics
用户类型 (struct 和 enum)
traits 的定义
traits 或用户类型的实现关键字 impl

联系方式

如需对您的 Rust 代码库进行形式化验证服务，请通过 contact@formal.land 联系我们。形式化验证可以应用于智能合约、数据库引擎或任何关键的 Rust 项目。与其他技术（如人工审查或测试）相比，这提供了对不存在错误的最高置信度。

替代项目

以下是其他致力于 Rust 形式化验证的项目：

Aeneas: 从 MIR 翻译到纯函数式的 Coq/F* 代码。自动将代码放入函数式形式。请参阅他们的论文 Aeneas: Rust verification by functional translation。
Hacspec v2: 从 THIR 翻译到 Coq/F* 代码
Creusot: 从 MIR 翻译到 Why3（然后是 SMT 求解器）
Verus: 使用注释自动验证 Rust
Kani: 使用 CBMC 进行模型检查

贡献

这都是开源软件。

打开一些 pull requests 或 issues 来为此项目做出贡献。欢迎所有贡献！本项目在 AGPL 许可下对 Rust 代码（翻译器）开源，在 MIT 许可下对 Coq 库开源。有一些代码取自 Creusot 项目，以使 Cargo 命令 coq-of-rust 并在与 Cargo 相同的上下文中运行翻译。