你想知道的关于以太坊智能合约符号执行的一切（但你可能不敢问）
- SaferMaker
- 发布于 2023-05-02 14:11
- 阅读 15
这篇文章系统介绍了符号执行作为一种确保智能合约安全性和正确性的技术，详细阐述了其定义、原理及应用。文章还对多种以太坊智能合约的符号执行工具（如Mythril、Manticore、hevm和EthBMC）进行了对比实验，展示了它们在识别智能合约漏洞方面的优势和局限，并探讨了未来的改进方向。
作者: Palina Tolmach
形式验证技术被广泛认为是一个可靠但复杂的方法，可以严格确保智能合约的安全性和正确性。其中一种技术是符号执行，它允许用户检查程序的执行是否 可能 违反某个属性或到达一个脆弱状态。符号执行最近受到关注，许多工具可用，包括已建立的工具如 Mythril 或 Manticore，以及较新的工具如 Halmos。在这篇博文中，我们将介绍符号执行，并探讨针对以太坊智能合约的现有字节码级符号执行工具。
我们讨论了使用这些工具进行的一些实验，并强调了它们的优点和局限性。我们还提供了方便的shell命令，供你复现每个实验！
这篇文章是关于智能合约符号分析主题的两篇文章中的第一篇。一旦第二部分的符号测试准备就绪，相关链接会在这里出现，请随时回来查看！我们在这篇文章中发布了一个小型的智能合约基准，后续还会发布一个扩展版本。现在，请享受第一部分！
什么是符号执行？
如果你知道这个问题的答案，可以直接跳到 下一部分 :)
定义
符号执行是一种程序分析技术，它同时探索多个执行路径。如果一个程序以 具体 的方式运行，即在特定的 具体 输入上，程序的单个控制流路径将被探索——这就是单元测试执行期间发生的情况。类似地，模糊测试具体地在一组随机（但具体）输入上执行程序。与这些技术相对，符号执行将 符号 值而非具体值分配给输入变量，这决定了应当执行哪些路径。符号值表示可以分配给变量的任意值；换句话说，符号值意味着该变量可以取该类型的变量所能拥有的 任何 值（不考虑程序代码对该变量施加的约束）。
if (x > 5) {
// 符号变量 x 是 _任何_ 大于 5 的整数
} else {
// 符号变量 x 是 _任何_ 小于等于 5 的整数
}因此，符号执行可以被视为一种泛化测试的方法。它通常被用来检查某个属性 能否 被任何程序执行违反，即检查某个脆弱状态是否 可达。
if (balance >= 0) {
...
} else {
// 这应该是不可达的
// 但真的不可达吗？...
}为了确定可达性，符号执行引擎通常依赖于现成的 满足性模块理论 (SMT) 求解器，例如 Z3。可达性等价于某个执行路径的可行性。执行路径由执行流程中的一系列条件定义（例如，包含在 if 语句中的条件）。这些路径条件被转换为逻辑公式，然后交给 SMT 求解器检查其 满足性：这个条件组合是否理论上可以评估为 true。一个 SMT 求解器要么找到一个符号变量的满足性具体赋值，从而证明路径的可行性（例如，输出可能表明"如果 i == 6 && j == 17，则该路径是可行的"）；要么证明一个公式是不可满足的，表明没有满足赋值存在，该路径是不可行的。生成会导致特定路径执行的具体程序输入可以用来自动生成测试用例。
范例中的符号执行
考虑以下智能合约。它是从 Foundry 仓库中的 issue condition not caught by invariant/fuzzer 中包含的代码稍作修改的。代码中通常通过断言明确规定的条件。我们特别关注第 15 行中的断言。我们将函数体包裹在一个 unchecked 块中，以忽略第 8 行可能的下溢（因此我们专注于失败的断言检测）。
pragma solidity ^0.8.17;
contract PostExample {
// https://github.com/foundry-rs/foundry/issues/2851
function backdoor(uint256 x) external pure {
uint256 number = 99;
unchecked {
uint256 z = x - 1;
if (z == 6912213124124531) {
number = 0;
} else {
number = 1;
}
}
assert(number != 0);
}
}合约 PostExample 包含一个以参数 uint256 x 被调用的函数 backdoor。在函数开始时，变量 number 初始化为 99 （第 6 行）。第 8 行初始化另一个变量 z，其值等于 x - 1，这里的 x 是输入参数。根据 z 是否等于 6912213124124531（第 9 行），number 被设置为 0 （第 10 行）或 1（第 12 行）。最后，第 15 行中的断言语句用于检查 number 是否不等于 0（即如果执行了 真实 分支——第 10 行，断言就会被违反）。
如同问题的标题和以下截图所示，Foundry 的模糊测试工具无法识别触发第 9 行条件语句的 真实 分支的输入，即使我们增加了运行次数：
import "forge-std/Test.sol";
import "../src/PostExample.sol";
contract PostExampleTest is Test {
PostExample public example;
function setUp() public {
example = new PostExample();
}
function testBackdoor(uint256 x) public view {
example.backdoor(x);
}
}
另一方面，符号执行在识别可能很难通过其他方式触及的脆弱状态时尤其有用，例如使用测试或黑盒模糊测试。我们来看看如何使用符号执行识别第 15 行的 assert(number != 0) 违反。以下图示说明了逐步符号执行 backdoor 的过程。
对于程序的每个控制流路径，符号执行 引擎 维护（1）一个 路径条件——一个关于变量值的 一阶逻辑 公式，捕获沿该路径所遵循的条件，以及（2）一个 符号内存存储，该存储将变量映射到沿该路径计算出的符号表达式或值。对分支语句的执行更新路径条件，而赋值则更新存储。在初始化状态下，路径约束
π 是 真 的，输入参数 x 被分配一个符号（即任意）值 🤷♀️。当第 6 行中初始化 number 时，符号存储
σ 被用 99 的具体值相关联，从而更新。接下来的路径更新发生在将 z 的值设置为 x - 1 时，其中 x 是输入参数，因而是一个符号变量。
第 9 行的条件分支将进一步执行分成两个子树。当选取 真实 分支时，第 9 行的约束（用符号术语而言）被添加到路径条件中，变为
π= 🤷♀️
−1==6912213124124531。当采取 虚假 分支时，路径条件更新为添加分支条件的 否定 ——例如，如果 z == 6912213... 不成立，则路径条件更新如下：
π=¬( 🤷♀️
−1==6912213124124531)。根据不同的分支，行 10 和 12 分别将变量 number 赋值为 0 或 1，因此更新符号状态。
断言的违反相当于构造为路径条件与被断言表达式的否定的结合的逻辑公式的满足性（如图示底部所示）。在对 backdoor 的两个执行路径解开之后，我们可以得出结论，一个路径确实到达了该公式是可满足的状态。如果执行了第 10 行（将 number 设置为 0），换句话说，如果满足第 9 行的条件（z == 6912213124124531），则断言可以被违反。由于 z 的值是由输入参数 x 导出的， z = x - 1，因此用于确定路径约束的满足性的 SMT 求解器也可以建议具体输入值对应此执行路径：x = 6912213124124531 + 1 = 6912213124124532。符号执行工具产生的输出（它对应于导致断言违反的反例）通常看起来像这一形式：postExample.backdoor(6912213124124532)。
为了说明符号执行过程，请观看电影《下一步》(Next) 中的 Nicolas "Symbolic Execution" Cage 在每个分支点自我分叉以探索所有可能的执行路径并识别一个失败的断言的场景。
以下是我们以前的更详细的符号执行描述和一些练习链接，帮助更好地理解正在发生的事情：
符号执行中的挑战
尽管对各种分析都很有用——在本帖的后续部分将看到——符号执行对所有可能执行路径的穷举探索带来了某些性能和可扩展性限制（的确！）。挑战包括：
- 处理状态空间爆炸（状态数量在系统组件数量上呈指数增长，而探索具有例如循环和递归调用的智能合约可能是不切实际的）
- 约束求解（某些类型的约束对于 SMT 求解器构成困难——包括 DeFi 智能合约中常见的非线性算术表达式，例如 Uniswap 不变式；或任何类型的哈希）
- 与环境的交互（例如，调用其他智能合约并考虑可能的副作用）
- 建模记忆和存储（可以完全符号化、部分符号化，或具体化）
有哪些工具？
符号执行已经被广泛用于实施智能合约的漏洞检测工具，示例包括 Pakala、Oyente、Osiris、HoneyBadger、Maian、teEther。然而，这些工具大多没有维护，支持的 EVM 子集有限，仅限于 Z3 作为求解器，或者有其他限制或缺陷。经过高层次分析和探索性实验，我们选择了以下四种开源 EVM 级符号执行工具进行全面的实证分析：
一个由 Trail of Bits 开发的符号执行工具。Manticore 使用 Python 实现，并支持多种 SMT 求解器（Z3、Yices2、Boolector、cvc4）。Manticore 有几种接口：可以用作命令行工具，通过其 Python API，或使用 manticore-verifier——一个基于属性的符号执行工具。除了漏洞检测之外，Manticore 还自动生成与通过符号执行识别的执行路径对应的测试用例。
一个用于 EVM 字节码的安全分析工具，通过符号执行进行漏洞检测。Mythril 由 ConsenSys 开发。使用 Python 实现，并通过其 Python API 使用 Z3 作为 SMT 求解器。
EVM 字节码的符号执行引擎和等价性检查器。hevm 最初作为 dapptools 框架的一部分开发，由以太坊基金会进行了分叉，当前正在积极开发中——我们在实验中使用的是以太坊基金会的较新分叉。hevm 用 Haskell 实现，并支持 Z3 和 cvc5 作为求解器。
一个基于符号执行的 EVM 字节码 有界模型检验器，由鲁尔大学波鸿开发。EthBMC 是我们列表中唯一的学术工具，在 2020 年的 Usenix Security 上提出了学术论文 [http://www.usenix.org/system/files/sec20-frank.pdf]。EthBMC 的一个独特特性是它使用 geth 对识别的反例进行具体验证。EthBMC 使用 Rust 实现，并支持多种 SMT 求解器（Z3、Yices2、Boolector）。
另外两个相关工具包括 a16z 的新工具 Halmos；和基于 K Framework 构建的 KEVM，由于各种原因这两种工具没有被纳入本文，但它们都执行 符号测试，这是我们下一篇文章的主题，敬请关注 ;)
它们能做什么？
让我们看看这四种工具如何用于分析以太坊智能合约。本帖描述的所有实验均在配备 M1 Max 芯片和 64 GB 内存的 MacBook Pro 上进行。当在 Docker 中运行时（如"跟随"片段中所建议），你可能会看到性能下降，具体取决于分配给你的容器的资源量。
设置
如果你想要跟随我们，可以使用以下命令拉取预构建的 Docker 镜像：
docker pull baolean/manticore:latest
docker pull baolean/mythril:latest
docker pull baolean/ethbmc:latest
docker pull baolean/hevm:latest你可以在 这个 Docker Hub 注册表 中找到这些容器镜像。
用于评估的智能合约可以在 这个仓库 中找到，你可以使用下面的命令将其克隆：
git clone https://github.com/baolean/symexec-bench.git && \
cd symexec-bench && \
git submodule init && git submodule update现在，你可以在容器中运行 Docker 容器，将克隆的 repo 挂载到容器中的 /examples 目录中。
假设你当前的目录（pwd）是克隆的 repo（你在 symexec-bench 文件夹中），命令如下：
docker run -it --rm --platform linux/amd64 \
-v $(pwd):/examples baolean/hevm:latest尝试运行 hevm version 来验证一切正常。要退出容器，键入 exit 然后按回车。感谢 --rm 标志，容器（而不是镜像！）将在退出时自动删除，因此你不需要在后续清理。
我们在这篇文章中检查的所有工具的安装详细步骤可以在 Dockerfiles 中找到：Manticore、Mythril、EthBMC 和 hevm。如果你愿意，可以通过运行
docker build -t IMAGE_NAME .在相应的克隆仓库中从头开始构建镜像，或者直接在你的机器上安装工具。
简单示例
首先，让我们比较我们在介绍中提到的 PostExample 智能合约 中选择的四种工具。除非另有说明，否则这些工具在默认配置下运行——对漏洞检测工具，如 Mythril、Manticore、EthBMC，这意味着启用所有默认检测器。然而在本帖中，我们主要根据工具识别可能失败的 assert 语句的能力进行比较，这通常用于表示始终应满足的条件。失败的断言检测受所有分析工具支持，除了 EthBMC，针对 EthBMC，我们已 自行添加；此外，我们还必须将 geth 使用的以太坊分叉更新为更新版本（伦敦）。Manticore 基于 INVALID 操作码识别失败的断言，因此在与 Manticore 的实验中将 Solidity 的版本设置为 v0.7.6。
使用 Z3 进行符号执行
由于所有四种工具支持 Z3 作为 SMT 求解器，因此作为第一步，我们将所有工具与 Z3 一起运行。符号执行工具的分析通常通过发出一个或多个符号交易进行，即具有符号 calldata 的交易。由于失败的断言可以通过一次函数调用（提供适当的输入）检测，因此在这里，我们将所有工具执行的符号分析限制为一次交易。
Mythril 通过其 myth a 命令执行符号执行，该命令将 Solidity 文件作为输入，在 2.7 秒内识别一个失败的断言及其导致的输入（ backdoor(6912213124124532)）。下面截图所示的输出演示了所识别的反例，以及与发送给 SMT 求解器的查询数量和花费的时间相关的一些补充信息（处理 76 次查询耗时 0.31 秒）。Z3 是唯一被 Mythril 支持的求解器，因此默认使用。
要跟进，请通过运行以下命令进入容器：
docker run -it --rm --platform linux/amd64 \
-v $(pwd):/examples baolean/mythril:latest在容器中运行：
myth a examples/PostExample/PostExample.sol -t1Manticore 的 CLI 也可以将 Solidity 文件作为输入，但是，如前所述，Solidity 的版本须 降级到 0.7.6。 --smt.solver z3 标志确保 Manticore 使用 Z3 作为 SMT 求解器。此外，Manticore 还需使用 --thorough-mode 标志运行，以便报告潜在漏洞（对应于下方截图中的 WARNING: INVALID instruction）。SMT 求解器使用的时间也能在输出中看到（0.13 秒）。
使用 Docker，可以复现如下：
docker run -it --rm --platform linux/amd64 \
-v $(pwd):/examples baolean/manticore:latest
manticore examples/PostExample/PostExample_0.7.sol \
--smt.solver z3 --thorough-mode --txlimit 1Manticore 还会为每个可能的执行路径生成测试用例，以及与分析相关的其他信息（代码覆盖率等）——所有这些都在 1.7 秒内完成！检查其中生成的一个文件显示识别的反例：
Manticore 的其他优点包括分析的灵活性和定制性，例如，不同的 gas 模型、启用或禁用关于符号余额的推理等。关于相应标志的信息可以通过 manticore --help 获取。
与 Manticore 和 Mythril 可以在 Solidity 文件上运行不同的是，接下来的两种工具——hevm 和 EthBMC——则基于智能合约的运行时字节码进行分析。可以通过 Solidity 编译器 solc 使用命令 solc --bin-runtime examples/PostExample/PostExample.sol 生成运行时二进制文件：
hevm 通过 hevm symbolic 对智能合约的二进制文件进行符号分析。hevm 默认使用 Z3，但我们可以通过 --solver z3 显式指示 hevm 使用 Z3：
要复现：
docker run -it --rm --platform linux/amd64 \
-v $(pwd):/examples baolean/hevm:latest
hevm symbolic --code \
$(<examples/PostExample/PostExample.bin-runtime)执行时间少于一秒（甚至少于 0.1 秒！）。然而，输出需要额外解码——截图中的解码输出实际上是 backdoor(6912213124124532)，可以使用可用的 calldata 解码器 验证。读者可以把这作为一个练习；要进行解码，使用编译器生成的 ABI（ solc --abi examples/PostExample/PostExample.sol）和生成的 calldata。
Calldata
0x99d7cd3400000000000000000000000000000000000000000000000000188e9f07e00f74
PostExample ABI
[{"inputs":[{"internalType":"uint256","name":"x","type":"uint256"}],"name":"backdoor","outputs":[],"stateMutability":"pure","type":"function"}]
EthBMC 接受更具体格式的输入——它要求用户提供 配置 YAML 文件，其中包含分析中涉及的所有合约的地址、它们的余额、运行时二进制文件和nonce。初始的存储变量值也可以在该文件中提供——否则它们被假定为该类型的默认值（智能合约的构造函数不被执行或分析，因为它不包含在运行时字节码中，这与 hevm 同样适用）。
当提供此类输入时，EthBMC 4.3 秒内输出一个识别的反例（也需要进行解码）。如上所述，EthBMC 通过在 geth 本地部署的智能合约中对识别的反例进行具体验证，可以避免误报（可以通过 --no-verify 标志关闭具体验证）。
在使用 --solver z3 标志运行时，EthBMC 会使用 Z3。
要复现：
docker run -it --rm --platform linux/amd64 \
-v $(pwd):/examples baolean/ethbmc:latest
ethbmc examples/PostExample/PostExample.yml --solver z3我们的初步评估表明，所有四种分析工具都可以在几秒钟内成功识别出我们示例中的失败断言——这非常好！使用 Z3 作为求解器的五次运行的平均结果如下：
| 工具 | 语言 | 求解器 | 时间 (Z3) |
|---|---|---|---|
| Mythril | Python | Z3 | 2.8 秒 |
| Manticore | Python | Z3、cvc4、Boolector、Yices2 | 1.6 秒 |
| hevm | Haskell | Z3、cvc5 | 0.1 秒 |
| EthBMC | Rust | Z3、Boolector、Yices2 | 3.6 秒 |
不同求解器
虽然进行的分析结果看起来非常令人信服，但让我们看看是否可以通过使用 Z3 以外的 SMT 求解器进一步改善这些结果，因为不同任务所呈现的性能可能会因求解器而异。
确实如此：将 EthBMC 与 Yices2 作为求解器运行后，分析在 0.19 秒完成，这比使用 Z3 所需的 3.6 秒明显减少！
ethbmc examples/PostExample/PostExample.yml \
--solver yicesBoolector 的性能也优于 Z3，使分析在 0.3 秒完成：
ethbmc examples/PostExample/PostExample.yml \
--solver boolector当使用 Yices2 时，Manticore 的执行时间为 2 秒：
manticore examples/PostExample/PostExample_0.7.sol \
--smt.solver yices --thorough-mode --txlimit 1使用 Boolector 时需要 1.6 秒：
manticore examples/PostExample/PostExample_0.7.sol \
--smt.solver boolector --thorough-mode --txlimit 1而 cvc4 需时 4.9 秒 (这可能源于我在 M1 上通过 Rosetta 运行)：
manticore examples/PostExample/PostExample_0.7.sol \
--smt.solver cvc4 --thorough-mode --txlimit 1hevm 与 cvc5 的性能与 hevm 显示的 Z3 性能相似，分析完成约需 0.08 秒。要复现：
hevm symbolic --code \
$(<examples/PostExample/PostExample.bin-runtime) \
--solver cvc5可以总结的平均结果如下（最佳性能的求解器加粗，若适用）：
| 工具 | 语言 | 求解器 | 时间 (Z3) | 最佳时间 |
|---|---|---|---|---|
| Mythril | Python | Z3 | 2.6 秒 | 2.6 秒 |
| Manticore | Python | Z3、cvc4、Boolector、Yices2 | 1.6 秒 | 1.6 秒 |
| hevm | Haskell | Z3、cvc5 | 0.1 秒 | 0.08 秒 |
| EthBMC | Rust | Z3、Boolector、Yices2 | 3.6 秒 | 0.19 秒 |
包含两个交易的简单示例
到目前为止我们使用的示例展示了使用符号执行的优势，但它也相当简单。在许多情况下，需要多个交易才能达到脆弱状态。让我们稍微修改我们的示例合约，使其在调用 backdoor 函数之前必须通过调用 setLive(true) 来“激活”。
pragma solidity ^0.8.17;
contract PostExample {
bool live;
modifier isLive() {
require(live);
_;
}
function setLive(bool _live) external {
live = _live;
}
// https://github.com/foundry-rs/foundry/issues/2851
function backdoor(uint256 x) external view isLive {
uint256 number = 99;
unchecked {
uint256 z = x - 1;
if (z == 6912213124124531) {
number = 0;
} else {
number = 1;
}
}
assert(number != 0);
}
}大多数工具可以识别导致断言违反的两个交易，尽管这自然花费了近两倍的时间。例如，Mythril 可以正确识别两次函数调用的顺序：setLive(true) 后跟 backdoor(691221...)，耗时 5.4 秒：
要复现：
myth a examples/PostExample/PostExample_2tx.sol -t2Manticore 花费 3.2 秒识别一个违反并生成测试用例：
要复现：
manticore examples/PostExample/PostExample_2tx_0.7.sol \
--smt.solver boolector --thorough-mode --txlimit 2EthBMC 仅需 0.5 秒即可找到脆弱的函数调用顺序：
要复现：
ethbmc examples/PostExample/PostExample_2tx.yml \
--solver yices符号存储
然而，hevm 只是在一次交易中检测到失败的断言（并且仍在不到 0.1 秒的时间内）。现在，输出中添加了 Storage 部分，指示在槽 0x0（对应于 live 变量）中的值必须为 1（即 true），才能使违反发生。这种行为对应于使用的符号存储，这在 hevm 中是默认启用的。在符号存储中，SLOAD 的默认返回值被假定为符号值，而没有其他约束（而不是它等于该类型的默认值，例如布尔值的 false 或 uint 的 0）。在这种模式下，该工具进行欠约束分析，这可能会生成与不可达状态相对应的误报。然而，在某些验证场景下——如我们所用示例中的场景，它可以减少必需探索的函数调用次数，即在该示例中，我们可以避免必须先调用 setLive(true)。除了符号存储，hevm 还支持其他存储模型，可以通过 --storage-model [ConcreteS, SymbolicS, InitialS] 标志进行配置。hevm 当前将分析限制为单个交易，因此在使用 "具体" 存储模型（--storage-model InitialS）时无法识别违反。
要复现：
hevm symbolic --code \
$(<examples/PostExample/postExample_2tx.bin-runtime)
hevm symbolic --code \
$(<examples/PostExample/postExample_2tx.bin-runtime) \
--storage-model InitialS在 Mythril 中，符号存储可以通过 --unconstrained-storage 标志启用。以这种模式进行的分析能够成功发现一个违反，并在 3.4 秒内完成，比之前讨论的两交易分析（5.4 秒）更快，但比前面部分执行的单个交易分析（1.6 秒）慢。你也可能会注意到，查询数量在此时更高。
要复现：
myth a examples/PostExample/PostExample_2tx.sol \
-t1 --unconstrained-storage我们已在 Manticore（ 见此）和 EthBMC（ 见此） 中添加了符号存储。在 Manticore 中，可以通过简单地将默认存储值从零更改为符号值来实现；而在 EthBMC 中，所需的工作则大得多——尤其要实现对应于符号存储位置和存储在其中值的符号值的具体化，以启用基于 geth 的具体验证；这可能是另一篇博文的主题。
在使用符号存储启用的情况下分析单个交易时，Manticore（ --evm.symbolic_storage true）和 EthBMC（ --symbolic-storage）分别在 2.2 秒和 0.2 秒识别出违反：
要复现：
manticore examples/PostExample/PostExample_2tx_0.7.sol \
--smt.solver boolector --thorough-mode \
--txlimit 1 --evm.symbolic_storage True与 hevm 相似，EthBMC 生成的输出中的 Concretized storage 部分显示了允许识别攻击的存储变量的具体化位置和值：
要复现：
ethbmc examples/PostExample/PostExample_2tx.yml \
--solver yices --symbolic-storage| 工具 | 时间 (Z3) | 最佳时间 | 最佳: 2 交易 | 最佳: 2交易 + SS |
|---|---|---|---|---|
| Mythril | 2.6 秒 | 2.6 秒 | 5.1 秒 | 3.4 秒 |
| Manticore | 1.6 秒 | 1.6 秒 | 3.2 秒 | 2.2 秒 |
| hevm | 0.1 秒 | 0.08 秒 | x | 0.08 秒 |
| EthBMC | 3.6 秒 | 0.19 秒 | 0.5 秒 | 0.2 秒 |
SS 代表符号存储。
来自 Echidna VS Forge 仓库的示例
我们可以进一步测试分析过的符号执行工具，通过使用它们运行对 clabby 的仓库 里的示例。这个仓库最初是为了检验 Echidna 和 Foundry 模糊测试工具的性能，其中包含两个智能合约：Foo（以 uint256 变量作为函数输入）和 FooBytes（以 bytes32 变量作为函数输入）。目标是找到两个与魔法数字 0x69 相等的输入，以提供给合约的 foo(uint256/bytes32) 和 bar(uint256/bytes32) 函数。如果这两个函数都以 0x69 的输入被调用，另一个函数 revertIfCracked() 将会 revert。
为了测试分析的工具，我们从 稍微修改了合约，在 revertIfCracked() 中使用 assert Solidity 语句，因为工具只有在识别出执行轨迹中的特定错误代码时才会报告违反。
Mythril 可以在 11 秒内找到导致两个智能合约中的违反的三个交易。为了检测问题，必须用 -t3 标志调用 Mythril，从而增加分析交易的限制——否则分析将只在两个符号交易后没有检测到问题而完成。
十进制数字 105 作为 foo 和 bar 的参数对应于十六进制的 0x69，这可以在 转换器 中验证。
重现步骤：
myth a examples/echidna-vs-forge/symexec/Foo_assert.sol -t3
EthBMC 在 1.2 秒内识别出两个可能的反例（foo() 和 bar() 的两种不同排序）：
ethbmc examples/echidna-vs-forge/symexec/Foo.yml \
--solver yice
有趣的是，即使指示它分析 3 个交易（使用相应的标志 --txlimit 3），Manticore 在仅探索了两个交易后就完成了分析，未发现违规。在调查后，我们意识到第三个交易没有被分析，因为在第二个交易之后没有识别到新的覆盖--在代码中注释掉这一点 使得 Manticore 在 43 秒内找到问题。由于在编写生成的测试用例上花费了大量时间（此 Foo 的分析生成了 187 个测试用例！），我们添加了 --only-invalid-testcases 标志，使其仅生成对应于已识别违反的测试用例。带有此标志的 Foo 分析在 29 秒内完成：
重现步骤：
manticore examples/echidna-vs-forge/symexec/Foo_assert_0.7.sol \
--thorough-mode --smt.solver boolector \
--only-invalid-testcases --txlimit 3
hevm 仅探索一个符号交易--然而，它可以通过使用符号存储（而不是通过调用 foo 和 bar 函数设置变量的值）在 0.1 秒内识别出违规：
重现步骤：
hevm symbolic --code \
$(<examples/echidna-vs-forge/symexec/Foo.bin-runtime)
在使用 bytes32 变量的 FooBytes 智能合约上，所有工具的表现与使用 uint256 变量的 Foo 智能合约相似（与模糊测试器的性能表现有所不同，后者的表现取决于类型）。
| 工具 | 时间 (Z3) | 最佳时间 | 最佳: 2 个交易 | 最佳: 2 个交易 + SS | Foo[Bytes] |
|---|---|---|---|---|---|
| Mythril | 2.6 秒 | 2.6 秒 | 5.1 秒 | 3.4 秒 | 11 秒 |
| Manticore | 1.6 秒 | 1.6 秒 | 3.1 秒 | 2.2 秒 | 29 秒 |
| hevm | 0.1 秒 | 0.08 秒 | x | 0.08 秒 | 0.07 秒 (SS) |
| EthBMC | 3.6 秒 | 0.19 秒 | 0.5 秒 | 0.2 秒 | 1.2 秒 |
Foo 和 FooBytes 的时间相似。SS表示符号存储。
更现实的示例
如果我们在稍微复杂一些的智能合约代码上运行所有这些工具，会发生什么？我们考虑一个 简化版本 的 Vat 智能合约，这是 MakerDAO的一部分。该示例基于使用 Certora Prover 识别的 根本 DAI 方程不变式的违反--另一种形式验证工具。
（简化的）MiniVat 合约包含四个函数 init(), move(address, int256), frob(int256) 和 fold(int256)。除这些函数外，我们在一个单独的函数中编码导致不变式违反的反例：
function counterexample() external {
init();
frob(10**18);
fold(-10**27);
init();
assert(debt == Art * rate);
}
因此，此处符号执行工具的任务是分析 counterexample() 函数，并报告第 6 行中的断言语句的违反（函数的参数是具体的并且 确实 导致了违规，因此我们只是测试工具分析或多或少现实的字节码的能力）。你可能会认为任何符号执行工具都会立即捕捉到这一点--你可能会感到惊讶;）。
正如你所看到的，EthBMC 是唯一一个在分析 MiniVat 示例时保持高性能的工具（尤其是在使用 Boolector 作为求解器时--在这种情况下，分析耗时 0.8 秒；使用 Yices2 时耗时 3.2 秒；使用 Z3 时--29 秒）：
重现步骤：
ethbmc examples/Vat/MiniVat.yml \
--solver boolector
由于 EthBMC 表现良好，我们可以要求它识别导致不变式违反的 2 个函数调用序列，例如：
function counterexample() public {
init();
frob(10**18);
fold(-10**27);
init();
}
function check_assert() public {
assert(debt == Art * rate);
}
这导致在其中一个查询上发生求解器超时（默认为 120 秒），但这并不妨碍 EthBMC 在使用 Yices2 作为求解器时在不到 3 分钟内识别出两笔交易的脆弱序列（counterexample(); check_assert()）（有趣的是，对于 1txn-MiniVat 示例来说，它不是性能最好的求解器）。增加超时或修改合约的实验可能是读者有趣的练习。
重现步骤：
ethbmc examples/Vat/MiniVat_2tx.yml \
--solver yice
Manticore 在 MiniVat 智能合约中需要花费很长时间（超过 10 分钟）才能识别出违规。然而，如果我们关闭其他问题的漏洞检测（通过提供 --exclude 标志），性能会显著改善。当仅生成失败测试用例（--only-invalid-testcases）并仅探索一个交易（--txlimit 1）时，Manticore 在仅 22 秒内识别出 MiniVat 中的断言违规！请记住，这种方法仅在你知道要寻找的漏洞时才能起作用--不幸的是，这种情况很少见。
重现步骤：
manticore examples/Vat/MiniVat_0.7.sol --thorough-mode \
--txlimit 1 --only-invalid-testcases \
--exclude 'overflow,uninitialized-storage,uninitialized-memory,'`
`'reentrancy,reentrancy-adv,unused-return,suicidal,'`
`'delegatecall,ext-call-leak,env-instr,lockdrop'
有趣的是，当在 2 个交易示例上运行（counterexample(); check_assert()）时，Manticore 成功识别我们所寻找的断言违规，耗时 16 分钟。然而，它还报告了两个由于 Manticore 处理哈希所使用的“非安全符号化”策略而产生的假阳性，这种策略不正确地假定存在可能的哈希冲突。当使用不同的哈希策略（--evm.sha3 concretize）运行相同的分析时，这些假阳性没有产生--在这种情况下的执行完成时间略微超过 6 分钟。
重现步骤：
manticore examples/Vat/MiniVat_2tx_0.7.sol --thorough-mode \
--only-invalid-testcases \
--exclude 'overflow,uninitialized-storage,uninitialized-memory,'`
`'reentrancy,reentrancy-adv,unused-return,suicidal,'`
`'delegatecall,ext-call-leak,env-instr,lockdrop' \
--evm.sha3 concretize
由于我们与其他工具的实验表明它们无法跟上 EthBMC 和 Manticore 在 MiniVat 上的性能，为了使它们更容易使用，在接下来的部分，我们默认使用一个 修改过的 MiniVat，其中 counterexample() 是唯一的 external 函数，即可以并且应该在合同中进行分析的唯一函数（其它四个函数被设为 internal）。
在这个版本的 MiniVat 上运行时，如果使用 Z3 求解器，则 hevm 发现失败的断言，时间略超过 2 分钟（我们确实遇到了一个 问题 ，该问题在 hevm 的早期版本中，迅速得到了处理）。
重现步骤：
hevm symbolic --code \
$(<examples/Vat/MiniVat_internal.bin-runtime) \
--storage-model InitialS
然而，当使用 cvc5 作为求解器（--solver cvc5）时，未识别出反例，并显示以下错误：无法确定以下最终状态的可达性：...。
分析原始版本的 MiniVat，其中所有函数都是 public 或 external 可见性，完成时间大约为 5 分 30 秒。重现步骤：
hevm symbolic --code \
$(<examples/Vat/MiniVat.bin-runtime) \
--storage-model InitialS
Mythril 在简化的 MiniVat 版本（具有内部函数）上探索一个符号交易时，耗时 2 分 19 秒，但未报告任何违规。在 140 秒的时间里，125 秒用于约束求解，这表明可能存在 SMT 求解器超时，阻止 Mythril 完成分析：
重现步骤：
myth a examples/Vat/MiniVat_internal.sol -t1
正如预期的那样，如果我们增加求解器超时，分析将无法在 2.5 分钟内完成（请注意，与超时相关的 警告信息 未在默认日志级别下显示）。相反，分析在 30 分钟内甚至没有完成，就被中止（请注意，在 1825 秒中有 1814 秒花费在约束求解上）：
重现步骤：
myth a examples/Vat/MiniVat_internal.sol -t1 \
--solver-timeout 10000000
延迟约束求解
然而，我们可以进一步提高 Mythril 的性能。首先，让我们将检测到的漏洞类型限制为失败的断言（-m Exceptions），类似于我们在 Manticore 中所做的。此外，我们还可以使用 --sparse-pruning 0 标志，启用延迟约束评估。相同的特性在 hevm 默认情况下 被使用，似乎也可以在 Manticore 的 实验性分支 中使用，该分支在 Uniswap V3 审核 期间使用。当执行延迟（或懒惰）约束评估时，并非在每个 JUMPI 时检查路径可达性--而是延迟求解可达性查询，例如，直到事务结束。虽然有效，但在存在循环的情况下可能会导致问题（会无限制地分析）；因此，在 Mythril 中，可达性检查的频率由 --sparse-pruning 提供的参数控制，而 --ask-smt-iterations 在 hevm 中用于指定在可达性检查之前要探测的循环迭代次数。
使用上述参数执行的（优化）分析仅需 1.5 分钟即可找到反例：
重现步骤：
myth a examples/Vat/MiniVat_internal.sol -t1 \
--solver-timeout 10000000 --pruning-factor 0 \
-m Exceptions
我们希望这些简短示例能够展示可用的符号执行工具的 辉煌与悲惨！只要有正确的标志，积极的洞见，它们在不熟练的手中可能会超时并失败。我们在 MakerDAO 对符号执行的很多工作旨在简化和民主化符号执行工具，以使更广泛的智能合约开发人员群体能够使用这些工具，而不一定是形式验证的专家。
总结
这次评估选定的所有四个工具（Mythril、Manticore、hevm、EthBMC）都支持基本的 EVM 和符号执行功能，包括哈希和合约间分析；它们还执行基本的查询优化，例如常量折叠（在将常量表达式发送给求解器之前进行计算）。
基于 Python 的工具如 Mythril 和 Manticore 通常具有更好的用户体验，并提供良好的灵活性和分析配置。另一方面，hevm 和 EthBMC 往往更快。Manticore、hevm 和 EthBMC 支持多个求解器，这在实践中是很有用的，因为不同的求解器各有优缺点。关于这些工具的优缺点的更多详细信息如下：
Mythril
优点：
- 由 ConsenSys 积极维护
- 良好的用户体验，高度可配置，例如，支持几种路径探索策略
- 支持多种优化和特性，包括懒惰约束求解和符号存储
缺点：
- 比 hevm 和 EthBMC 慢
- 仅支持 Z3 的求解器
Manticore
优点：
- 由 Trail of Bits 维护
- 具有多个 API
- 支持多种求解器
- 高度可配置：支持不同的汽油计量策略、模拟 ETH 余额和处理哈希
缺点：
- 通常比 hevm 和 EthBMC 慢
- 不完全支持一些优化和功能，例如符号存储（尽管可以很容易添加）和懒惰约束评估（尽管它在 Uniswap V3 审核 时在一个实验性分支中实现）
EthBMC
优点：
- 快速
- 支持多个求解器
- 用 Rust 编写（这是一个与 Foundry 兼容的语言，可以实现更紧密的集成，这对 条件执行 可能很有用）
缺点：
- 自 2021 年 7 月以来没有维护，错过了一些硬分叉更新（例如更新的操作码）
- 用户体验不佳：输入应作为 YAML 配置文件提供，输出 calldata 应解码
- 缺少一些功能：符号存储和失败的断言检测是我们添加的
hevm
优点：
- 快速
- 与
dapptools集成，支持符号测试 - 支持符号存储模式，多种 SMT 求解器
缺点：
- 正在积极开发中
- 用户体验不佳：输入应作为运行时二进制文件提供，输出 calldata 应解码
- 不探索长度超过 1 的交易序列
总结
最后，符号执行在代码安全性方面是一种有前途的技术，我们的实验证明它可以发现一些其他技术无法解决的问题。令人兴奋的是，这个领域许多团队正在积极开发。同时，在当前状态下，符号执行工具通常容易受到影响、易变且任性。要获得期望的结果，甚至使其正常工作，你通常需要彻底了解它们的内部机制。这篇文章是我们关于使符号执行更实用和可访问的大众化努力系列的第一篇。
有前途的方向
在智能合约的符号执行领域，有前途的方向包括 条件执行--一种具体测试（或模糊测试）和符号执行的组合，这可能有助于克服单纯符号执行的可扩展性挑战和随机测试的不可理解性；以及 符号测试--hevm 通过与 dapptools 的集成以及 Halmos 执行基于参数的测试的符号执行。
根据我们的结果，我们决定进一步尝试 EthBMC，将其与 Foundry 集成，以启用符号测试。虽然符号测试是下一篇博文的主题，但这里是这个集成能做的一小部分：
其他资源
正如在引言中提到的，我们还准备了一个关于智能合约符号执行的教程和两个练习：
参考文献
Keith Schwarz. 2019. Lectures on Mathematical Foundations of Computing. Stanford University. https://web.stanford.edu/class/archive/cs/cs103/cs103.1202/lectures/04/Small04.pdf, https://web.stanford.edu/class/archive/cs/cs103/cs103.1202/lectures/05/Small05.pdf
R. Baldoni, E. Coppa, D. C. D'Elia, C. Demetrescu, and A. Finocchi. 2018. Survey of Symbolic Execution Techniques. ACM Computing Surveys. https://arxiv.org/pdf/1610.00502.pdf
J. C. King. 1976. Symbolic execution and program testing. ACM Communications. https://madhu.cs.illinois.edu/cs598-fall10/king76symbolicexecution.pdf
Trail of Bits. 2020. "如何使用 Manticore 寻找智能合约中的错误". https://ethereum.org/en/developers/tutorials/how-to-use-manticore-to-find-smart-contract-bugs/
网络资源. dapptools & Ethereum Foundation. 2023. "symbolic - hevm". https://hevm.dev/symbolic.html
- 原文链接： hackmd.io/@SaferMaker/EV...
- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
