原创 securify：以太坊智能合约的实证安全分析

无许可区块链允许执行任意程序(称为智能合约)，允许相互不可信的实体在不依赖可信第三方的情况下进行交互。尽管存在这样的潜力，但不断出现的安全担忧已经动摇了人们对通过智能合同处理数十亿美元资产的信心。

为了解决这个问题，我们提出了SECURIFY，这是一个为以太坊智能合约提供的安全分析程序，它是可伸缩的、完全自动化的，并且能够证明对于给定的属性，合约行为是安全的/不安全的。SECURIFY的分析包括两个步骤。首先，它象征性地分析合约的依赖关系图，以从代码中提取精确的语义信息。然后，它检查遵从性和违反模式，这些模式捕获了足够的条件来证明属性是否具有。为了支持可扩展性，所有模式都是用指定的领域特定语言指定的

10.2.1引文：

区块链平台，如中本聪的比特币，使相互不信任的各方能够进行加密货币的交易。为了消除对信任的需求，他设计了一个对等网络，使其同行能够就交易达成一致。之后，由于分散计算在交易之外的适用性， Ethereum区块链被设计出来，它支持用图灵完备语言编写的程序(称为智能合约)的执行。

越来越多地采用智能合同需要强有力的安全保障。不幸的是，创建没有安全漏洞的智能合约非常具有挑战性。因此，智能契约中的关键漏洞每隔几个月就会被发现和利用。

为智能合约创建一个有效的安全分析器的主要挑战是编程语言的图灵完整性，它使得对任意属性的自动验证不可判定。为了解决这个问题，目前的自动化解决方案往往依赖于相当通用的测试和符号执行方法。这些方法有几个缺点i)他们可以错过关键违规(ii),也可以产生假阳性和(iii)他们能不能达到足够的代码覆盖现实合约。总的来说，这些缺陷给用户带来了很大的负担，他们必须检查所有报告是否有错误警报，并担心未报告的漏洞。实际上，智能契约的许多安全属性本来就很难直接推理。解决这些挑战的可行途径是构建一个针对重要领域特定属性的自动验证器。

对这项工作的一个关键观察是，通常可以设计出在合约的数据流图上表示的精确模式，其中模式的匹配意味着违反或满足原始安全属性。例如，在Ethereum智能合约中的所有调用中，有90.9%可以通过匹配一个模式来证明没有臭名昭著的DAO bug，该模式声明调用之后没有写入存储。之所以能够建立这样的对应关系，是因为在实际契约中，对原始属性的违反往往会违反一个简单得多的属性。实际上，就验证而言，使用模式而不是使用它们相应的属性的一个关键好处是，模式实际上更适合自动推理。

基于以上认识，我们开发了SECURIFY，一个轻量级的、可伸缩的以太坊智能合约安全验证器。关键的技术思想是定义两种模式来反映给定的安全属性i)遵从模式，这意味着属性的满足;(ii)违反模式，这意味着属性的否定。

与现有的智能合同符号分析仪相比，SECURIFY减少了两种方式检查报告所需的努力。首先，现有的分析程序没有报告明确的违规，因此要求用户手动将所有报告的漏洞分类为真阳性或假阳性。相比之下，SECURIFY会自动对被担保为违规的行为进行分类。因此，用户只需要手动将警告分类为真或假阳。

10.2.2SECURIFY系统介绍

SECURIFY的输入是合约的EVM字节码和一组安全模式，在我们指定的领域特定语言中指定。SECURIFY也可以作为以可靠形式编写的输入契约，这些契约在进行分析之前被编译为EVM字节码。有两种安全模式:遵从性模式和违反模式，它们捕获足够的条件来确保合约满足给定的安全属性，并分别违反给定的安全属性。

要发现合约中不受限制的条款，SECURIFY主要有以下三个步骤

第一步:反编译EVM字节码。SECURIFY首先将作为输入提供的EVM字节码转换为静态单分配表单中的无堆栈表示形式。

第二步:推断语义事实。反编译之后，SECURIFY分析契约，以推断语义事实，包括数据和控制流依赖关系，它们控制契约的所有行为。

语义事实的SECURIFY派生在分层数据中声明性地指定，并使用现有的可伸缩引擎实现完全自动化。声明式方法的主要优点是i)推理规则简明地捕获关于不同组件的抽象推理;(ii)可以轻松添加更多的事实和推理规则;(iii)推理规则以模块化的方式指定。

第三步:检查安全模式。在获得语义事实之后，SECURIFY检查作为输入的遵从性和违反安全性模式集。这些模式是用特定于领域的专用语言(DSL)编写的，这使安全专家能够使用定制的模式扩展我们的内置模式集。我们的DSL是通过SECURIFY推断出的语义事实的逻辑公式片段。

我们注意到，在进行安全审计时，安全专家有时会添加特定于合约的模式。例如,它经常需要检查没有不良的依赖关系,如:只有主人可以修改某些值的存储,或确保特定算术表达式的结果不依赖于部门指令。

对于任何违反模式的匹配，SECURIFY输出导致该模式匹配的指令。它突出显示了指令sstore(c, b)。此外，对于违反或合规模式都不匹配的任何财产，证券化都会输出警告，表明它未能证明或反驳该财产。

我们简要总结了SECURIFY的几个局限性。首先，当前版本的SECURIFY无法对溢出等数值属性进行推理。为了解决这一局限性，我们计划将SECURIFY扩展到数值分析，这不仅可以提高SECURIFY的精度，而且可以检查数值属性。

其次，SECURIFY不考虑可达性，而是假设合同中的所有指令都是可达的。这一假设对于在SECURIFY所支持的证券属性与用来证明和反驳它们的模式之间建立正式的对应关系是必要的。

最后，我们认为捕获违规的属性常常会被攻击者利用，但并不总是如此。例如，契约中的某些字段必须是所有用户都可以通用编写的。为了解决这个问题，安全专家可以在SECURIFY的DSL中编写特定于契约的模式。

10.3语义事实

在本节中，我们将介绍SECURIFY所使用的控制和数据流依赖关系的自动推理。在此过程中推断的事实称为语义事实，稍后将用于检查安全性属性。我们从理解这个分析所必需的背景开始:EVM指令集和分层数据。然后，我们将介绍SECURIFY派生的语义事实，以及分层数据中指定的用于派生这些事实的声明推理规则。

10.3.1背景

Ethereum虚拟机(EVM)。智能合约是在区块链上执行的。当用户提交指定合约、要运行的方法和方法参数的事务时，将执行合约。当事务被处理时，它被添加到区块链的新块中。合约可以访问易失性内存和非易失性存储。EVM指令集支持几十个操作码。SECURIFY处理所有EVM操作码。

分层数据日志。分层数据日志是一种声明性逻辑语言，它支持编写事实和规则来推断事实。接下来，我们将简要概述它的语法和语义。

语法。我们在图10-1中给出了Datalog s语法。Datalog程序由一个或多个规则组成，用r表示。规则r由头部A和体l组成，体l由文字组成，中间用逗号分隔。头部，也称为原子，是零个或多个术语上的谓词，表示为t，逗号分隔。字面量l是一个谓词或它的否定。按照惯例，我们用大写字母写Datalog变量，用小写字母写常量。

图10-1

语义。设

(其中t是由逗号分隔的术语列表)表示所有ground原子;我们把这些称为事实。解释是一组事实。完全格

对的解释集部分排序。

给定一个替换变量映射到常数,一个原子,我们写σ(a)获得的事实根据σ替换的变量。例如,σ(p (X))返回的p(σ(X))。给定一个程序P，其结果运算符定义为

10.3.2事实与推理规则

SECURIFY首先提取一组适用于每条指令的基本事实。这些基本事实构成一个Datalog输入，该输入被输入到Datalog程序中，以推断关于合同的其他事实。我们使用术语语义事实来引用Datalog程序派生的事实。出现在契约中的所有程序元素，包括指令标签、变量、字段、字符串和整数常量，都表示为Datalog程序中的常量。

基本事实。我们推理机的基本事实描述了合同控制流程图(CFG)中的指令。基本事实以，其中instr是指令名，L是指令s标签，Y是存储指令结果的变量(如果有的话)，是作为参数给指令的变量。

连续指令的基本事实由在称为Follow的标签上定义的谓词表示。对于每两个标签，L1和L2，它们的指令在CFG中是连续的(要么在相同的基本块中，要么在链接的基本块中)，我们都有基本事实Follow(L1, L2)。

Flow-Dependency谓词。我们考虑的流谓词是MayFollow和MustFollow，它们都是在一对标签上定义的，并从合约CFG中推断。

为了推断MayFollow和MustFollow谓词，我们使用Follow(L1, L2)输入事实，如果CFG中L2紧跟L1，则该事实成立。也就是说，谓词MayFollow是由以下两个Datalog规则定义的：

第一条规则解释为:如果Follow(L1, L2)成立(即:，它包含在Datalog输入中)，然后导出谓词MayFollow(L1, L2)(即，它被添加到定点)。第二个规则被解释为:如果MayFollow(L1, L3)和Follow(L3, L2)都成立，那么就派生出MayFollow(L1, L2)。注意，如果在定点计算中(定点计算结束时)没有派生出MayFollow(L1, L2)，那么在执行任何合约时，标记L2处的指令不会出现在标记L1处的指令之后。

10.4安全模式

在本节中，我们将展示如何在语义事实之上表达安全模式。我们首先定义表示安全模式的SECURIFY语言。然后，为了形式化地定义安全属性，我们提供了EVM契约执行语义的背景知识，并形式化地定义了属性。我们继续展示一组相关的安全属性，对于每一个属性，我们都显示遵从性和违反模式，它们分别表示属性及其否定性。这种构造使我们能够确定合同是否符合或违反给定的安全属性。最后，我们将展示SECURIFY如何利用一些模式来进行错误定位。

10.4.1语言安全

我们首先定义用于编写模式的语言的语法，然后定义如何根据给定契约派生的语义事实解释模式。

语法。SECURIFY语言的语法由以下BNF给出：

语义。模式是通过检查推断的语义事实来解释的：

量词和连接器按通常的方法被解释。流和数据依赖谓词的解释当且仅当它包含在Datalog定点中时，语义事实才成立。

10.4.2EVM背景和属性

EVM语义。契约是EVM指令序列。契约的语义是初始状态的所有跟踪的集合。跟踪合同的C是一系列state-instruction 。从一个初始状态σ0,这样的关系是根据EVM有效的执行语义。

属性。属性是一组跟踪上的关系。合同满足安全属性我们说C违反房地产ρ。我们使用一阶逻辑公式定义关系。公式通过由用户标识符、偏移量和EVM指令的其他参数或返回值组成的跟踪和位串来解释。我们用t1 t2…引用跟踪的变量。我们用i1 i2…引用跟踪中一对的索引的变量。我们对位串变量使用其他字母。

10.4.3安全属性和模式

Ether动性(LQ)。我们定义此安全性属性通过要求(i)所有跟踪t不改变契约的余额，或者(ii)存在一个减少契约余额的跟踪t。

调用后无写操作（NW）。首先，调用指令在执行时使调用的接收者能够在返回到契约之前执行自己的代码。其次，此调用传输的数量取决于存储值，存储值在此调用之后更新。这个值非常重要，因为它记录了调用方在合同中拥有的ether的数量，因此可以请求接收ether。

受限制的写操作（RW）。攻击者利用了契约对库的依赖，库可以无条件地将所有者字段设置为任何地址。这使得攻击者能够获得契约的所有权并窃取它的ether。

受限制的发送(RT)。我们定义了一个属性，它保证ether传输(通过调用)不能被任何用户a调用

异常处理（HE）。我们的遵从性模式检查调用指令之后是否遵循goto指令，该指令的条件由调用的返回代码决定

交易顺序依赖（TOD）。我们的遵从性模式要求调用指令发送的ether量独立于存储状态和契约余额。

参数验证（VA）。我们的遵从性模式检查在持久性内存中存储一个可能依赖于方法参数的变量之前，是否存在对参数值的检查。

10.5主要贡献

我们提出了SECUIFY，一个新的轻量级和可伸缩的验证Ethereum智能合同。SECUIFY利用了特定于领域的洞见，即对智能合约的许多实际属性的违反，也违反了更简单的属性，而这些更简单的属性以一种完全自动化的方式检查起来要容易得多。基于这一认识，我们设计了遵从性和违反模式，这些模式可以有效地证明现实世界中的合同是否与相关属性相关是安全的/不安全的。总的来说，证券化有几个重要的好处:

(一) 分析所有合同行为，避免不必要的虚假否定;

(二) 确保某些行为是实际错误，从而减少用户将警告分为真报警和假报警的工作量;它支持一种新的特定于领域的语言，使用户能够在出现新的漏洞模式时加以表示;最后，它的分析管道——从字节码反编译、优化到模式检查——是完全自动化的，使用可伸缩的现成Datalog解决方案。