Certora/CertoraProver
GitHub: Certora/CertoraProver
面向智能合约的自动化形式化验证工具，通过数学证明确保合约满足指定的安全属性和不变量。
Stars: 302 | Forks: 37
[](https://gitmcp.io/Certora/CertoraProver)
[](https://x.com/certorainc)
# Certora Prover
Certora Prover 是一款用于形式化验证智能合约的工具。
本文档面向希望为该工具做出贡献的开发者。
如果您希望在我们的云平台上使用该工具而无需在本地进行构建，
我们建议您遵循此处的文档说明：https://docs.certora.com/en/latest/docs/user-guide/install.html。
此处的说明适用于 Mac OS 和 Linux 用户。
## 依赖项
* JDK 19+
* SMT 求解器：
* [必需] Z3 -- https://github.com/Z3Prover/z3/releases
* [必需] CVC5 -- https://github.com/cvc5/cvc5/releases
* [可选] CVC4 -- https://cvc4.github.io/downloads.html
* [可选] Yices -- https://github.com/SRI-CSL/yices2/releases
* [可选] Bitwuzla -- https://github.com/bitwuzla/bitwuzla/releases
* _注意_ 无论您决定安装哪种求解器，请务必将可执行文件放置在系统 `PATH` 中的某个目录下。
* Python 3
- 我们建议从此处下载：https://www.python.org/downloads/
- 确保 pip 的版本与 python 的版本相匹配
* Solidity 编译器 -- https://github.com/ethereum/solidity/releases。
请选择与您想要验证的合约所使用的版本相匹配的编译器版本。
由于我们经常使用许多不同的版本，建议将每个 `solc` 可执行文件重命名，
例如改为 solc5.12，并将所有版本放入系统 `PATH` 中的某个目录下，例如：`export PATH="/path/to/dir/with/executables:$PATH"`
* Rust（已在 1.81.0+ 版本上测试）-- https://www.rust-lang.org/tools/install
* [`llvm-symbolizer`](https://llvm.org/docs/CommandGuide/llvm-symbolizer.html) 和 [`llvm-dwarfdump`](https://llvm.org/docs/CommandGuide/llvm-dwarfdump.html)，
它们作为 LLVM 的一部分被安装。
* [`rustfilt`](https://github.com/luser/rustfilt)
## 可选依赖项：
* [`Graphviz`](https://graphviz.org/download/)：
Graphviz 是一个可选依赖项，用于渲染可视化元素，特别是 `dot`。
如果未安装，某些功能可能无法正常工作，例如 [Tac 报告](https://docs.certora.com/en/latest/docs/prover/diagnosis/index.html#tac-reports)。
_注意_ 请记住通过运行以下命令将 `dot` 添加到系统的 `PATH` 中：
```
export PATH="/usr/local/bin:$PATH".
```
* （请将 /usr/local/bin 替换为 dot 实际的安装路径。）
## 安装说明
* 在任意位置创建一个目录以存储构建输出。
- 添加一个环境变量 `CERTORA`，其值为该目录的路径。
- 同时将该目录添加到 `PATH` 中。例如，如果您使用的是 bash shell，可以像这样编辑您的 `~/.bashrc` 文件：
```
export CERTORA="preferred/path/for/storing/build/outputs"
export PATH="$CERTORA:$PATH"
```
* `cd` 进入您想要存储 CertoraProver 源码的目录并克隆该仓库：
git clone --recurse-submodules https://github.com/Certora/CertoraProver.git
* 通过运行以下命令编译代码：`./gradlew assemble`
* 如果您想清理项目的所有构建产物，请运行：`./gradlew clean`
* 确保您用于设置变量 `CERTORA` 的路径下包含重要的 jar 包、脚本和二进制文件，例如 `emv.jar`、`certoraRun.py`、`tac_optimizer`。
### 故障排除
- 我们建议在 Python 虚拟环境中进行工作，并在其中安装所有依赖项：
```
cd CertoraProver
python -m venv .venv
source .venv/bin/activate
pip install -r scripts/certora_cli_requirements.txt
```
- 如果您已经安装了 `Crypto`，可能需要先卸载它（`pip uninstall crypto`），然后再安装 `pycryptodome`
- 您可以通过 `cd` 进入 `fried-egg` 目录并运行 `cargo build --release` 来确保 `tac_optimizer` 构建正确。同时请确保 `tac_optimizer` 在您的路径中（使用 `CERTORA` 设置）。
## 运行
- 您可以通过运行 `certoraRun.py -h` 来查看所有选项并运行该工具。
- 在 `Public/TestEVM` 目录下有几个用于测试的小示例。例如，您可以像这样运行其中一个：
cd Public/TestEVM/CVLCompilation/OptionalFunction
certoraRun.py Default.conf
- 有关如何在真实智能合约上运行该 prover 的详细信息，请参考用户指南：https://docs.certora.com/en/latest/docs/user-guide/index.html
- 您可以直接从 IntelliJ 等 IDE 中运行单元测试，或者通过命令行使用 `./gradlew test --tests 标签：Bitwuzla, Certora Prover, CVC5, DeFi安全, EVM, JS文件枚举, Mac OS, Python, Rust, SMT求解器, Solana, Solidity, Stellar, Web3安全, Z3, 云安全监控, 代码分析, 代码安全, 以太坊, 凭证管理, 区块链安全, 去中心化应用安全, 可视化界面, 后台面板检测, 密码学验证, 形式化验证, 无后门, 智能合约审计, 漏洞枚举, 网络流量审计, 逆向工具, 静态分析