SAFEVM：以太坊智能合约的安全验证器

17.1 参考文献

Elvira Albert、Jesús Correas、Pablo Gordillo、Guillermo Román-Díez 和 Albert Rubio。 2019. SAFEVM：以太坊智能合约的安全验证器。 在第 28 届 ACM SIGSOFT 软件测试与分析国际研讨会 (ISSTA '19) 的会议记录中，2019 年 7 月 15 日至 19 日，中国北京。 ACM，美国纽约州纽约市，4 页。

17.2 总结

以太坊智能合约是公开的、不可变的和分布式的，因此它们很容易因开发人员的编程错误而出现漏洞。 本文介绍了 SAFEVM，这是一种用于以太坊智能合约的验证工具，它使用最先进的 C 程序验证引擎。 SAFEVM 将以太坊智能合约（以 Solidity 源代码或编译的 EVM 字节码的形式）作为输入，可选地带有断言和需求验证注释，并在输出中生成包含验证结果的报告。 除了常规的安全注释外，SAFEVM 还处理数组访问的验证：它自动生成 SV-COMP 验证语句，以便 C 验证引擎可以证明数组访问的安全性。 我们使用 CPAchecker、SeaHorn 和 VeryMax 作为后端验证器，通过实验评估从 etherscan.io（超过 24,000 个）中提取的所有合约。

17.3 SAFEVM 概述

每个区块链都提供自己的编程语言来实现智能合约。 Solidity 是一种图灵完备的语言，是为以太坊平台编写智能合约最流行的语言，然后将其编译为 EVM（以太坊虚拟机）字节码。 EVM 执行的每条指令都有以太坊指定的相关气体消耗。 安全是以太坊的主要关注点，Solidity 语言包含面向验证的函数、声明和要求，用于检查安全条件或要求以太坊交易软件，如果不满足则终止执行。 像往常一样，assert 函数可用于验证目的（例如，检查不变量），而 require 函数用于指定前提条件（例如，确保输入或合同状态变量的有效条件）。 将 Solidity 代码编译为 EVM 字节码时以太坊交易软件，要求条件被转换为测试，以检查条件和 REVERT 字节码是否为真。 REVERT 终止智能合约的整个执行，恢复状态，并将所有剩余的气体返回给发送者。 如果条件不为真，则使用断言检查条件，并调用 INVALID 字节码。 当INVALID被执行时，状态会恢复，但不会退还gas，所以后果比REVERT更严重：除了损失gas的经济后果外，唯一提供给交易的信息就是低gas错误信息。 数组访问的处理与声明相同。 当访问数组位置时，生成的 EVM 字节码会检查访问的位置是否在数组范围内，否则将执行 INVALID 字节码。 除法和相关字节码（如 MOD、SMOD、ADDMOD、MULMOD）也会导致在分母为零时执行 INVALID。

因此，无效的字节码是使以太坊智能合约合法化的关键，因为它们会被来自多个来源的断言违规和操作失误所捕获（例如，越界访问、被零除）。 因此，我们验证智能合约的方法是将智能合约的EVM字节码反编译成带有ERROR注解的C程序，这样就可以使用现有的C程序验证工具进行验证。 从低级 EVM 开发验证器具有以下优点：（i）有时源代码不可用（例如，区块链只存储字节码），（ii）在字节码级别只有 INVALID 字节码可见，我们可以各种安全问题得到统一处理，(iii) 我们的分析适用于可以编译到 EVM 的任何其他语言（例如 Vyper），并且不受源语言更改或编译器优化的影响。 好在现在有很多开源工具可以帮助我们反编译，并且都集成到了工具链中。

图 1 SAFEVM 的主要组件

图 1 描绘了 SAFEVM 的主要组件如下（阴影框是现成的二手系统）：（1）输入。 SAFEVM 使用智能合约，可选择使用断言并需要验证注释。 智能合约可以作为 Solidity 源代码或 EVM 编译代码提供，在后一种情况下，注释已被编译为字节代码，如上所述。 (2) CFG。 在任何一种形式中，代码都以符号形式提供给 Oyente 执行引擎，该引擎已扩展为从给定的智能合约计算完整的 CFG。 由于 Oyente 不处理递归函数，因此在此步骤中已将其丢弃。 本文未描述 CFG 生成阶段。 (3) 以太坊。 EthIR 将生成的 CFG 中的 EVM 字节码反编译为更高级别的基于规则的表示 (RBR)。 该阶段的技术细节在本文中不作描述。 (4) C+SV-COMP转换器。 我们已经将递归 RBR 表示的转换器实现为带有验证的抽象整数 C 程序（即所有数据都是整数类型）。 使用 SV-COMP 格式的注释。 我们还无法处理的 EVM 功能，例如按位运算，在转换中被抽象出来（参见第 IV 节）。 按照 SV-COMP 格式将 INVALID 指令转换为 C 程序中的 ERROR 注释。 (5) 验证。 任何带有 SV-COMP 注解的 Integer C 程序验证工具都可以用来验证我们的 C 转换合约的安全性。 我们使用三个最先进的 C 验证器、CPA Checker、VeryMax 和 SeaHorn 评估了我们的方法，并且我们处理了它们生成的验证报告以根据智能合约的功能报告结果。

我们的工具 SAFEVM 拥有庞大的（潜在）用户群，因为以太坊目前是编码和处理智能合约的最先进平台。 正如我们将在第五节中描述的那样，使用 SAFEVM，我们已经自动验证了大约 20% 的函数（取决于验证者）的安全性，这些函数可能会执行从 etherscan.io 中提取的整个合约（超过 24,000 个合约），并且发现了具有潜在无法验证潜力的功能漏洞。

17.4 使用 SV-COMP 注释转换为 C

作为一个激励性的例子，我们使用一个 Solidity 合约（可在 ）实现一个名为 SmartBillions 的彩票系统。 我们举例说明其内部函数commitDividend的安全验证，将剩余的分红承诺给用户wh。 通过从名称中删除元音，我们缩短了变量名称。

我们翻译的起点是 EthIR 制作的 RBR。 RBR 由一组规则组成，这些规则包含字节码指令的反编译版本（例如 LOAD 和 STORE 是反编译的指令），其规则调用结构是从 Oyente 生成的 CFG 中获得的。 RBR 可能包含两种规则：称为 blockX 的指令序列和称为 jumpX 的条件跳转规则，其第一条指令是布尔条件，用于在函数定义的规则之间进行选择。 本节的其余部分说明了从 RBR 转换为抽象整数 C 程序的四个主要阶段。

(1) C 函数：对于 RBR 中的每个非递归规则定义，我们的转换将生成一个没有参数且返回 void 的 C 函数。 循环产生的递归规则被转换为迭代代码。 对于这部分转换，我们从 CFG 计算 SCC 并通过 goto 指令对检测到的循环建模。

(2) 变量的类型：原始类型、有符号和无符号数据类型以无类型的256位字存储在EVM字节码中，字节码不包含变量实际类型的信息。 此外，除了少数特定的签名操作（SLT、SGT、SIGNEXTEND、SDIV 和 SMOD）外，大多数 EVM 操作不区分它们。 由于验证器在溢出时的行为不同，我们的翻译允许用户选择（通过标志）是将 C 程序中的所有变量声明为 int 类型还是为特定标志操作声明 unsigned int 类型（将其转换为 int）。

(3) 变量定义：为了在验证过程中能够在它们的范围内进行推理，SAFEVM 在 C 程序中将它们翻译如下： (i) 在展平执行堆栈时，我们将堆栈变量声明为全局 C 变量。 使它们可用于所有 C 函数。 这些变量不需要初始化，因为它们从程序代码中取值。 (ii) 将局部变量定义为全局 C 变量，因为合约的函数可能会被翻译成多个 C 函数，并且都需要访问局部数据。 它们在与首次使用它们的块相对应的函数的开头进行初始化。 (iii) 状态变量也被转换为所有函数都可以访问的全局变量，由于函数验证时其值是未知的，所以用_VERIFIERnondet_int初始化； (iv) 函数输入参数也定义为全局变量。

(4) SV-COMP 注：以太坊智能合约的验证是在SAFEVM中通过C转换代码保证NVALID操作的不可达性来完成的。 按照 SV-COMP 规则，我们将 INVALID 操作转换为对 VERIFIERerror 函数的调用。

17.5 实验评价

SAFEVM 的所有组件（C 验证器除外）都是用 Python 实现的，并且是开源的。 SAFEVM 接受以最高版本 0.4.25 的 Solidity 编写的智能合约和以太坊虚拟机 v1.8.18 的字节码。 本节报告使用 SAFEVM 和 CPAchecker、SeaHorn 和 VeryMax 作为验证后端的实验评估结果。 具体的评价结果​​数据可以通过阅读原文获得。

从评估数据来看，我们认为虽然准确率还有很大的提升空间，但我们的实验评估结果是令人鼓舞的：我们验证了安全性。 通过使用最新的验证器，大约 20% 的函数可能会完全自动到达 INVALID 的 INVALID 字节码。

17.6 结论

据我们所知，SAFEVM 是第一个使用为 C 程序开发的现有验证引擎来验证低级 EVM 代码的工具。 这为验证 C 程序开发的先进技术适用于编码智能合约的新语言打开了大门。 虽然我们的工具仍处于原型阶段，但它提供了转换方法的概念验证，我们相信它为构建 EVM 智能合约验证工具提供了一个有前途的基础。 我们打算在未来工作中改进的一些方面是处理存储在内存中的数据，因为一旦存储在内存中，SAFEVM 就会使用 EthIR 组件将其抽象出来。 为 EVM 智能合约开发内存分析对于验证准确性至关重要。 我们还旨在处理未来在 EVM 字节码中广泛使用的位操作。 使用数组和映射（以太坊智能合约中唯一可用的数据结构）的高级推理也可以添加到框架中以提高准确性。 这也需要在反编译方面做进一步的工作。 同样，在反编译过程中学习有关变量类型的信息将对验证过程的准确性产生影响。

本文由南京大学软件学院2016级本科生曹家伟转载。