bitstable-fi/echidna
GitHub: bitstable-fi/echidna
一个用于以太坊智能合约的基于属性的模糊测试工具，帮助发现合约中的安全缺陷。
Stars: 0 | Forks: 0
# Echidna: 快速智能合约模糊测试器 
Echidna 是一种会吃掉错误并且高度电敏感的生物（感谢 Jacob Stanley）
更严肃地说，Echidna 是一个用于模糊测试/基于属性的测试以太坊智能合约的 Haskell 程序。它使用基于[合约 ABI](https://solidity.readthedocs.io/en/develop/abi-spec.html) 的复杂语法模糊测试活动来发现用户定义的谓词或[Solidity 断言](https://solidity.readthedocs.io/en/develop/control-structures.html#id4) 中的问题。我们设计 Echidna 时考虑了模块化，因此可以轻松扩展以包含新的变异或针对特定合约进行测试。
## 功能
* 生成针对实际代码的输入
* 可选的语料库收集、变异和覆盖率引导，以发现更深层次的错误
* 通过 [Slither](https://github.com/crytic/slither) 在模糊测试活动前提取有用信息
* 源代码集成以识别模糊测试后哪些行被覆盖
* 交互式终端 UI，仅文本或 JSON 输出
* 自动测试用例最小化以快速分类
* 无缝集成到开发工作流程中
* 模糊测试活动的最大 gas 使用报告
* 支持使用 [Etheno](https://github.com/crytic/etheno) 和 Truffle 进行复杂的合约初始化
.. 以及一个精美的高分辨率手工制作 logo。
## 用法
### 执行测试运行器
Echidna 的核心功能是一个名为 `echidna` 的可执行文件，它接收一个合约和一个不变式列表（应始终保持为真的属性）作为输入。对于每个不变式，它会生成随机调用序列并检查不变式是否成立。如果能找到某种方式来证明该不变式不成立，它会打印出导致不成立的调用序列。如果找不到，则表明合约是安全的。
### 编写不变式
不变式表示为 Solidity 函数，函数名以 `echidna_` 开头，没有参数，并返回布尔值。例如，如果你有一个 `balance` 变量永远不应低于 `20`，你可以在合约中编写如下额外函数：
```
function echidna_check_balance() public returns (bool) {
return(balance >= 20);
}
```
要检查这些不变式，运行：
```
$ echidna myContract.sol
```
一个包含测试的示例合约可以在 [tests/solidity/basic/flags.sol](tests/solidity/basic/flags.sol) 中找到。要运行它，你应该执行：
```
$ echidna tests/solidity/basic/flags.sol
```
Echidna 应该能找到使 `echidna_sometimesfalse` 不成立的调用序列，并且应该无法找到使 `echidna_alwaystrue` 不成立的输入。
### 收集和可视化覆盖率
完成活动后，Echidna 可以将最大化的 **语料库** 保存到通过 `corpusDir` 配置选项指定的特殊目录中。该目录将包含两个条目：(1) 一个名为 `coverage` 的目录，其中包含可由 Echidna 重放的 JSON 文件；(2) 一个名为 `covered.txt` 的纯文本文件，即带有覆盖率注释的源代码副本。
如果你运行 `tests/solidity/basic/flags.sol` 示例，Echidna 将在 `coverage` 目录中保存一些序列化交易文件，并生成名为 `covered.$(date +%s).txt` 的文件，内容如下：
```
*r | function set0(int val) public returns (bool){
* | if (val % 100 == 0)
* | flag0 = false;
}
*r | function set1(int val) public returns (bool){
* | if (val % 10 == 0 && !flag0)
* | flag1 = false;
}
```
我们的工具使用以下“行标记”对语料库中的每个执行跟踪进行标记：
* `*` 如果执行以 STOP 结束
* `r` 如果执行以 REVERT 结束
* `o` 如果执行因耗尽 gas 而结束
* `e` 如果执行因任何其他错误（零除、断言失败等）而结束
### 支持智能合约构建系统
Echidna 可以测试使用不同智能合约构建系统编译的合约，包括 [Truffle](https://truffleframework.com/) 或 [hardhat](https://hardhat.org/)，通过 [crytic-compile](https://github.com/crytic/crytic-compile)。要使用当前构建框架调用 echidna，请使用 `echidna .`。
除此之外，Echidna 支持两种测试复杂合约的模式。首先，可以[使用 Truffle 和 Etheno 描述初始化过程](https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/end-to-end-testing.md)，并将其作为 Echidna 的基础状态。其次，Echidna 可以通过在 CLI 中传递相应的 Solidity 源代码来调用任何具有已知 ABI 的合约。使用 `allContracts: true` 在配置中开启此功能。
### Echidna 速成课程
我们的 [构建安全智能合约](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna#echidna-tutorial) 仓库包含 Echidna 的速成课程，包括示例、课程和练习。
### 在 GitHub Actions 工作流中使用 Echidna
有一个 Echidna 操作，可以用于在
GitHub Actions 工作流中运行 `echidna`。请参考
[crytic/echidna-action](https://github.com/crytic/echidna-action) 仓库获取
使用说明和示例。
### 配置选项
Echidna 的 CLI 可用于选择要测试的合约并加载配置文件。
```
$ echidna contract.sol --contract TEST --config config.yaml
```
配置文件允许用户选择 EVM 和测试生成参数。一个带有默认选项的完整且带注释的配置文件示例可以在
[tests/solidity/basic/default.yaml](tests/solidity/basic/default.yaml) 找到。
有关配置选项的更多详细信息，请查阅我们的
[维基](https://github.com/trailofbits/echidna/wiki/Config)。
Echidna 支持三种不同的输出驱动程序。默认的 `text` 驱动程序、`json` 驱动程序，以及应抑制所有 `stdout` 输出的 `none` 驱动程序。JSON 驱动程序按如下方式报告整体活动：
```
Campaign = {
"success" : bool,
"error" : string?,
"tests" : [Test],
"seed" : number,
"coverage" : Coverage,
"gas_info" : [GasInfo]
}
Test = {
"contract" : string,
"name" : string,
"status" : string,
"error" : string?,
"testType" : string,
"transactions" : [Transaction]?
}
Transaction = {
"contract" : string,
"function" : string,
"arguments" : [string]?,
"gas" : number,
"gasprice" : number
}
```
`Coverage` 是一个描述某些覆盖率增加调用的字典。
每个 `GasInfo` 条目是一个元组，描述了如何实现最大 gas 使用情况，并且这些接口目前不太重要。这些接口将在未来变得更易于用户使用。`testType` 将是 `property` 或 `assertion`，`status` 始终为 `fuzzing`、`shrinking`、`solved`、`passed` 或 `error`。
### 调试性能问题
诊断 Echidna 性能问题的一种方法是使用性能分析运行 `echidna`。
要使用基本性能分析运行 Echidna，请在原始 `echidna` 命令中添加 `+RTS -p -s`：
```
$ nix develop # alternatively nix-shell
$ cabal --enable-profiling run echidna -- ... +RTS -p -s
$ less echidna.prof
```
这将生成一个报告文件 (`echidna.prof`)，显示哪些函数占用了最多的 CPU 和内存。
如果基本性能分析没有帮助，可以使用更多[高级性能分析技术](https://input-output-hk.github.io/hs-opt-handbook.github.io/src/Measurement_Observation/Heap_Ghc/eventlog.html)。
我们观察到的性能问题的常见原因包括：
- 在热路径中调用的昂贵函数
- 积累 thunk 的惰性数据构造函数
- 热路径中使用的低效数据结构
检查这些是很好的起点。如果你怀疑某些计算过于懒惰并导致内存泄漏，可以使用 `force` 从 `Control.DeepSeq` 来确保它被求值。
## 限制和已知问题
EVM 模拟和测试很难。Echidna 在最新版本中存在一些限制。其中一些是从 [hevm](https://github.com/ethereum/hevm) 继承的，而另一些则是由于设计/性能决策或代码中的简单错误。我们在此列出这些问题及其对应的 issue 和状态（“wont fix”、“on hold”、“in review”、“fixed”。“fixed” 的问题预计将在下一个 Echidna 版本中包含。
| 描述 | 问题 | 状态 |
| :--- | :---: | :--- |
| 对 Vyper 的支持有限 | [#652](https://github.com/crytic/echidna/issues/652) | *wont fix* |
| 测试的库支持有限 | [#651](https://github.com/crytic/echidna/issues/651) | *wont fix* |
## 安装
### 预编译二进制文件
在开始之前，请确保已安装 Slither (`pip3 install slither-analyzer --user`)。
如果你想在 Linux 或 MacOS 上快速测试 Echidna，我们提供了在 Ubuntu 上构建的静态链接 Linux 二进制文件，以及 mostly static 的 MacOS 二进制文件，地址在我们的 [releases 页面](https://github.com/crytic/echidna/releases)。你也可以从我们的 [CI 流水线](https://github.com/crytic/echidna/actions?query=workflow%3ACI+branch%3Amaster+event%3Apush) 获取相同类型的二进制文件，只需点击提交即可找到适用于 Linux 或 MacOS 的二进制文件。
### Homebrew（macOS / Linux）
如果你的 Mac 或 Linux 机器上安装了 Homebrew，你可以通过运行 ` install echidna` 来安装 Echidna 及其所有依赖项（Slither、crytic-compile）。
你也可以通过运行 `brew install --HEAD echidna` 来编译和安装最新的 `master` 分支代码。
你可以在 [`echidna` Homebrew Formula](https://formulae.brew.sh/formula/echidna) 页面获取更多信息。该公式本身由 [homebrew-core 仓库](https://github.com/Homebrew/homebrew-core/blob/HEAD/Formula/echidna.rb) 维护。
### Docker 容器
如果你更喜欢使用预构建的 Docker 容器，请查看我们的 [docker package](https://github.com/orgs/crytic/packages?repo_name=echidna)，它通过 GitHub Actions 自动构建。`echidna` 容器基于 `ubuntu:focal`，旨在成为一个体积小但足够灵活的镜像，用于在 Echidna 上进行测试。它提供了预构建的 `echidna` 版本，以及 `slither`、`crytic-compile`、`solc-select` 和 `nvm`（版本低于 200 MB）。
请注意，容器镜像目前仅在 x86 系统上构建。在 ARM 设备（如 Mac M1 系统）上运行由于 CPU 模拟导致的性能损失，不建议运行。
可用的标签包括：
| 标签 | 构建标识 |
|------|----------|
| `vx.y.z` | 对应于发布版本 `vx.y.z` 的构建 |
| `latest` | 最新的 Echidna 标记版本 |
| `edge` | 默认分支的最新提交 |
| `testing-foo` | 基于 `foo` 分支的测试构建 |
要以交互方式运行最新版本的 Echidna 容器，可以使用如下命令。它会将当前目录映射到容器内的 `/src`，并提供一个 shell，你可以在其中使用 `echidna`：
```
$ docker run --rm -it -v `pwd`:/src ghcr.io/crytic/echidna/echidna
```
否则，如果你想本地构建最新版本的 Echidna，我们推荐使用 Docker。在该仓库的克隆版本中，运行以下命令来构建 Docker 容器镜像：
```
$ docker build -t echidna -f docker/Dockerfile --target final-ubuntu .
```
然后，你可以本地运行 `echidna` 镜像。例如，要安装 solc 0.5.7 并检查 `tests/solidity/basic/flags.sol`，你可以运行：
```
$ docker run -it -v `pwd`:/src echidna bash -c "solc-select install 0.5.7 && solc-select use 0.5.7 && echidna /src/tests/solidity/basic/flags.sol"
```
### 使用 Stack 构建
如果你更喜欢从源代码构建，请使用 [Stack](https://docs.haskellstack.org/en/stable/README/)。`stack install` 应该会在 `~/.local/bin` 中构建并编译 `echidna`。你需要链接 libreadline 和 libsecp256k1（使用恢复功能构建），这些应该可以通过你选择的软件包管理器安装。还需要安装最新版本的 [libff](https://github.com/scipr-lab/libff)。请参考我们的 [CI 测试](.github/scripts/install-libff.sh) 获取指导。
某些 Linux 发行版不会为 Haskell 所需的内容提供静态库，例如 Arch Linux，这会导致 `stack build` 因链接错误而失败，因为我们使用了 `-static` 标志。在这种情况下，使用 `--flag echidna:-static` 来生成动态链接的二进制文件。
如果你在构建相关链接时遇到错误，可以尝试调整 `--extra-include-dirs` 和 `--extra-lib-dirs`。
### 使用 Nix（在 Apple M1 系统上原生工作）
[Nix 用户](https://nixos.org/download.html) 可以通过以下方式安装最新版本的 Echidna：
```
$ nix-env -i -f https://github.com/crytic/echidna/tarball/master
```
启用 flakes 后，你可以直接从该仓库运行 Echidna：
```
$ nix run github:crytic/echidna # master
$ nix run github:crytic/echidna/v2.1.1 # specific ref (tag/branch/commit)
```
要为非 Nix 的 macOS 系统构建独立发行版，可以使用以下命令将 Echidna 和所有链接的 dylibs 打包：
```
$ nix build .#echidna-bundle
```
Nix 会自动安装开发所需的所有依赖项，包括 `crytic-compile` 和 `solc`。快速开始开发 Echidna 的方式如下：
```
$ git clone https://github.com/crytic/echidna
$ cd echidna
$ nix develop # alternatively nix-shell
[nix-shell]$ cabal run echidna
[nix-shell]$ cabal run tests
[nix-shell]$ cabal new-repl
```
## 公开使用 Echidna
### 属性测试套件
以下是一些使用 Echidna 进行测试的智能合约项目：
* [Primitive](https://github.com/primitivefinance/rmm-core/tree/main/contracts/crytic)
* [Uniswap-v3](https://github.com/search?q=org%3AUniswap+echidna&type=commits)
* [Balancer](https://github.com/balancer-labs/balancer-core/tree/master/echidna)
* [MakerDAO vest](https://github.com/makerdao/dss-vest/pull/16)
* [Optimism DAI Bridge](https://github.com/BellwoodStudios/optimism-dai-bridge/blob/master/contracts/test/DaiEchidnaTest.sol)
* [WETH10](https://github.com/WETH10/WETH10/tree/main/contracts/fuzzing)
* [Yield](https://github.com/yieldprotocol/fyDai/pull/312)
* [Convexity Protocol](https://github.com/opynfinance/ConvexityProtocol/tree/dev/contracts/echidna)
* [Aragon Staking](https://github.com/aragon/staking/blob/82bf54a3e11ec4e50d470d66048a2dd3154f940b/packages/protocol/contracts/test/lib/EchidnaStaking.sol)
* [Centre Token](https://github.com/centrehq/centre-tokens/tree/master/echidna_tests)
* [Tokencard](https://github.com/tokencard/contracts/tree/master/tools/echidna)
* [Minimalist USD Stablecoin](https://github.com/usmfum/USM/pull/41)
### 奖杯
以下是通过 Echidna 发现的安全漏洞。如果你在使用我们的工具时发现安全漏洞，请提交一个包含相关信息的 PR。
| 项目 | 漏洞 | 日期 |
|------|------|------|
| [0x Protocol](https://github.com/trailofbits/publications/blob/master/reviews/0x-protocol.pdf) | 如果订单无法填充，则无法取消 | 2019 年 10 月 |
| [0x Protocol](https://github.com/trailofbits/publications/blob/master/reviews/0x-protocol.pdf) | 如果订单可以部分填充为零，则可以部分填充为一个 token | 2019 年 10 月 |
| [0x Protocol](https://github.com/trailofbits/publications/blob/master/reviews/0x-protocol.pdf) | cobbdouglas 函数在使用有效输入参数时不会 revert | 2019 年 10 月 |
| [Balancer Core](https://github.com/trailofbits/publications/blob/master/reviews/BalancerCore.pdf) | 攻击者无法从公共池中窃取资产 | 2020 年 1 月 |
| [Balancer Core](https://github.com/trailofbits/publications/blob/master/reviews/BalancerCore.pdf) | 攻击者无法通过 joinPool 生成免费 pool token | 2020 年 1 月 |
| [Balancer Core](https://github.com/trailofbits/publications/blob/master/reviews/BalancerCore.pdf) | 调用 joinPool-exitPool 不会导致免费 pool token | 2020 年 1 月 |
| [Balancer Core](https://github.com/trailofbits/publications/blob/master/reviews/BalancerCore.pdf) | 调用 exitswapExternAmountOut 不会导致免费资产 | 2020 年 1 月 |
| [Liquity Dollar](https://github.com/trailofbits/publications/blob/master/reviews/Liquity.pdf) | [关闭金库需要持有全部 LUSD 抵押](https://github.com/liquity/dev/blob/echidna_ToB_final/packages/contracts/contracts/TestContracts/E2E.sol#L242-L298) | 2020 年 12 月 |
| [Liquity Dollar](https://github.com/trailofbits/publications/blob/master/reviews/Liquity.pdf) | [金库可能被不当移除](https://github.com/liquity/dev/blob/echidna_ToB_final/packages/contracts/contracts/TestContracts/E2E.sol#L242-L298) | 2020 年 12 月 |
| [Liquity Dollar](https://github.com/trailofbits/publications/blob/master/reviews/Liquity.pdf) | 初始赎回可能意外 revert | 2020 年 12 月 |
| [Liquity Dollar](https://github.com/trailofbits/publications/blob/master/reviews/Liquity.pdf) | 无赎回操作的赎回可能仍返回成功 | 2020 年 12 月 |
| [Origin Dollar](https://github.com/trailofbits/publications/blob/master/reviews/OriginDollar.pdf) | 允许用户转移的 token 超过其持有量 | 2020 年 11 月 |
| [Origin Dollar](https://github.com/trailofbits/publications/blob/master/reviews/OriginDollar.pdf) | 用户余额可能大于总供应量 | 2020 年 11 月 |
| [Yield Protocol](https://github.com/trailofbits/publications/blob/master/reviews/YieldProtocol.pdf) | 买卖 token 的算术计算不精确 | 2020 年 8 月 |
### 研究
我们也可以使用 Echidna 来重现智能合约模糊测试论文中的研究示例，以展示其发现解决方案的速度有多快。所有这些都可以在几秒钟到一两分钟内在笔记本电脑上解决。
| 来源 | 代码 |
|------|------|
| [使用自动分析工具与 MakerDAO 合约](https://forum.openzeppelin.com/t/using-automatic-analysis-tools-with-makerdao-contracts/1021) | [SimpleDSChief](https://github.com/crytic/echidna/blob/master/tests/solidity/research/vera_dschief.sol) |
| [Sigma Prime 中的整数精度错误](https://github.com/b-mueller/sabre#example-2-integer-precision-bug) | [VerifyFunWithNumbers](https://github.com/crytic/echidna/blob/master/tests/solidity/research/solcfuzz_funwithnumbers.sol) |
| [使用符号执行的应用到智能合约的模糊学习](https://files.sri.inf.ethz.ch/website/papers/ccs19-ilf.pdf) | [Crowdsale](https://github.com/crytic/echidna/blob/master/tests/solidity/research/ilf_crowdsale.sol) |
| [Harvey: 智能合约的灰盒模糊器](https://arxiv.org/abs/1905.06944) | [Foo](https://github.com/crytic/echidna/blob/master/test/solidity/research/harvey_foo.sol), [Baz](https://github.com/crytic/echidna/blob/master/tests/solidity/research/harvey_baz.sol) |
### 学术出版物
| 论文标题 | 会议 | 出版日期 |
|----------|------|----------|
| [echidna-parade: 多样化的多核智能合约模糊测试](https://agroce.github.io/issta21.pdf) | [ISSTA 2021](https://conf.researchr.org/home/issta-2021) | 2021 年 7 月 |
| [Echidna 高效、易用且快速的智能合约模糊测试](https://agroce.github.io/issta20.pdf) | [ISSTA 2020](https://conf.researchr.org/home/issta-2020) | 2020 年 7 月 |
| [Echidna: 实用的智能合约模糊测试器](papers/echidna_fc_poster.pdf) | [FC 2020](https://fc20.ifca.ai/program.html) | 2020 年 2 月 |
如果你在学术工作中使用 Echidna，请考虑申请 [Crytic $10k 研究奖](https://blog.trailofbits.com/2019/11/13/announcing-the-crytic-10k-research-prize/)。
## 获取帮助
欢迎来到我们的 #ethereum Slack 频道（[Empire Hacking](https://slack.empirehacking.nyc/)），获取使用或扩展 Echidna 的帮助。
* 从查看这些简单的 [Echidna 不变式](tests/solidity/basic/flags.sol) 开始
* 考虑[直接邮件](mailto:echidna-dev@trailofbits.com)给 Echidna 开发团队以获取更详细的问题
## 许可证
Echidna 在 [AGPLv3 许可证](https://github.com/crytic/echidna/blob/master/LICENSE) 下授权和分发。
Echidna 是一种会吃掉错误并且高度电敏感的生物（感谢 Jacob Stanley）
更严肃地说，Echidna 是一个用于模糊测试/基于属性的测试以太坊智能合约的 Haskell 程序。它使用基于[合约 ABI](https://solidity.readthedocs.io/en/develop/abi-spec.html) 的复杂语法模糊测试活动来发现用户定义的谓词或[Solidity 断言](https://solidity.readthedocs.io/en/develop/control-structures.html#id4) 中的问题。我们设计 Echidna 时考虑了模块化，因此可以轻松扩展以包含新的变异或针对特定合约进行测试。
## 功能
* 生成针对实际代码的输入
* 可选的语料库收集、变异和覆盖率引导，以发现更深层次的错误
* 通过 [Slither](https://github.com/crytic/slither) 在模糊测试活动前提取有用信息
* 源代码集成以识别模糊测试后哪些行被覆盖
* 交互式终端 UI，仅文本或 JSON 输出
* 自动测试用例最小化以快速分类
* 无缝集成到开发工作流程中
* 模糊测试活动的最大 gas 使用报告
* 支持使用 [Etheno](https://github.com/crytic/etheno) 和 Truffle 进行复杂的合约初始化
.. 以及一个精美的高分辨率手工制作 logo。
## 用法
### 执行测试运行器
Echidna 的核心功能是一个名为 `echidna` 的可执行文件，它接收一个合约和一个不变式列表（应始终保持为真的属性）作为输入。对于每个不变式，它会生成随机调用序列并检查不变式是否成立。如果能找到某种方式来证明该不变式不成立，它会打印出导致不成立的调用序列。如果找不到，则表明合约是安全的。
### 编写不变式
不变式表示为 Solidity 函数，函数名以 `echidna_` 开头，没有参数，并返回布尔值。例如，如果你有一个 `balance` 变量永远不应低于 `20`，你可以在合约中编写如下额外函数：
```
function echidna_check_balance() public returns (bool) {
return(balance >= 20);
}
```
要检查这些不变式，运行：
```
$ echidna myContract.sol
```
一个包含测试的示例合约可以在 [tests/solidity/basic/flags.sol](tests/solidity/basic/flags.sol) 中找到。要运行它，你应该执行：
```
$ echidna tests/solidity/basic/flags.sol
```
Echidna 应该能找到使 `echidna_sometimesfalse` 不成立的调用序列，并且应该无法找到使 `echidna_alwaystrue` 不成立的输入。
### 收集和可视化覆盖率
完成活动后，Echidna 可以将最大化的 **语料库** 保存到通过 `corpusDir` 配置选项指定的特殊目录中。该目录将包含两个条目：(1) 一个名为 `coverage` 的目录，其中包含可由 Echidna 重放的 JSON 文件；(2) 一个名为 `covered.txt` 的纯文本文件，即带有覆盖率注释的源代码副本。
如果你运行 `tests/solidity/basic/flags.sol` 示例，Echidna 将在 `coverage` 目录中保存一些序列化交易文件，并生成名为 `covered.$(date +%s).txt` 的文件，内容如下：
```
*r | function set0(int val) public returns (bool){
* | if (val % 100 == 0)
* | flag0 = false;
}
*r | function set1(int val) public returns (bool){
* | if (val % 10 == 0 && !flag0)
* | flag1 = false;
}
```
我们的工具使用以下“行标记”对语料库中的每个执行跟踪进行标记：
* `*` 如果执行以 STOP 结束
* `r` 如果执行以 REVERT 结束
* `o` 如果执行因耗尽 gas 而结束
* `e` 如果执行因任何其他错误（零除、断言失败等）而结束
### 支持智能合约构建系统
Echidna 可以测试使用不同智能合约构建系统编译的合约，包括 [Truffle](https://truffleframework.com/) 或 [hardhat](https://hardhat.org/)，通过 [crytic-compile](https://github.com/crytic/crytic-compile)。要使用当前构建框架调用 echidna，请使用 `echidna .`。
除此之外，Echidna 支持两种测试复杂合约的模式。首先，可以[使用 Truffle 和 Etheno 描述初始化过程](https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/end-to-end-testing.md)，并将其作为 Echidna 的基础状态。其次，Echidna 可以通过在 CLI 中传递相应的 Solidity 源代码来调用任何具有已知 ABI 的合约。使用 `allContracts: true` 在配置中开启此功能。
### Echidna 速成课程
我们的 [构建安全智能合约](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna#echidna-tutorial) 仓库包含 Echidna 的速成课程，包括示例、课程和练习。
### 在 GitHub Actions 工作流中使用 Echidna
有一个 Echidna 操作，可以用于在
GitHub Actions 工作流中运行 `echidna`。请参考
[crytic/echidna-action](https://github.com/crytic/echidna-action) 仓库获取
使用说明和示例。
### 配置选项
Echidna 的 CLI 可用于选择要测试的合约并加载配置文件。
```
$ echidna contract.sol --contract TEST --config config.yaml
```
配置文件允许用户选择 EVM 和测试生成参数。一个带有默认选项的完整且带注释的配置文件示例可以在
[tests/solidity/basic/default.yaml](tests/solidity/basic/default.yaml) 找到。
有关配置选项的更多详细信息，请查阅我们的
[维基](https://github.com/trailofbits/echidna/wiki/Config)。
Echidna 支持三种不同的输出驱动程序。默认的 `text` 驱动程序、`json` 驱动程序，以及应抑制所有 `stdout` 输出的 `none` 驱动程序。JSON 驱动程序按如下方式报告整体活动：
```
Campaign = {
"success" : bool,
"error" : string?,
"tests" : [Test],
"seed" : number,
"coverage" : Coverage,
"gas_info" : [GasInfo]
}
Test = {
"contract" : string,
"name" : string,
"status" : string,
"error" : string?,
"testType" : string,
"transactions" : [Transaction]?
}
Transaction = {
"contract" : string,
"function" : string,
"arguments" : [string]?,
"gas" : number,
"gasprice" : number
}
```
`Coverage` 是一个描述某些覆盖率增加调用的字典。
每个 `GasInfo` 条目是一个元组，描述了如何实现最大 gas 使用情况，并且这些接口目前不太重要。这些接口将在未来变得更易于用户使用。`testType` 将是 `property` 或 `assertion`，`status` 始终为 `fuzzing`、`shrinking`、`solved`、`passed` 或 `error`。
### 调试性能问题
诊断 Echidna 性能问题的一种方法是使用性能分析运行 `echidna`。
要使用基本性能分析运行 Echidna，请在原始 `echidna` 命令中添加 `+RTS -p -s`：
```
$ nix develop # alternatively nix-shell
$ cabal --enable-profiling run echidna -- ... +RTS -p -s
$ less echidna.prof
```
这将生成一个报告文件 (`echidna.prof`)，显示哪些函数占用了最多的 CPU 和内存。
如果基本性能分析没有帮助，可以使用更多[高级性能分析技术](https://input-output-hk.github.io/hs-opt-handbook.github.io/src/Measurement_Observation/Heap_Ghc/eventlog.html)。
我们观察到的性能问题的常见原因包括：
- 在热路径中调用的昂贵函数
- 积累 thunk 的惰性数据构造函数
- 热路径中使用的低效数据结构
检查这些是很好的起点。如果你怀疑某些计算过于懒惰并导致内存泄漏，可以使用 `force` 从 `Control.DeepSeq` 来确保它被求值。
## 限制和已知问题
EVM 模拟和测试很难。Echidna 在最新版本中存在一些限制。其中一些是从 [hevm](https://github.com/ethereum/hevm) 继承的，而另一些则是由于设计/性能决策或代码中的简单错误。我们在此列出这些问题及其对应的 issue 和状态（“wont fix”、“on hold”、“in review”、“fixed”。“fixed” 的问题预计将在下一个 Echidna 版本中包含。
| 描述 | 问题 | 状态 |
| :--- | :---: | :--- |
| 对 Vyper 的支持有限 | [#652](https://github.com/crytic/echidna/issues/652) | *wont fix* |
| 测试的库支持有限 | [#651](https://github.com/crytic/echidna/issues/651) | *wont fix* |
## 安装
### 预编译二进制文件
在开始之前，请确保已安装 Slither (`pip3 install slither-analyzer --user`)。
如果你想在 Linux 或 MacOS 上快速测试 Echidna，我们提供了在 Ubuntu 上构建的静态链接 Linux 二进制文件，以及 mostly static 的 MacOS 二进制文件，地址在我们的 [releases 页面](https://github.com/crytic/echidna/releases)。你也可以从我们的 [CI 流水线](https://github.com/crytic/echidna/actions?query=workflow%3ACI+branch%3Amaster+event%3Apush) 获取相同类型的二进制文件，只需点击提交即可找到适用于 Linux 或 MacOS 的二进制文件。
### Homebrew（macOS / Linux）
如果你的 Mac 或 Linux 机器上安装了 Homebrew，你可以通过运行 ` install echidna` 来安装 Echidna 及其所有依赖项（Slither、crytic-compile）。
你也可以通过运行 `brew install --HEAD echidna` 来编译和安装最新的 `master` 分支代码。
你可以在 [`echidna` Homebrew Formula](https://formulae.brew.sh/formula/echidna) 页面获取更多信息。该公式本身由 [homebrew-core 仓库](https://github.com/Homebrew/homebrew-core/blob/HEAD/Formula/echidna.rb) 维护。
### Docker 容器
如果你更喜欢使用预构建的 Docker 容器，请查看我们的 [docker package](https://github.com/orgs/crytic/packages?repo_name=echidna)，它通过 GitHub Actions 自动构建。`echidna` 容器基于 `ubuntu:focal`，旨在成为一个体积小但足够灵活的镜像，用于在 Echidna 上进行测试。它提供了预构建的 `echidna` 版本，以及 `slither`、`crytic-compile`、`solc-select` 和 `nvm`（版本低于 200 MB）。
请注意，容器镜像目前仅在 x86 系统上构建。在 ARM 设备（如 Mac M1 系统）上运行由于 CPU 模拟导致的性能损失，不建议运行。
可用的标签包括：
| 标签 | 构建标识 |
|------|----------|
| `vx.y.z` | 对应于发布版本 `vx.y.z` 的构建 |
| `latest` | 最新的 Echidna 标记版本 |
| `edge` | 默认分支的最新提交 |
| `testing-foo` | 基于 `foo` 分支的测试构建 |
要以交互方式运行最新版本的 Echidna 容器，可以使用如下命令。它会将当前目录映射到容器内的 `/src`，并提供一个 shell，你可以在其中使用 `echidna`：
```
$ docker run --rm -it -v `pwd`:/src ghcr.io/crytic/echidna/echidna
```
否则，如果你想本地构建最新版本的 Echidna，我们推荐使用 Docker。在该仓库的克隆版本中，运行以下命令来构建 Docker 容器镜像：
```
$ docker build -t echidna -f docker/Dockerfile --target final-ubuntu .
```
然后，你可以本地运行 `echidna` 镜像。例如，要安装 solc 0.5.7 并检查 `tests/solidity/basic/flags.sol`，你可以运行：
```
$ docker run -it -v `pwd`:/src echidna bash -c "solc-select install 0.5.7 && solc-select use 0.5.7 && echidna /src/tests/solidity/basic/flags.sol"
```
### 使用 Stack 构建
如果你更喜欢从源代码构建，请使用 [Stack](https://docs.haskellstack.org/en/stable/README/)。`stack install` 应该会在 `~/.local/bin` 中构建并编译 `echidna`。你需要链接 libreadline 和 libsecp256k1（使用恢复功能构建），这些应该可以通过你选择的软件包管理器安装。还需要安装最新版本的 [libff](https://github.com/scipr-lab/libff)。请参考我们的 [CI 测试](.github/scripts/install-libff.sh) 获取指导。
某些 Linux 发行版不会为 Haskell 所需的内容提供静态库，例如 Arch Linux，这会导致 `stack build` 因链接错误而失败，因为我们使用了 `-static` 标志。在这种情况下，使用 `--flag echidna:-static` 来生成动态链接的二进制文件。
如果你在构建相关链接时遇到错误，可以尝试调整 `--extra-include-dirs` 和 `--extra-lib-dirs`。
### 使用 Nix（在 Apple M1 系统上原生工作）
[Nix 用户](https://nixos.org/download.html) 可以通过以下方式安装最新版本的 Echidna：
```
$ nix-env -i -f https://github.com/crytic/echidna/tarball/master
```
启用 flakes 后，你可以直接从该仓库运行 Echidna：
```
$ nix run github:crytic/echidna # master
$ nix run github:crytic/echidna/v2.1.1 # specific ref (tag/branch/commit)
```
要为非 Nix 的 macOS 系统构建独立发行版，可以使用以下命令将 Echidna 和所有链接的 dylibs 打包：
```
$ nix build .#echidna-bundle
```
Nix 会自动安装开发所需的所有依赖项，包括 `crytic-compile` 和 `solc`。快速开始开发 Echidna 的方式如下：
```
$ git clone https://github.com/crytic/echidna
$ cd echidna
$ nix develop # alternatively nix-shell
[nix-shell]$ cabal run echidna
[nix-shell]$ cabal run tests
[nix-shell]$ cabal new-repl
```
## 公开使用 Echidna
### 属性测试套件
以下是一些使用 Echidna 进行测试的智能合约项目：
* [Primitive](https://github.com/primitivefinance/rmm-core/tree/main/contracts/crytic)
* [Uniswap-v3](https://github.com/search?q=org%3AUniswap+echidna&type=commits)
* [Balancer](https://github.com/balancer-labs/balancer-core/tree/master/echidna)
* [MakerDAO vest](https://github.com/makerdao/dss-vest/pull/16)
* [Optimism DAI Bridge](https://github.com/BellwoodStudios/optimism-dai-bridge/blob/master/contracts/test/DaiEchidnaTest.sol)
* [WETH10](https://github.com/WETH10/WETH10/tree/main/contracts/fuzzing)
* [Yield](https://github.com/yieldprotocol/fyDai/pull/312)
* [Convexity Protocol](https://github.com/opynfinance/ConvexityProtocol/tree/dev/contracts/echidna)
* [Aragon Staking](https://github.com/aragon/staking/blob/82bf54a3e11ec4e50d470d66048a2dd3154f940b/packages/protocol/contracts/test/lib/EchidnaStaking.sol)
* [Centre Token](https://github.com/centrehq/centre-tokens/tree/master/echidna_tests)
* [Tokencard](https://github.com/tokencard/contracts/tree/master/tools/echidna)
* [Minimalist USD Stablecoin](https://github.com/usmfum/USM/pull/41)
### 奖杯
以下是通过 Echidna 发现的安全漏洞。如果你在使用我们的工具时发现安全漏洞，请提交一个包含相关信息的 PR。
| 项目 | 漏洞 | 日期 |
|------|------|------|
| [0x Protocol](https://github.com/trailofbits/publications/blob/master/reviews/0x-protocol.pdf) | 如果订单无法填充，则无法取消 | 2019 年 10 月 |
| [0x Protocol](https://github.com/trailofbits/publications/blob/master/reviews/0x-protocol.pdf) | 如果订单可以部分填充为零，则可以部分填充为一个 token | 2019 年 10 月 |
| [0x Protocol](https://github.com/trailofbits/publications/blob/master/reviews/0x-protocol.pdf) | cobbdouglas 函数在使用有效输入参数时不会 revert | 2019 年 10 月 |
| [Balancer Core](https://github.com/trailofbits/publications/blob/master/reviews/BalancerCore.pdf) | 攻击者无法从公共池中窃取资产 | 2020 年 1 月 |
| [Balancer Core](https://github.com/trailofbits/publications/blob/master/reviews/BalancerCore.pdf) | 攻击者无法通过 joinPool 生成免费 pool token | 2020 年 1 月 |
| [Balancer Core](https://github.com/trailofbits/publications/blob/master/reviews/BalancerCore.pdf) | 调用 joinPool-exitPool 不会导致免费 pool token | 2020 年 1 月 |
| [Balancer Core](https://github.com/trailofbits/publications/blob/master/reviews/BalancerCore.pdf) | 调用 exitswapExternAmountOut 不会导致免费资产 | 2020 年 1 月 |
| [Liquity Dollar](https://github.com/trailofbits/publications/blob/master/reviews/Liquity.pdf) | [关闭金库需要持有全部 LUSD 抵押](https://github.com/liquity/dev/blob/echidna_ToB_final/packages/contracts/contracts/TestContracts/E2E.sol#L242-L298) | 2020 年 12 月 |
| [Liquity Dollar](https://github.com/trailofbits/publications/blob/master/reviews/Liquity.pdf) | [金库可能被不当移除](https://github.com/liquity/dev/blob/echidna_ToB_final/packages/contracts/contracts/TestContracts/E2E.sol#L242-L298) | 2020 年 12 月 |
| [Liquity Dollar](https://github.com/trailofbits/publications/blob/master/reviews/Liquity.pdf) | 初始赎回可能意外 revert | 2020 年 12 月 |
| [Liquity Dollar](https://github.com/trailofbits/publications/blob/master/reviews/Liquity.pdf) | 无赎回操作的赎回可能仍返回成功 | 2020 年 12 月 |
| [Origin Dollar](https://github.com/trailofbits/publications/blob/master/reviews/OriginDollar.pdf) | 允许用户转移的 token 超过其持有量 | 2020 年 11 月 |
| [Origin Dollar](https://github.com/trailofbits/publications/blob/master/reviews/OriginDollar.pdf) | 用户余额可能大于总供应量 | 2020 年 11 月 |
| [Yield Protocol](https://github.com/trailofbits/publications/blob/master/reviews/YieldProtocol.pdf) | 买卖 token 的算术计算不精确 | 2020 年 8 月 |
### 研究
我们也可以使用 Echidna 来重现智能合约模糊测试论文中的研究示例，以展示其发现解决方案的速度有多快。所有这些都可以在几秒钟到一两分钟内在笔记本电脑上解决。
| 来源 | 代码 |
|------|------|
| [使用自动分析工具与 MakerDAO 合约](https://forum.openzeppelin.com/t/using-automatic-analysis-tools-with-makerdao-contracts/1021) | [SimpleDSChief](https://github.com/crytic/echidna/blob/master/tests/solidity/research/vera_dschief.sol) |
| [Sigma Prime 中的整数精度错误](https://github.com/b-mueller/sabre#example-2-integer-precision-bug) | [VerifyFunWithNumbers](https://github.com/crytic/echidna/blob/master/tests/solidity/research/solcfuzz_funwithnumbers.sol) |
| [使用符号执行的应用到智能合约的模糊学习](https://files.sri.inf.ethz.ch/website/papers/ccs19-ilf.pdf) | [Crowdsale](https://github.com/crytic/echidna/blob/master/tests/solidity/research/ilf_crowdsale.sol) |
| [Harvey: 智能合约的灰盒模糊器](https://arxiv.org/abs/1905.06944) | [Foo](https://github.com/crytic/echidna/blob/master/test/solidity/research/harvey_foo.sol), [Baz](https://github.com/crytic/echidna/blob/master/tests/solidity/research/harvey_baz.sol) |
### 学术出版物
| 论文标题 | 会议 | 出版日期 |
|----------|------|----------|
| [echidna-parade: 多样化的多核智能合约模糊测试](https://agroce.github.io/issta21.pdf) | [ISSTA 2021](https://conf.researchr.org/home/issta-2021) | 2021 年 7 月 |
| [Echidna 高效、易用且快速的智能合约模糊测试](https://agroce.github.io/issta20.pdf) | [ISSTA 2020](https://conf.researchr.org/home/issta-2020) | 2020 年 7 月 |
| [Echidna: 实用的智能合约模糊测试器](papers/echidna_fc_poster.pdf) | [FC 2020](https://fc20.ifca.ai/program.html) | 2020 年 2 月 |
如果你在学术工作中使用 Echidna，请考虑申请 [Crytic $10k 研究奖](https://blog.trailofbits.com/2019/11/13/announcing-the-crytic-10k-research-prize/)。
## 获取帮助
欢迎来到我们的 #ethereum Slack 频道（[Empire Hacking](https://slack.empirehacking.nyc/)），获取使用或扩展 Echidna 的帮助。
* 从查看这些简单的 [Echidna 不变式](tests/solidity/basic/flags.sol) 开始
* 考虑[直接邮件](mailto:echidna-dev@trailofbits.com)给 Echidna 开发团队以获取更详细的问题
## 许可证
Echidna 在 [AGPLv3 许可证](https://github.com/crytic/echidna/blob/master/LICENSE) 下授权和分发。标签：ABI, CI, Echidna, Etheno, Gas 优化, Haskell, JSON 输出, Slither, Truffle, 以太坊, 区块链安全, 区块链测试工具, 合约变体, 安全测试, 属性测试, 形式化验证, 攻击性安全, 智能合约, 智能合约审计, 最小化测试用例, 模糊测试框架, 源码集成, 终端界面, 覆盖率分析, 覆盖率引导, 语料库收集, 高分辨率Logo