智能合约是可执行的程序，它们能够在多个实体之间构建可编程的信任机制，而无需依赖受信任的第三方。截至本文撰写时，以太坊网络上已部署了超过 1000 万个智能合约，并且这个数字仍在快速增长。智能合约通常使用一种图灵完备的编程语言 Solidity 编写，但该语言不易审计，容易引入微妙的错误。此外，由于智能合约一旦部署就不可更改，错误可能导致攻击，造成数亿美元的加密货币损失和声誉损害。不幸的是，人工安全分析无法跟上智能合约数量和规模的增长。因此，如果智能合约要被广泛接受，就必须依赖自动化、可扩展的分析机制。

近年来，研究人员开发了多种安全扫描工具。然而，许多分析器要么无法很好地扩展，要么在扩展时会产生大量误报。当漏洞只有在经过一系列特定的函数调用后才会被触发时，这一问题尤为严重。我们将需要调用特定序列的 n 个函数才能触发的漏洞称为 深度-n（depth-n）漏洞。由于合约中可能执行的函数序列数量呈指数级增长，现有的自动化分析工具难以高效检测深度-n 漏洞。

本文提出了一种结合符号执行和数据依赖分析的方法，以高效、可扩展的方式分析深度-n 漏洞。符号执行与静态分析结合的一个重要优势是，它比单独使用符号执行方法更具可扩展性，同时避免了静态分析工具通常存在的误报问题。我们将该技术实现为一个名为 MPro 的工具，它基于现有的符号分析工具 Mythril-Classic 和静态分析工具 Slither。我们使用 MPro 分析了 100 个随机选择的智能合约，实验结果表明，与 Mythril-Classic 相比，MPro 在检测深度-n 漏洞时的速度提高了大约 n 倍，同时保留了 Mythril-Classic 的所有检测能力。

关键词：区块链、智能合约、符号执行、静态分析

引言

以太坊区块链的市值达 148 亿美元 [1]，已有超过 5900 万个账户 [2]，是智能合约的主要平台之一。然而，智能合约仍然容易受到各种安全攻击。例如，2016 年的 DAO 攻击 导致价值 6000 万美元 的以太币被盗 [3]；2017 年的 Parity 钱包攻击 由于访问控制不当，造成了超过 3000 万美元 的损失 [4]；2018 年的 批量溢出攻击（batch overflow attack） 允许攻击者创建大量加密货币代币，导致相关项目的声誉受损，并使以太币（ETH）价格在攻击被披露当天下跌 8% [5]。

符号执行（symbolic execution） 是一种广泛应用于智能合约分析的技术，它尝试探索所有可能的程序执行路径，并利用约束求解器为每条可行路径计算具体输入（测试用例）。然而，随着程序中的条件分支数量增加，可能的执行路径呈指数级增长，使得符号执行的扩展性受到路径爆炸（path explosion） 问题 [9] 的限制。然而，智能合约的代码量通常较小，这使得符号执行在智能合约分析领域的适用性较高，而不像传统软件系统那样面临数百万行代码的复杂性。

Mythril-Classic [7] 是目前最流行的智能合约安全扫描工具之一，它基于符号执行技术，能够高度准确地模拟 以太坊虚拟机（EVM） [8]，并支持广泛的安全检查。然而，现有的智能合约安全扫描工具（包括 Mythril-Classic）在分析不同长度的函数调用序列时面临组合爆炸（combinatorial explosion） 的问题。

深度-n 漏洞（depth-n vulnerabilities） 最早由文献 [10] 作为跟踪漏洞（trace vulnerabilities） 提出，这类漏洞不会在单次函数调用中触发，而是需要特定的函数调用序列。Mythril-Classic 目前使用暴力搜索（brute force） 方法（结合基本的路径修剪策略）来执行所有可能的函数调用序列，以检测深度-n 漏洞。然而，这种方法容易导致组合爆炸。

我们在 100 个智能合约上的实验（详见第 IV 节）表明，34% 的测试案例 包含深度-n 漏洞。此外，Mythril-Classic 的执行时间随着深度增加呈指数级增长：

• 在 深度 2 时，执行时间比 深度 1 增加 3.43 倍；
• 在 深度 3 时，执行时间比 深度 1 增加 14.04 倍。

这一结果表明，优化 Mythril-Classic 在更深层次上的符号执行引擎至关重要。

本文提出了一种基于数据依赖分析（data dependency analysis） 的优化方法，用于检测深度-n 漏洞，并将其与 Mythril-Classic 集成。通过利用数据依赖分析，可以在分析过程中剪枝掉不必要的函数调用序列，并优先执行更可能导致深度-n 漏洞的调用序列（即基于外部可访问函数对状态变量的读/写依赖关系）。

本文的主要贡献包括：

1. 基于数据依赖分析的优化方法，用于检测深度-n 漏洞，提高符号执行效率。
2. MPro 工具的开源实现——它在 Mythril-Classic 的基础上集成了数据依赖分析优化。
3. MPro 的评估实验，我们使用 100 个真实世界的智能合约 进行测试，验证 MPro 的性能提升。

本文余下部分的组织如下：

• 第 II 节：介绍理解本文所需的背景知识。
• 第 III 节：详细描述 MPro 的设计和实现。
• 第 IV 节：介绍 MPro 的评估实验，包括测试设置和实验结果。
• 第 V 节：讨论 MPro 目前的局限性。
• 第 VI 节：综述相关研究并与 MPro 进行比较。
• 第 VII 节：总结本文的研究成果，并展望未来工作。

背景

以太坊与智能合约

智能合约本质上是存储在以太坊区块链上的程序，并由一个唯一的合约地址标识。以太坊区块链由许多节点以点对点的方式连接到以太坊网络进行维护和更新。以太坊网络中的每个节点都运行以太坊虚拟机（EVM）。用户可以与以太坊网络交互，以执行以下操作：

1. 创建新的智能合约；
2. 调用智能合约的函数；
3. 将加密货币以太币（ETH）转移到其他合约或用户。

对智能合约的函数调用会被记录在交易中。以太坊区块链也可以被描述为基于交易的状态机，其中区块链上的交易序列决定了每个智能合约的状态以及每个用户的余额【12】。

每个智能合约都包含其私有存储、预定义的可执行字节码，并可能控制一定数量的以太币。当用户调用智能合约的函数时，以太坊虚拟机（EVM）【8】会执行该函数对应的字节码，这些字节码通常是由图灵完备的编程语言（如 Solidity 或 Vyper）编译而成的。下一节将介绍由于这些编程语言的复杂性及其底层编程范式所导致的各种漏洞。

易受重入攻击的以太坊智能合约

智能合约安全性

与传统软件程序不同，智能合约是公开可访问、透明且不可变的。这导致了一个问题，即其中的漏洞（包括安全问题）是可见的，并可能被攻击者利用。由于智能合约通常持有一定数量的加密货币，攻击者有很强的动机利用这些漏洞来谋取私利。在本节中，我们将具体描述两种可以被 MPro（以及 Mythril-Classic）检测出的漏洞。Mythril-Classic 和 MPro 的完整检测能力列表可参见【7】。

可重入漏洞

这是智能合约中一个众所周知的漏洞，因为它曾导致 2016 年 DAO 攻击事件【3】。图 1 展示了一个简单的易受可重入攻击的智能合约。

在 Solidity 语言中，智能合约可以使用 call 指令调用另一个智能合约的函数，并且这种调用是同步的。换句话说，调用合约在执行下一行代码之前，必须等待被调用合约执行完毕。

在图 1 中，第 4 行的 withdraw 函数的目的是在满足条件的情况下，将一定数量的以太币发送到外部账户（即 withdrawer）。该条件是 withdrawer 在当前合约中的余额（由全局变量 balance 记录）足够。合约会在发送以太币后（第 7 行）更新 withdrawer 的余额。

然而，可重入攻击可能在第 6 行发生。被调用的外部合约可以在第 6 行的调用过程中，再次调用 withdraw 函数。需要注意的是，此时 balance 变量尚未更新，因为调用合约仍在等待外部调用完成。因此，在可重入攻击的情况下，第 5 行的 if 语句的真分支会被反复执行，导致合约中存储的所有以太币在短时间内被提取完毕。

防止此类攻击的最简单方法之一是在执行外部调用之前，先更新所有持久化存储变量【13】。因此，为了修复该漏洞，需要在执行外部调用之前更新 balance 变量（如图 1 中第 11 行开始的 withdrawerFixed 函数所示）。

存在不受限制自毁漏洞的智能合约

由于仅调用单个函数即可触发此类漏洞，我们将这种特定的可重入漏洞分类为深度-1（depth-1）漏洞。然而，需要注意的是，并非所有的可重入漏洞都是深度-1 漏洞。

无限制的自毁漏洞

智能合约在以太坊区块链上会持续存在，直到它被合约所有者或其他授权代理调用 Solidity 语言中的 selfdestruct 指令销毁。然而，任意销毁智能合约可能导致以太币被锁定或发生意外的以太币转移，因此 selfdestruct 指令必须受到严格保护，防止被任意用户调用。

图 2 展示了一个可以被任意用户销毁的简单智能合约。在这个示例中，第 13 行的 kill 函数由 onlyOwner 修饰符（定义在第 4 行）保护，该修饰符确保只有合约的所有者（存储在 owner 变量中）才能访问该函数。

然而，攻击者可以通过调用 setOwner 函数（图 2 第 9 行）成为合约的新所有者，然后调用 kill 函数销毁合约。由于 setOwner 函数没有受到任何访问控制，任何人都可以调用它并篡改 owner 变量，从而夺取合约的控制权。

利用该漏洞，攻击者只需执行以下两步操作即可完成攻击：

1. 调用 setOwner 函数，使自己成为合约的所有者；
2. 调用 kill 函数销毁合约。

该漏洞曾在 2017 年的 Parity 钱包 中被发现，导致价值 3000 万美元的以太币损失【4】【14】。

在本文中，我们将需要特定的函数调用序列才能触发的漏洞称为深度-n（depth-n）漏洞，其中 n 是触发该漏洞所需的最小函数调用次数。因此，在本示例中，该无限制自毁漏洞属于深度-2（depth-2）漏洞。

值得注意的是，该漏洞仅能在交易深度为 2 时被 MPro（以及 Mythril-Classic）检测到，而无法在交易深度为 1 时被检测到。

设计与实现

本节深入介绍了依赖分析技术、启发式符号引擎以及 MPro 的设计。

数据依赖分析

本文的关键观察点是，在一系列函数调用中，至少需要存在一个状态变量依赖关系，才能导致 depth-n 漏洞。当一个交易（函数调用）完成后，对局部变量（存储在堆栈和内存中的变量）的更改会被丢弃，只有对状态变量的更改才会反映在后续交易中，因为它们存储在持久化存储中。换句话说，如果智能合约中不存在状态变量依赖关系，则不会包含 depth-n 漏洞。

此外，我们研究了 Mythril-Classic 的 11 个预定义安全分析模块，发现 Mythril-Classic 能检测到的所有 depth-n 漏洞，都是由智能合约的 读取后写入（RAW，Read After Write） 函数依赖关系引起的。

为了在 MPro 中实现数据依赖分析，我们使用了 Slither，因为它提供了便捷的 API，可以直接分析智能合约中各个函数的变量使用情况 [11]。Slither 是一个高度可扩展的静态分析工具，它在 SlithIR 层面分析智能合约的中间表示代码。在本文中，我们使用了一个稍作修改的 Slither 版本来分析目标智能合约中每个函数的状态变量使用情况。根据 Slither 返回的状态变量使用信息，我们按照以下方式确定优先级交易序列：

1. 对于给定合约中的每个 外部可访问函数 f，找到 f 中读取的所有状态变量。
2. 对于函数 f 读取的每个状态变量 v，找到合约中所有写入该状态变量的函数。

由此，我们确定了函数 f 的 RAW 依赖关系。

函数依赖信息存储在一个字典中，该字典的键是每个 外部可访问函数，值是该函数所依赖的一组相应函数。需要注意的是，如果一个函数在自身内部既读取又写入状态变量，则该函数可能对自身具有 RAW 依赖。

Mythril-Classic 工作流程

Mythril-Classic 和 MPro 都包含两个主要组件：（1）符号执行引擎 和（2）11 个预定义安全分析模块。每个安全分析模块封装了一个或多个智能合约安全属性。

从高层次来看，该工具首先调用其符号执行引擎，对目标合约进行符号执行，并生成一个执行树，表示所有可能的程序状态、执行路径和约束条件。在符号执行过程中，执行的程序状态和约束条件会在必要时传递给安全分析模块。

符号执行过程中生成的路径约束条件，与安全分析模块中安全属性的否定约束条件一起，被传递给 Z3 SMT 求解器 进行求解。如果这些约束的整体可满足，则表示违反了某个安全性属性（即发现了漏洞）。

本论文未详细解释安全分析模块的具体内容，因为 MPro 并未对 Mythril-Classic 的安全分析模块进行增强。

原始 Mythril-Classic 符号引擎

由于完整的执行树可视化难以适应单页展示（且仍然可读），图 3 仅展示了由 Mythril-Classic 生成的一个执行子树示例。

由Mythril-Classic生成的部分执行树

每个节点由一系列连续的 EVM 操作码 [8] 组成，表示程序的一个基本代码块。一个节点可能以终止指令（如 RETURN、STOP、REVERT、ASSERT_FAIL、SUICIDE）结束，或以跳转指令（如 JUMPI、JUMP）结束。

本质上，每条指令都代表智能合约的一个状态变化。每个节点都会关联一个指针，指向下一个基本代码块（终止指令除外），从而形成一条执行路径。每条路径都带有路径约束条件，用于表示状态的可达性。

所有已执行的程序状态都会被缓存。当执行新指令时，会检索前一个程序状态，并基于前一个状态和当前指令，确定新的程序状态。修改后的新状态会被推回缓存，并作为下一条指令执行的初始状态。

为了检测 depth-n 漏洞，Mythril-Classic 采用暴力搜索（结合基本的路径修剪策略）来模拟所有可能的交易序列。具体而言，其符号执行引擎会将前一个交易的终止状态作为下一个交易的初始状态，并继续下一次符号执行迭代。

Mythril-Classic 使用了两种路径修剪技术，若满足以下任一条件，则后续交易执行会被修剪：

1. 前一个交易的终止状态为 REVERT（意味着所有程序状态更改被回滚）或 SUICIDE（意味着智能合约在区块链上不再存活）。
2. 前一个交易未对持久存储进行写入（意味着智能合约的状态存储保持不变）。

然而，当智能合约包含多个可以以不同顺序调用的函数时，上述技术仍不足以缓解 Mythril-Classic 面临的组合爆炸问题。

MPro架构

MPro 启发式符号引擎

MPro 的启发式符号引擎构建在 Mythril-Classic 原始符号引擎之上，提供了额外的特性，以修剪不必要的执行路径（即函数序列），同时保留原始的路径修剪技术。

我们的启发式符号引擎不会修改函数内部的代码块执行，而是在前一个函数终止时，引导路径分支到依赖列表中的下一个函数（由 Slither 计算得出），并跳过不必要的路径生成。

MPro 启发式符号引擎的工作流程如下：

1. 调用 Mythril-Slither 接口，检索并存储 RAW 函数依赖关系至查找表。
2. 使用原始 Mythril-Classic 符号执行引擎，符号执行所有函数至调用深度 1。
3. 对于调用深度 1 处的所有终止状态，仅在满足以下条件时，标记该状态为下一个交易的起始状态：
   • 前一个交易的函数 在查找表的键集中（即，该函数至少对另一个函数具有 RAW 依赖）。
4. 在确定下一个交易中要调用的函数时，查找依赖列表，引导原始符号引擎执行 目标函数调用，并跳过其他分支。

MPro 设计

图 4 展示了 MPro 的工作流程。

MPro 以Solidity 源代码作为输入，并交给 Slither 和 Mythril-Classic 处理。

Slither 首先对智能合约进行静态分析，提取状态变量的使用情况，并将其传递给 Mythril-Slither 接口，在此分析 RAW 函数依赖关系。

然后，原始 Solidity 源代码 和 依赖信息 一起输入到 MPro 的启发式符号执行引擎中。该引擎根据依赖信息，以确定的顺序执行函数组合。

在 MPro 的启发式符号引擎中，执行路径始终沿着具有 RAW 依赖的函数组合进行，而其他路径被视为不必要的函数序列，因此被修剪出搜索空间。

评估

实验设置

我们在 4 台 Microsoft Azure 标准 D2s v3 实例上评估了 MPro 和 Mythril-Classic v0.20.0（撰写本文时 Mythril-Classic 的最新版本）的性能和漏洞报告。每台实例配备 2 个虚拟 CPU 和 8GB 内存。我们使用 solc v0.4.25 和 solc v0.5.4 分别编译需要 0.4 和 0.5 版本编译器的智能合约。约束求解器使用 Z3 v4.8.4。

我们在两个数据集上评估 MPro 和 Mythril-Classic：(1) SWC 测试套件 [15]，其中包含 102 个包含漏洞（以及部分修复方案）的简单智能合约，以及 (2) 100 个平均代码行数为 258.76 行的真实世界智能合约。真实世界合约数据集的构建方式如下：32 个合约是通过付费提交至 Quantstamp 智能合约扫描协议²；其余 68 个合约来自 Ethereum 主网和 Ropsten，我们在 2019 年 1 月底收集数据时选取了当时最新部署的合约，前提是其源代码可用且在数据集中是唯一的。

我们的评测目标是：(1) 验证 MPro 和 Mythril-Classic 生成的漏洞报告是否一致；(2) 验证 MPro 是否比 Mythril-Classic 更高效。

安全性

由于 MPro 的安全分析模块与 Mythril-Classic 保持一致，我们未专门检查两者检测出的漏洞是否存在误报或漏报。这不在本论文的讨论范围内。相反，我们检查了 MPro 在两个数据集上的漏洞报告，并验证在不设超时时间的情况下，MPro 在深度 1、2 和 3 处的漏洞报告与 Mythril-Classic 一致。

我们注意到，如果使用超时（例如 30 分钟）来终止 MPro 和 Mythril-Classic 的运行，那么在深度 2 和 3 处，MPro 能够检测到比 Mythril-Classic 更多的漏洞。更多细节将在下一节讨论。

从本论文的安全性评估来看，我们可以得出结论：MPro 至少与 Mythril-Classic 同等优秀。我们将 Mythril-Classic 安全能力的进一步改进留待未来研究。

性能

我们使用100个随机选择的真实世界智能合约来测量MPro和Mythril-Classic的性能。SWC测试套件的性能评估被跳过，因为SWC测试套件中的测试用例使用最少量的代码来展示特定类型的漏洞，它们并不是真实世界的合约。

表1 性能比较（深度2）

表2 性能比较（深度3）

总体加速比和超时情况

我们在 100 个随机选择的真实世界智能合约上测量了 MPro 和 Mythril-Classic 的性能。在 SWC 测试套件上的性能评估被省略，因为 SWC 测试套件的测试用例使用最少量的代码来展示特定类型的漏洞，并不代表真实世界的智能合约。

我们在深度 1、2 和 3 处，分别测量了两种工具在有无超时情况下的性能。在深度 1 处，两者的性能基本相同，仅有 MPro 额外运行数据依赖分析所需的少量时间增量。然而，如果用户仅关注深度 1，则可以通过简单优化排除该分析。

在深度 2 处，我们设置了 10 分钟和 30 分钟的超时，发现 Mythril-Classic 比 MPro 分别多 9 和 3 个程序超时，而 MPro 在相同条件下分别有 8 和 5 个程序超时。表 I 总结了 MPro 和 Mythril-Classic 在深度 2 处的性能比较。

在无超时的情况下，MPro 的平均运行速度几乎是 Mythril-Classic 的 2 倍。当设定 10 分钟超时时，加速比略有降低，因为超时实例的执行时间被限制在 10 分钟以内。然而，在 10 分钟超时的情况下，Mythril-Classic 超时的实例数量是 MPro 的两倍多。此外，在 Mythril-Classic 无超时运行时，有两个实例因内存限制被操作系统终止。而在 MPro 运行时，这两个实例成功完成分析，因为 MPro 采用了路径剪枝策略，从而减少了内存使用。

在深度 3 处，我们为了公平起见，将超时设置为 120 分钟，发现 Mythril-Classic 比 MPro 多 8 个程序超时，而 MPro 共有 12 个程序超时。表 II 总结了深度 3 处的性能比较，结果显示，在深度 3 处，MPro 相对于 Mythril-Classic 的加速比接近 3 倍。与深度 2 的观察结果类似，在设定超时的情况下，加速比有所降低，但 Mythril-Classic 超时的实例数量几乎是 MPro 的两倍。

我们在深度 3 处停止了评测，因为在我们的数据集中，两个工具都未检测到任何深度 3 及以上的漏洞。需要注意的是，我们未报告无超时情况下的深度 3 平均运行时间，因为 Mythril-Classic 运行超时的 20 个程序已执行了两天以上，最终被手动终止，因此无法准确计算加速比。但可以推测，无超时情况下，加速比可能会比 120 分钟超时时的 2.89 倍更高。

表3 按复杂性分类的性能比较

加速比与智能合约复杂度的相关性

我们进一步分析了 MPro 在深度 2 和 3 处性能明显优于 Mythril-Classic 的测试用例。我们将这些测试用例分为两类：(1) 在 Mythril-Classic 中运行时间在 0 到 10 分钟之间的测试用例；(2) 在 Mythril-Classic 中运行时间超过 10 分钟的测试用例。表 III 显示了 MPro 在这两类测试用例上的加速比。

随着智能合约复杂度的增加（由 Mythril-Classic 的整体运行时间指示），MPro 的加速比在 Mythril-Classic 运行时间超过 10 分钟的测试用例中达到 4.45 倍（深度 2）和 6.51 倍（深度 3）。这一趋势预计会继续，即智能合约越复杂，其整体执行树越大，因此 MPro 通过数据依赖分析剪枝的搜索空间就越多。

解决实例的数量

除了性能加速比，我们还测量了 MPro 在给定时间内解决的实例数量的优势。具体而言，我们统计了 100 个真实世界测试用例中，在 60、180、300、600 和 1800 秒内完成分析的测试用例数量。图 5 展示了深度 2 处的比较，x 轴表示在 100 个随机选择的智能合约测试用例中解决的实例数量，y 轴表示时间。

从图中可以看出，MPro 相较于 Mythril-Classic 具有绝对优势，在相应的采样点上分别多解决了 10%、17.14%、8.75%、9.52% 和 5.56% 的实例。类似地，我们在深度 3 处记录了 600、1800、3600 和 7200 秒阈值下的解决实例数量，结果显示 MPro 在这些时间点上分别比 Mythril-Classic 多解决了 19.67%、6.57%、8.97% 和 8.75% 的实例，具体见图 6。

限制

**限制；**MPro 存在一些限制，我们在本节中进行描述。

首先，Slither 的数据依赖分析不具备控制流敏感性。具体来说，Slither 仅报告出现在函数中的所有状态变量。然而，其中一些状态变量可能不可达。这可能导致 MPro 的函数依赖分析不够精确，从而在符号执行过程中生成非依赖函数组合。要解决此限制，需要采用更精确的静态分析技术，我们计划在未来的工作中进行改进。

深度2下已解决实例的比较

其次，MPro 并未优化智能合约函数的局部符号执行，而仅通过启发式方法剪枝不必要的后续函数。根据 MPro 的性能评估，我们认为仍然有改进空间，因为仍然有一些真实世界的智能合约在 MPro 中运行 30 或 120 分钟后超时。我们计划在未来的工作中解决此问题。

最后，由于 MPro 依赖 Slither 进行数据依赖分析，因此需要智能合约的源代码作为输入。我们计划在未来的工作中直接在智能合约字节码上应用数据依赖分析技术，以消除这一限制。

相关工作

在本节中，我们介绍与 MPro 相关的智能合约分析工具。由于本文主要关注性能优化，而非检测更多类型的漏洞或减少误报率，因此我们仅将 MPro 与 Mythril-Classic 进行性能比较。以下工具与 MPro 无法直接进行性能对比，因为它们检测的漏洞类型不同。

Maian [10]（已停止维护）是一款用于智能合约的符号分析工具，能够模拟智能合约的多个交易。Maian 团队首先系统地定义了交易漏洞的形式化特征。通过混合符号执行（concolic analysis），Maian 用具体数值初始化部分程序状态，从而使其能够扩展到分析真实世界的智能合约。为了进一步提高可扩展性，Maian 还利用了基本的静态分析来过滤掉不必要的符号执行。Maian 仅能检测三种漏洞模式：贪婪型（Greedy）、浪费型（Prodigal）和自毁型（Suicidal）。

Securify 是一款全自动的静态以太坊智能合约分析工具。Securify 通过两种模式定义安全属性：合规模式（compliance patterns），用于确认安全属性已被满足；违规模式（violation patterns），用于确认安全属性未被满足 [17]。借助这些模式，该工具能够提供明确的安全性违规信息，从而减少人工验证检测结果的工作量。Securify 提供了 7 种内置安全属性，以及相应的合规/违规模式，例如 “调用后禁止写入（no write after call）”、“受限写入（restricted write）” 和 “受限转账（restricted transfer）”。

Zeus [18] 是一个基于**抽象解释（abstract interpretation）和模型检测（model checking）的自动化形式化验证框架，专门用于分析智能合约。Zeus 将智能合约中的问题划分为正确性问题（correctness issues）和公平性问题（fairness issues）**两类。Zeus 在低级中间表示（IR）上分析输入的智能合约，并允许用户在模板中自定义正确性/公平性标准。

结论与未来工作

我们提出了 MPro，一款全自动且可扩展的以太坊智能合约安全扫描工具，并将其作为免费开源软件提供。该工具基于 Mythril-Classic 和 Slither 进行开发，结合了静态分析和符号执行，以减少不必要的执行路径。我们使用 100 个真实世界的智能合约数据集对 MPro 进行了性能评估，并将该数据集公开给大众。从实验结果来看，MPro 在检测深度 n 的漏洞时，比 Mythril-Classic 平均快 n 倍，同时保留了 Mythril-Classic 的所有检测能力。

未来工作

未来，我们计划对 MPro 进行两项重要改进：

1. 开发基于 Slither 的目标导向符号执行机制 [16]，结合 MPro 的启发式符号引擎。
2. 并行化 Mythril-Classic 的符号执行和安全分析流程，以进一步提升 MPro 的性能。

由于静态工具（如 Slither）在计算可用于验证漏洞的具体输入方面存在局限性，我们计划通过更高级的静态分析和符号执行结合机制来解决此问题。

在 基于 Slither 的目标导向符号执行机制 中，MPro 旨在针对 Slither 标记的安全警告生成测试用例，以证明漏洞确实可被利用。基本思想是引导 MPro 的符号执行引擎，沿着最有可能到达 Slither 标记的漏洞状态的路径执行。如果符号执行引擎和约束求解器能够返回具体输入，则漏洞被证实存在；否则，该问题可被归类为误报（false positive）。

目前，MPro 仅能引导执行路径至下一个相关交易。本改进可以被视为在 MPro 之上进一步剪枝搜索空间的技术。理想情况下，所有不会导致错误的路径都可以被跳过。由于 Slither 执行效率高，且单条路径的生成开销较低，因此该机制预计能进一步提升 MPro 的性能。

此外，Mythril-Classic 和 MPro 目前的分析流程是顺序执行的。虽然直接并行化符号执行引擎可能导致冗余，但可以通过初始函数调用来拆分整体执行树为多个独立子树。每个子树仅包含一个初始函数调用及其依赖项，因此可以轻松实现这些独立子树的并行执行。

[注意]看雪招聘，专注安全领域的专业人才平台！