AeneasVerif/aeneas

# Aeneas Aeneas（发音为 [Eh-nee-as]）是一个用于 Rust 程序的验证工具链。它依赖于从 Rust 的 MIR 内部语言到纯 lambda 演算的转换。它旨在与 [Charon](https://github.com/AeneasVerif/charon) 结合使用，后者将 Rust 程序编译为名为 LLBC 的中间 表示。它目前拥有 [F\*](https://www.fstar-lang.org)、 [Coq](https://coq.inria.fr/)、[HOL4](https://hol-theorem-prover.org/) 和 [LEAN](https://leanprover.github.io/) 的后端。 如果你想贡献代码或提出问题，我们强烈鼓励你加入 [Zulip](https://aeneas-verif.zulipchat.com/)。特别是，我们欢迎外部 贡献，但要求贡献者在深入修改 代码或实现非平凡功能之前与我们进行沟通，因为这些需要深入的设计 讨论和仔细的审查。如果你想贡献新功能，你应该在 Zulip 上讨论，或者在 github 上开启相应的 issue。 ## 项目结构 - `src`：OCaml 源代码。请注意，我们依赖 [Dune](https://github.com/ocaml/dune) 来构建项目。 - `backends`：现有后端的标准库（例如算术运算的定义，向量等标准集合，定理，策略等）。 - `tests`：将 Aeneas 应用于 Charon 的部分测试文件生成的文件， 并辅以手写文件（主要是证明脚本）。 ## 安装与构建 你需要安装 OCaml 以及一些包。 我们建议你按照这些[说明](https://ocaml.org/docs/install.html)进行操作， 并在过程中安装 OPAM（同样的说明）。 我们正在使用 **OCaml 5** 开发 Aeneas。例如，如果你想使用 OCaml 5.3.0： ``` opam switch create 5.3.0 ``` 然后你可以使用以下命令安装依赖项： ``` opam install calendar core_unix domainslib easy_logging menhir \ ocamlformat.0.27.0 ocamlgraph odoc ppx_deriving ppx_deriving_yojson \ progress unionFind visitors yojson zarith ``` 此外，Aeneas 使用了 [Charon](https://github.com/AeneasVerif/charon) 项目和库。 为了使 Aeneas 正常工作，`./charon` 必须包含 [Charon](https://github.com/AeneasVerif/charon) 仓库的一个克隆，且提交版本需符合 `./charon-pin` 的指定。最简单的设置方法是调用 `make setup-charon` （这会使用 [rustup](https://rustup.rs/) 或 [nix](https://nixos.org/download/) 来构建 Charon，具体取决于安装了哪一个）。 如果版本不匹配，系统将提示你更新 Charon。 如果你也在开发 Charon，你可以将 `./charon` 设置为指向你本地版本的符号链接： `ln -s PATH_TO_CHARON_REPO charon`。在这种情况下，脚本将不会检查你的 Charon 安装是否处于兼容的提交版本。当你拉取新版本的 Aeneas 时，你偶尔 需要更新你的 Charon 仓库，以便 Aeneas 能够正确构建和运行。 最后，只需在顶层目录中运行 `make` 即可 构建项目。 你还可以使用 `make test` 和 `make verify` 来运行测试，并检查 生成的文件。由于 `make test` 将运行使用 Charon 测试的测试， 你需要重新生成 `.llbc` 文件。为此，请在 `make test` 之前运行 `make setup-charon`。或者，调用 `REGEN_LLBC=1 make test-...` 来仅重新生成所需的文件。 ## 文档 如果你运行 `make`，你将生成一份可从 [`doc.html`](./doc.html) 访问的文档。 此外，[这里](./tests/lean/Tutorial/) 提供了使用 Aeneas Lean 后端的教程；原始的 Rust 文件可以在[这里](./tests/src/tutorial/src/lib.rs)找到。 它需要安装有效的 Lean。 ## 用法 你应该首先通过在你想翻译的 crate *内部*调用 Charon （类似于 cargo）来生成序列化的 `.llbc` 文件。**重要提示：**你应该 使用以下选项调用 Charon： ``` charon cargo --preset=aeneas ``` Aeneas 的二进制文件位于 `bin` 中；你可以运行：`./bin/aeneas -backend {fstar|coq|lean|hol4} [OPTIONS] LLBC_FILE`， 其中 `LLBC_FILE` 是由 Charon 生成的 .llbc 文件。 Aeneas 提供了大量的 flag 和选项来调整其行为：你可以使用 `--help` 来显示详细的文档。 ## 目标子集和当前限制 Aeneas 目前对安全 Rust 的一个子集进行了函数化，我们正在 通过引入基于分离逻辑的推理来扩展函数模型，以 支持 unsafe 代码和并发代码。 我们目前对*安全*子集有以下限制，我们计划逐一 解决： - **循环**：暂不支持在*嵌套*循环内使用 `return`，或向*外层*循环使用 `break`/`continue` （例如，`'a : loop { loop { break 'a; } } `）。这是一个 技术限制，而非根本性问题，我们计划在 不久的将来解决它，并且可以根据用户的需求确定优先级。 以下限制将随着分离逻辑方面的工作进展而被解除： - **unsafe 代码** - **并发** 如果你需要某些特定功能或 有兴趣贡献代码，请随时联系团队或加入 Zulip。 ## 后端支持 我们目前支持 F\*、Coq、HOL4 和 Lean。我们对开发 Isabelle 后端很感兴趣。我们最成熟的后端是 Lean 和 HOL4，特别地， 我们为它们提供了对部分函数和外部终止证明的支持（参见 `./backends/lean/Base/Diverge/Elab.lean` 和 `./backends/hol4/divDefLib.sig`）， 以及专为单子程序设计的策略（参见 `./backends/lean/Base/Progress/Progress.lean` 和 `./backends/hol4/primitivesLib.sml`）。 ## 将 Rust 定义的模型添加到 Lean 后端 在翻译需要外部定义（即来自外部依赖项（如 Rust 标准库）的定义）的 crate 时，我们建议使用 `-split-files` 选项。使用 `-split-files` 时，Aeneas 将生成模板文件，其中列出了 用户必须提供手写模型的缺失定义。 例如，它可能会在 Lean 中生成以下结构： ``` ... // Files containing type definitions, etc. FunsExternal_Template.lean // automatically generated template file FunsExternal.lean // hand-written file maintained by the user (not overwritten during the translation) Funs.lean // automatically generated file which imports FunsExternal.lean ``` 与其将模型添加到 `TypesExternal.lean`、`FunsExternal.lean` 等文件中， 不如将这些模型移植到 Aeneas 标准库，这样所有客户端项目 都可以从中受益。这样做时，务必要让 Aeneas 知道这些新 模型。这可以通过使用适当的 attribute （`rust_type`、`rust_const`、`rust_fun`、`rust_trait` 或 `rust_trait_impl`）标注 Lean 模型，然后运行 命令 `make extract-lean-std` 来完成。此命令将构建 Aeneas 的 Lean 库， 收集这些定义，并重新生成 `src/extract/ExtractBuiltinLean.ml` 文件， 该文件提供了有关这些模型的信息。 请注意，当在 `TypesExternal.lean` 等文件中列出缺失的外部定义时，Aeneas 会自动引入 `rust_type` 等 attribute： 用户只需复制/粘贴这些定义并填补漏洞（holes）。另外请注意， 这些 attribute 有相当多的选项可以调整提取的行为： 我们邀请用户阅读它们的 docstring 以获取更多信息。 ## Nix 用户的快速入门 假设已安装 Nix，并且支持 Flakes（`*`）： ``` $ # Run Charon with the exact same version required by Aeneas $ nix run github:aeneasverif/aeneas#charon -L $ nix run github:aeneasverif/aeneas -L -- -backend your_preferred_backend your_llbc.file ``` 要重新生成提取内容，只需再次运行第 2 步和第 3 步。 `(*)`：Flakes 并非必需，以下是在没有它的情况下执行类似步骤的示例： ``` $ nix-shell '' -A packages.x86_64-linux.charon --run "charon" -I aeneas=https://github.com/AeneasVerif/aeneas/archive/main.tar.gz $ nix-shell '' -A packages.x86_64-linux.default --run "aeneas --backend your_preferred_backend your_llbc.file" -I aeneas=https://github.com/AeneasVerif/aeneas/archive/main.tar.gz ``` ## 形式化 该转换已经过形式化，并在 ICFP2022 上发表：[Aeneas：通过函数 转换进行 Rust 验证](https://dl.acm.org/doi/abs/10.1145/3547647) （[长版本](https://arxiv.org/abs/2206.07185)）。我们还有一个证明表明， Aeneas 在转换期间执行的符号执行正确地 实现了 borrow checker，并在 ICFP 2024 上发表：[Sound Borrow-Checking for Rust via Symbolic Semantics](https://dl.acm.org/doi/10.1145/3674640)（[长版本](https://arxiv.org/abs/2404.02680)）。

标签：OCaml, Rust, Web安全扫描, 可视化界面, 定理证明, 形式化验证, 漏洞数据库, 编译器工具链, 网络流量审计