本文作为我们研究的进展报告，重点在于利用区间分析这一已有的静态分析方法来检测智能合约中的漏洞。我们展示了一些具有代表性的易受攻击的智能合约示例，并分享了我们使用多个现有检测工具进行实验的结果。我们的发现表明，这些工具未能检测出我们示例中的漏洞。为了提高检测能力，我们在现有检测工具 Slither [3] 的基础上实现了区间分析，并展示了它在识别某些其他工具无法检测到的漏洞方面的有效性。

“智能合约”这一术语最初用来描述自动化的法律合同，其内容不可协商或更改。如今，这一术语通常指的是由去中心化网络或区块链中的特殊节点执行的程序。事实上，区块链技术体现了该术语最初的含义：合约被编码为不可变的代码片段，合约条款是预先确定的，并由合约本身自动执行。

这种不可变性也意味着合约开发者需要投入更多的精力：他们必须非常谨慎地部署代码，因为该代码（1）是公开的，任何人都可以看到；（2）不能像普通程序那样被更改或更新。Ethereum 是一个非常流行的区块链平台，其部署代码中的漏洞曾导致一些重大的攻击事件。例如，“The DAO 攻击” 就是基于智能合约在执行过程中可以被中断并再次调用的事实。这被称为重入漏洞。攻击者注意到，在该智能合约的提现函数中，数字资产的转移发生在更新余额（即将提现金额从余额中扣除）之前。攻击者首先向智能合约中存入加密货币，然后通过构造一个使提现函数在更新其自身余额之前再次调用自身的场景，持续提取合约中的资金，直到合约余额低于提现金额为止。

这种错误是令人遗憾的，因此研究人员和从业者开始提出各种方法和工具来检测它们。例如，Slither [3] 是一个易于使用的静态分析工具，用于分析用 Solidity 编写的智能合约；Mythril 是一个基于符号执行的 EVM 字节码安全分析工具；Solhint 是一个 Solidity 代码的语法检查器。工具的数量很多，并且在多篇论文中进行了探讨（例如，[5, 7, 6, 1, 4]）。这些工具确实非常有用，但它们并不完美，可能无法检测出智能合约代码中的问题情况。

在本文中，我们提供了几个包含漏洞的智能合约示例，并发现现有漏洞检测工具并不像我们预期的那样精确，它们未能检测出我们示例中的漏洞。我们尝试将一种名为区间分析的现有静态分析方法添加到 Slither 工具中。该方法可以更好地近似每个程序变量的取值范围。根据我们进行的实验，区间分析在检测智能合约中的问题情况方面非常有用。例如，Solidity 中的整数除法会忽略余数。在一种需要将加密货币金额进行分配并转移给多个接收者的情况下，若除法操作忽略了余数，可能会导致部分资金被锁定在智能合约中。另一个示例与未初始化变量有关：此类变量被赋予默认值，而默认值可能不适用于该变量的用途。通过跟踪每个程序变量的所有可能取值，区间分析可以提示智能合约中的此类情况。

贡献总结

论文结构

第 2 节我们展示几个智能合约漏洞示例。第 3 节中我们展示当前最先进工具在这些示例上的表现。第 4 节介绍了区间分析技术及我们的实现。第 5 节为结论部分。

本节包含多个用 Solidity 编写的智能合约漏洞示例。这些示例选自一个更大的分类体系 [6]。该分类共包含 55 个漏洞，分为 10 个类别。在选择这些缺陷时，参考了文献和现有的社区分类。我们选择这些漏洞是因为当前最先进的工具无法检测出它们，而这些漏洞可以使用区间分析来检测。

Solidity 的 assert 和 require 语句通常用于验证布尔条件。根据 Solidity 文档，assert 用于检查内部错误，而 require 应该用于测试运行时才能确定的条件。这两个语句都会抛出异常并回滚相应的交易。在其预期用法中，assert 中的条件永远不应为 false，因为这表示合约级别的错误，而 require 中的条件可以为 false，因为它们表示输入错误。无论语句指定的是哪种级别的错误，如果它们包含的条件是重言式或矛盾式，都是一个问题。重言式会使语句毫无意义，而矛盾式则会导致交易无法完成，如下代码所示：

这是大多数编程语言中常见的经典算术问题。Solidity 编译器不允许直接除以零。然而，编译器无法检测分母是否可能在计算时变为零。以下代码示例中，在计算每个接收者应获得的金额（第 4 行）之前，并未检查 recipients 数组的长度：

这也是许多编程语言中常见的算术问题。Solidity 执行整数除法，这意味着除法操作的结果会被截断。这可能导致忽略除法余数，从而产生逻辑错误。以下代码片段提供一个示例：如果提供的金额不能被接收者的数量整除，那么部分加密货币可能会被锁定在合约中。

未初始化的变量可能会导致逻辑错误或异常。如果变量未被初始化，根据其类型赋予的默认值很可能不适合该变量的用途。以下代码包含一个依赖于 owner 状态变量的访问修饰符。该变量是私有的，因此无法在合约外部访问或赋值。此外，构造函数中也没有对 owner 进行显式初始化。这会导致变量保持默认值，从而使所有带有 onlyOwner 修饰符的函数无法执行。

参数验证或“净化”是每个方法开始时必须实现的过程。这确保了方法总是按预期执行。不能信任终端用户总是提供有效参数。如果缺少验证，而用户又不了解，甚至是恶意的，就可能导致关键性错误，从而产生意外结果或完全停止合约的执行。以下示例包含一个内部数组的 getter 方法。用户可以提供未经验证的索引，因此有可能越界访问。

在 Solidity 中，枚举类型以无符号整数的形式存储。因此，它们可以与 uint 类型的变量进行比较和赋值。然而，这种情况可能很棘手，因为枚举的值域通常远小于无符号整数的值域。如果将一个超过枚举范围的变量赋值给枚举变量，则交易将被回滚。虽然回滚交易被认为是安全的，但这种情况表明合约代码存在逻辑错误，最好避免出现此类问题。

本节简要介绍我们所进行的一些实验结果。基本上，我们使用了一些工具对智能合约进行分析，以检查它们在第 2 节所示示例中的表现。我们选择的工具如下所示。值得注意的是，我们选取了实现不同技术（如静态分析、符号执行、代码风格检查器）的工具。一个工具要符合我们的研究标准，必须是开源的、活跃的，并且兼容最新版本的 Solidity。

表 1：工具在我们的示例上执行时的评估摘要（第2节）

Slither 是一个用 Python 编写的静态分析工具，提供漏洞检测和代码优化建议。它具有许多针对不同问题的检测器。与其他工具相比，它的分析运行时间非常短。它通过将 EVM 字节码转换为一种称为 SlithIR 的中间表示来分析 Solidity 代码。作为开源项目，它允许任何人参与和改进，是我们后续实现的基础（详见第 4 节）。Slither 能够检测未初始化变量、明显的恒真与恒假条件。

Solhint 是一个 Solidity 代码的代码风格检查器。作为一个开源项目，它可以检测潜在漏洞、优化机会以及是否遵循代码风格约定。该工具还包含一套可自定义的检测规则以及预设配置。用户可以定义自己的配置并选择要检测的问题。不幸的是，Solhint 无法检测出我们示例中的任何问题。

Remix 也包含一个静态分析插件。我们无法找到该工具所执行分析过程的任何信息。此外，它也无法检测出我们示例中的任何问题。

Mythril 是一个利用符号执行来模拟合约方法多次运行的工具。与其他工具相比，它的运行时间相当长，我们甚至遇到过执行时间超过几个小时的情况。Mythril 也未能检测出上面所提到的任何问题。

我们在表 1 中总结了所获得的结果。结果表明，几乎所有工具都未能检测出我们示例中的漏洞。这并不意味着这些工具在智能合约代码中发现问题方面无用或效果很差。我们对结果的解读是：这些工具需要通过更强大的技术进行增强，以提高其检测能力。

区间分析是一种静态分析技术，用于在某条指令处近似每个变量的值区间。该技术不仅可以预测变量的值区间，还可以用于预测可以从变量值中推导出的某些属性。例如，不使用整数区间，而是分析变量的奇偶性，仅使用两个值的区间（偶数、奇数）。

表 2：投票函数的区间分析

我们通过第 2.6 节中的不匹配类型示例来介绍区间分析。此外，我们展示了区间分析如何帮助我们检测该示例中的问题，具体来说是 vote 函数中的问题：

该函数记录用户的投票并增加所选项的总票数。问题出现在第 2 行：

输入类型为 uint，它很容易超出枚举类型允许的值范围 [0,1,2]。

区间分析为程序中每个位置的每个变量提供值区间的近似。在表 2 中，我们展示了如何为示例计算这些区间。表中每一行展示了在执行每条语句（第一列）之前，各程序变量（列显示）的区间。例如，在执行语句 1 之前，我们对变量 option 没有任何信息，因此其值区间为 uint 的取值域。在正常执行情况下（否则事务将被回滚），_votes[msg.sender] 在语句 2 之前的值区间变为 [0,2]，即 Option 可取的唯一范围。

区间分析使用工作列表算法执行该计算，该算法遍历程序的控制流图（CFG），并不断更新变量的区间直到达到不动点。该算法见第 4.2 节。

请记住，我们试图通过区间分析检测的问题是赋值变量与被赋值变量之间的取值域不匹配。由于区间分析会计算 option 和 _votes[msg.sender] 的区间，因此仔细检查两者之间的差异即可揭示问题。一个 require 语句在前面检查 option 参数的取值将解决该问题，并且我们的检测技术将不会发出警告。

我们使用 Slither 提供的 Python 模块构建了我们的实现。这些模块也是 Slither 自身检测器内部使用的模块。在执行过程中，Slither 会填充其内部数据结构，包含合约的控制流图（CFG）、代码的 SSA（单赋值）中间表示，以及每个变量的信息（如类型、作用域和名称）。我们利用这些数据结构中的信息来实现区间分析。

图1：worklist算法

图 1 所示的工作列表算法通过处理合约 CFG 中的每条边来工作。这些边被加入一个列表（即“工作列表”）。这是一个迭代算法，处理已有元素直到列表为空。当有新信息加入当前状态时，会将新的边也加入工作列表。算法在不再发现新信息时终止。

我们实现了一个模块化的工作列表算法。极值标签、顺序函数和流函数等必要信息通过参数提供给工作列表算法。这使我们能够使用相同的基础实现执行多种类型的分析。我们的实现利用 Slither 提供的 CFG 将函数代码划分为多个部分。每个节点进一步被划分为 SlithIR SSA 代码行，逐条进行分析。除了基本类型如 uint 和 bool，我们的实现还可以建模数组、映射和结构体等复杂类型。

我们定义了自己的数据类型来封装变量的信息，如类型、作用域、名称，最重要的是值区间。程序状态被表示为一个字典，键为变量名，值为我们自定义的数据类型对象。复杂类型被建模为递归字典，例如结构体的区间表示为一个字典，包含其每个字段的区间，若为嵌套结构体则继续嵌套字典。

当前状态。我们的实现目前能够成功分析包含赋值和算术表达式的程序，支持基本类型和复杂类型。它考虑了状态变量、函数参数和局部变量。我们目前能够检测以下问题：

在本文中，我们识别出了一些当前最先进的智能合约分析工具未能处理的漏洞。这些漏洞的严重性各不相同，但无论影响大小，缺陷和潜在错误都应尽早被发现。我们尝试通过一种更强大的技术——区间分析（Interval Analysis）来改进 Slither。我们解释了为什么这种技术适合用于检测这些问题，以及它是如何检测这些问题的。我们在 Slither 的基础上构建了自定义的区间分析，利用 Slither 已经提供的关于合约、其属性、方法、方法参数、程序流程等信息。目前，我们的实现能够检测出其他工具遗漏的漏洞。

我们目前仅处理 Solidity 编程语言中部分表达式的情况，包括整数、布尔值、数组、结构体和映射等表达式。然而，要处理地址及其相关操作、更复杂的循环或条件语句等方面，还需要进行更深入的工作。目前，我们的代码可以在任何用 Solidity 编写的智能合约上执行，但只对我们所覆盖的子集进行区间分析。

过程内分析（Intraprocedural Analysis）将显著提高我们分析的精度。例如，我们尚无法检测的一种漏洞是短地址漏洞（Short Address），这可以通过监控 payload 的长度属性来检测。另一个例子是断言或 require 语句中的恒真与矛盾表达式，这可以通过近似布尔表达式的结果并检查区间是否仅包含一个值来检测：恒真为 true，矛盾为 false。

能够处理更复杂的条件语句和循环也将有助于通过解释布尔表达式的语义，更准确地监控程序状态。一旦我们根据条件分支识别出多个可能的状态，就可以利用如轨迹划分（Trace Partitioning）等统一技术。此外，监控隐式状态变量，如合约级别或函数级别的变量（例如 balance 或 msg.sender），也将有助于识别与余额相关的问题和用户交互问题。

[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课