
Echidna 是一种奇怪的生物,它以虫子为食,并且对电高度敏感(向 Jacob Stanley 致歉)
更严肃地说,Echidna 是一个 Haskell 程序,专为以太坊智能合约的模糊测试/基于属性的测试而设计。它基于合约 ABI 使用复杂的基于语法的模糊测试活动,来证伪用户定义的谓词或 Solidity 断言。我们在设计 Echidna 时充分考虑了模块化,因此可以轻松扩展以包含新的变异方式,或在特定情况下测试特定合约。
.. 以及一个精美的高分辨率手工制作标志。
Echidna 的核心功能是一个名为 echidna 的可执行文件,它接收一个合约和一组不变量(应始终保持为真的属性)作为输入。对于每个不变量,它会生成对合约的随机调用序列,并检查该不变量是否成立。如果它能找到某种方式证伪该不变量,就会打印出相应的调用序列。如果找不到,你就可以对合约的安全性有一定的信心。
不变量以 Solidity 函数的形式表达,其名称以 echidna_ 开头,没有参数,并返回一个布尔值。例如,如果你有一个 balance 变量,它永远不应低于 20,你可以在合约中编写一个额外的函数,如下所示:```solidity
function echidna_check_balance() public returns (bool) {
return(balance >= 20);
}
要检查这些不变量,请运行:```sh
$ echidna myContract.sol
一个带有测试的示例合约可以在 tests/solidity/basic/flags.sol 中找到。要运行它,你应该执行:```sh $ echidna tests/solidity/basic/flags.sol
Echidna 应找到一个能证伪 `echidna_sometimesfalse` 的调用序列,并且应无法为 `echidna_alwaystrue` 找到证伪输入。
### 测试模式
上面的示例使用默认的 **property** 模式,但 Echidna 支持多种测试模式,可通过配置文件中的 `testMode` 或命令行上的 `--test-mode` 进行配置:
* **`property`**(默认):测试以 `echidna_` 为前缀且返回 `bool` 的函数。
* **`assertion`**:检测来自 `assert()` 和 Foundry 的 `assertX` 辅助函数(`assertTrue`、`assertEq` 等)的断言失败。
* **`foundry`**:运行 Foundry 风格的测试,遵循其命名约定:以 `test` 为前缀的单元测试和模糊测试(以 `testFail` 为前缀的测试预期会回滚),以及以 `invariant` 或 `statefulFuzz` 为前缀的状态不变量。以 `check` 和 `prove` 为前缀的函数是符号入口点,但由于此模式是模糊测试活动,它们会像其他测试函数一样被模糊测试。
* **`verification`**:使用单笔交易对合约的每个函数进行符号验证。以 `check` 和 `prove` 为前缀的函数始终用作入口点。
* **`overflow`**:检测整数上溢/下溢(Solidity >= 0.8.0)。
* **`optimization`**:最大化以 `echidna_` 为前缀且返回 `int256` 的函数的返回值(使用与 property 模式相同的可配置前缀)。
* **`exploration`**:在不检查属性的情况下收集覆盖率。
### 收集和可视化覆盖率
完成一次活动后,Echidna 可以将最大化覆盖率的 **corpus** 保存到由 `corpusDir` 配置选项指定的特殊目录中。该目录将包含两个条目:(1) 一个名为 `coverage` 的目录,其中包含可由 Echidna 重放的 JSON 文件;(2) 一个名为 `covered.txt` 的纯文本文件,即带有覆盖率注释的源代码副本。
如果你运行 `tests/solidity/basic/flags.sol` 示例,Echidna 将在 `coverage` 目录中保存一些序列化交易的几个文件,以及一个包含以下行的 `covered.$(date +%s).txt` 文件:```text
*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 如果执行以 out-of-gas 错误结束e 如果执行以任何其他错误结束(除零、断言失败等)Echidna 可以测试使用不同智能合约构建系统编译的合约,包括 Foundry、Hardhat 和 Truffle,通过 crytic-compile 实现。要使用当前编译框架调用 Echidna,请使用 echidna .。
除此之外,Echidna 支持两种测试复杂合约的模式。首先,可以利用现有网络状态并将其用作 Echidna 的基础状态。其次,Echidna 可以通过在 CLI 中传入相应的 Solidity 源代码来调用任何具有已知 ABI 的合约。在配置中使用 allContracts: true 来开启此功能。
我们的 Building Secure Smart Contracts 仓库包含一个 Echidna 速成课程,包括示例、课程和练习。
有一个 Echidna action 可用于在 GitHub Actions 工作流中运行 echidna。请参阅 crytic/echidna-action 仓库以获取使用说明和示例。
Echidna 的 CLI 可用于选择要测试的合约并加载配置文件。```sh $ echidna contract.sol --contract TEST --config config.yaml
配置文件允许用户选择 EVM 和测试生成参数。一个包含默认选项的完整且带注释的配置文件示例可以在
[tests/solidity/basic/default.yaml](https://github.com/crytic/echidna/blob/master/tests/solidity/basic/default.yaml) 找到。
有关可用配置选项的更详细信息,请参阅[文档](https://secure-contracts.com/program-analysis/echidna/configuration.html)。
Echidna 支持三种不同的输出驱动。有默认的 `text` 驱动、`json` 驱动,以及 `none` 驱动,后者应抑制所有
`stdout` 输出。JSON 驱动按如下方式报告整体活动。```
Campaign = {
"success" : bool,
"error" : string?,
"tests" : [Test],
"seed" : number,
"coverage" : Coverage
}
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 是一个描述某些增加覆盖率的调用的字典。这些接口在以后可能会稍作调整以更加用户友好。testType 将是 property、assertion、optimization、exploration 或 call 之一,而 status 始终取 fuzzing、shrinking、solved、passed 或 error 之一。
诊断 Echidna 性能问题的一种方法是启用性能分析来运行 echidna。
要使用基本性能分析运行 Echidna,请将 +RTS -p -s 添加到您原来的 echidna 命令中:```sh
$ nix develop # alternatively nix-shell
$ cabal --enable-profiling run echidna -- ... +RTS -p -s
$ less echidna.prof
这会生成一个报告文件(`echidna.prof`),显示哪些函数占用了最多的 CPU 和内存使用量。
如果基本性能分析没有帮助,你可以使用更[高级的性能分析技术](https://haskell.foundation/hs-opt-handbook.github.io/src/Measurement_Observation/Haskell_Profiling/eventlog.html)。
我们观察到的性能问题的常见原因:
- 在热路径中调用开销大的函数
- 累积 thunk 的惰性数据构造函数
- 在热路径中使用低效的数据结构
检查这些是一个好的起点。如果你怀疑某些计算过于惰性并泄漏内存,你可以使用 `Control.DeepSeq` 中的 `force` 来确保它被求值。
## 限制和已知问题
EVM 模拟和测试很困难。Echidna 在最新版本中有一些限制。其中一些继承自 [hevm](https://github.com/argotorg/hevm),而另一些则是设计/性能决策的结果,或者仅仅是我们代码中的错误。我们在此列出它们,包括相应的问题和状态(“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 已[安装](https://github.com/crytic/slither)(`pip3 install slither-analyzer --user`)。
如果你想在 Linux 或 MacOS 中快速测试 Echidna,我们在[发布页面](https://github.com/crytic/echidna/releases)上提供了在 Ubuntu 上构建的静态链接 Linux 二进制文件以及大部分静态的 MacOS 二进制文件。你也可以从我们的 [CI 流水线](https://github.com/crytic/echidna/actions?query=workflow%3ACI+branch%3Amaster+event%3Apush)中获取相同类型的二进制文件,只需点击提交即可找到适用于 Linux 或 MacOS 的二进制文件。
### Homebrew(macOS / Linux)
如果你在 Mac 或 Linux 机器上安装了 Homebrew,你可以通过运行 `brew install echidna` 来安装 Echidna 及其所有依赖项(Slither、crytic-compile)。
你也可以通过运行 `brew install --HEAD echidna` 来编译并安装最新的 `master` 分支代码。
你可以在 [`echidna` Homebrew Formula](https://formulae.brew.sh/formula/echidna) 页面获取更多信息。该 formula 本身作为 [homebrew-core 仓库](https://github.com/Homebrew/homebrew-core/blob/HEAD/Formula/e/echidna.rb)的一部分进行维护。
### Docker 容器
如果你更喜欢使用预构建的 Docker 容器,请查看我们的 [docker
包](https://github.com/orgs/crytic/packages?repo_name=echidna),它是
通过 GitHub Actions 自动构建的。`echidna` 容器基于
`ubuntu:noble`,它旨在成为一个体积小但足够灵活的镜像,以便使用
Echidna。它提供了预构建版本的 `echidna`,以及
`slither`、`crytic-compile`、`solc-select`、`nvm` 和 `foundry`(包括
`forge`、`cast`、`anvil` 和 `chisel`),大小在 200 MB 以下。
请注意,容器镜像目前仅在 x86 系统上构建。不建议在
ARM 设备(如 Mac M1 系统)上运行它们,因为 CPU 模拟会导致
性能损失。
Docker 容器镜像有不同的标签可用:
| 标签 | 构建标签
|---------------|-------------
| `vx.y.z` | 对应于发布版本 `vx.y.z` 的构建
| `latest` | 最新的 Echidna 标记发布版本。
| `edge` | 默认分支上的最新提交。
| `testing-foo` | 基于 `foo` 分支的测试构建。