17.1引用
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Al- bert Rubio. 2019. SAFEVM: A Safety Verifier for Ethereum Smart Contracts. In Proceedings of the 28th ACM SIGSOFT International Symposium on Soft- ware Testing and Analysis (ISSTA ’19), July 15–19, 2019, Beijing, China. ACM, New York, NY, USA, 4 pages. https://doi.org/10.1145/3293882.3338999
17.2摘要
以太坊智能合约是公开的，不可变的和分布式的，因此，它们很容易因开发人员的编程错误而产生漏洞。本文介绍了SAFEVM，这是一种用于以太坊智能合约的验证工具，它使用了针对C程序的最新验证引擎。SAFEVM将以太坊智能合约（以Solidity源代码或编译的EVM字节码形式）作为输入，并可选地使用断言和要求验证注释，并在输出中生成带有验证结果的报告。除了常规安全注释外，SAFEVM还处理阵列访问的验证：它会自动生成SV-COMP验证声明，以便C验证引擎可以证明阵列访问的安全性。我们使用CPAchecker，SeaHorn和VeryMax作为后端验证程序，对从etherscan.io（超过24,000个）中提取的所有合同进行了实验评估。
17.3 SAFEVM概述
每个区块链提供其自己的编程语言来实现智能合约。Solidity是一种Turing完整的语言，是为以太坊平台编写智能合约然后被编译为EVM（以太坊虚拟机）字节码的最流行的语言。 EVM执行的每条指令都有以太坊指定的相关汽油消耗量。安全性是以太坊的主要关注点，Solidity语言包含面向验证的功能、声明和要求，以检查安全条件或要求并在不满足安全条件或要求时终止执行。像往常一样，assert函数可用于验证目的（例如，检查不变量），而require函数用于指定前提条件（例如，确保输入或合同状态变量的有效条件）。当将Solidity代码编译为EVM字节码时，require条件将转换为检查条件和REVERT字节码是否成立的测试。REVERT终止智能合约的整个执行，恢复状态，并将所有剩余的燃料退还给者。如果条件不成立，则使用断言检查条件，并调用INVALID字节码。当执行INVALID时，状态将被还原，但不会退还任何燃料，因此，其后果比REVERT更为严重：除了失去燃料的经济后果外，唯一提供给交易的信息是燃料不足的错误消息。对数组访问的处理与声明相同，在访问数组位置时，生成的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。 EthIR 从生成的CFG中将EVM字节码反编译为更高级别的基于规则的表示（RBR）。该阶段的技术细节未在本文中描述。（4）C + SV-COMP转换器。我们已将用于递归RBR表示的转换器实现为带有验证的抽象Integer C程序（即，所有数据均为Integer类型）。使用SV-COMP格式的注释。我们尚无法处理的EVM功能（例如按位操作）在转换中被抽象化了（请参见第四节）。遵循SV-COMP格式，在C程序中将INVALID指令转换为ERROR注释。（5）验证。任何使用SV-COMP注释的Integer C程序Verification工具都可以用来验证我们C转换合同的安全性。我们已经使用三个最先进的C验证器，CPA检查器，VeryMax和SeaHorn评估了我们的方法，并且我们处理了它们生成的验证报告以根据智能合约的功能报告结果。
我们的工具SAFEVM具有庞大的（潜在）用户群，因为以太坊目前是用于编码和处理智能合约的最先进的平台。正如我们将在第五节中描述的那样，使用SAFEVM，我们已经自动验证了大约20％的功能的安全性（取决于验证者），这些功能可能会执行从etherscan.io提取的整个合同（超过24,000个合同）中的INVALID字节码，并且发现了潜力无法验证的功能漏洞。
17.4 使用SV-COMP注释转换成C
作为激励示例，我们使用实现了称为SmartBillions的彩票系统的Solidity合同（可从https://smartbillions.com/获得）。我们说明了对其内部功能commitDividend的安全性验证，该函数将剩余的红利提交给用户wh。通过从名称中删除元音，我们缩短了变量名称。
我们翻译器的起点是EthIR生产的RBR。 RBR由一组规则组成，这些规则包含字节码指令的反编译版本（例如LOAD和STORE被反编译ssignments），其规则调用的结构是从Oyente生成的CFG中获得的。 RBR可能包含两种规则：称为blockX的指令序列和名为jumpX的条件跳转规则，其第一条指令是用于在函数定义的规则之间进行选择的布尔条件。本节的其余部分说明了从RBR到抽象Integer C程序的转换的四个主要阶段。
（1）C函数：对于RBR中的每个非递归规则定义，我们的转换都将产生一个C函数，该函数没有返回void的参数。循环产生的递归规则将转换为迭代代码。对于转换的这一部分，我们根据CFG计算SCC，并通过goto指令对检测到的循环进行建模。
（2）变量的类型：基本类型，有符号和无符号数据类型存储在EVM字节码中的无类型256位字中，并且字节码不包含有关变量实际类型的信息。此外，除了少数特定的签名操作（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注释：通过保证C转换代码中NVALID操作的不可达性，在SAFEVM中完成对以太坊智能合约的验证。跟随SV-COMP规则，我们将INVALID操作转换为对VERIFIERerror函数的调用。
17.5 实验评估
SAFEVM的所有组件（除C验证程序外）均以Python实现，并且是开源的。 SAFEVM接受以Solidity最高版本0.4.25编写的智能合约以及以太坊虚拟机v1.8.18的字节码。 本节报告使用SAFEVM和CPAchecker，SeaHorn和VeryMax作为验证后端的实验评估结果。具体评估结果数据可以阅读原文获取。
从评估数据看来，我们认为尽管有很多提高精度的空间，但我们的实验评估结果令人鼓舞：我们已经验证了安全性。 通过使用最新的验证程序，大约20％的功能可能会完全自动达到INVALID的INVALID字节码。
17.6 结论
据我们所知，SAFEVM是第一个使用为C程序开发的现有验证引擎来验证低级EVM代码的工具。这为验证C程序而开发的先进技术的适用性打开了大门，这些先进技术可用于对智能合约进行编码的新语言。尽管我们的工具仍处于原型阶段，但它提供了转换方法的概念验证，并且我们认为它为构建EVM智能合约的验证工具提供了有希望的基础。我们打算在将来的工作中改进的一些方面是处理存储在内存中的数据，因为一旦内存上进行存储操作，SAFEVM就会使用EthIR组件将其抽象化。为EVM智能合约开发内存分析对于验证准确性至关重要。我们还旨在将来处理EVM字节码中广泛使用的按位操作。数组和地图的高级推理（以太坊智能合约中唯一可用的数据结构）也可以添加到框架中，以提高准确性。这也需要反编译方面的进一步工作。同样，在反编译期间学习有关变量类型的信息将对验证过程的准确性产生影响。
本文由南京大学软件学院2016级本科生曹佳玮转述。
添加新手交流群：币种分析、每日早晚盘分析
添加助理微信，一对一亲自指导：YoYo8abc
