区块链研究实验室|以太坊自动静态分析（上）

区块链技术正在彻底改变分布式系统的格局， 利用概率保证和激励机制为共识问题提供创新的解决方案。它们允许在互不信任的各方之间安全执行付款；一些加密货币（比如比特币）仅提供一种针对支付而量身定制的脚本语言，其他的加密货币（比如以太坊）则支持完备的智能合约语言，允许高级应用程序，比如交易平台、选举、权限管理、数据管理系统或拍卖。

然而，随着智能合约日益复杂，黑客的可攻击面也在增长。由于智能合约控制着真实的资金流，因此成为黑客的核心目标。此外，由于区块链的不可更改性，智能合约一旦上传到区块链就无法修改，使安全漏洞的影响永久存在。这不仅是理论上的威胁，而且是一个实际问题。

如我们所见，黑客攻击往往一下子导致几百万美元的损失，真是臭名昭著。这种情况需要可靠的以太系统用户可访问的静态分析工具。开发者，他们需要能够在上传到区块链前验证他们的合同。以及与现有智能合同交互的用户，他们需要工具协助来评估这些合同（这些合同是以人类无法阅读字节码格式发布在区块链上的）是否具有欺诈性的。

漏洞查找工具Oyente(2016年发布)开创了以太智能合约(自动）静态分析的先河，它首次强调了通常影响智能合约的一般类型的bug，并提出了一种基于符号执行的检测工具。用于检测易受这些bug影响的合同。Oyente一个特别引人注目的特点是它是一个按钮工具，这不需要用户进行任何交互或对契约语义有更深入的了解。

然而，Oyente没有提供任何对报告结果的保证，既不可靠也不完整，因此只产生合同安全的启发式指示。鉴于严格的安全保障在这方面的重要性，后来提出了几种方法用于验证以太智能合约。具体地说，目的是机器检查智能合同审计一项工作专注于验证过程中的自动化，以确保可用性、适用性和广泛性。尽管进行了四年的深入研究，但是到目前为止，只有四个以太坊智能合约的这种合理且全自动的静态分析工作已经发表。此外，所有这些作品都存在缺点。最终破坏了他们旨在提供的安全保证。

以上的种种缺陷阻碍了静态分析的发展，对此，我们将会这篇文章的上篇首先简要介绍以太坊平台及其本机智能合约语言，通过概述该领域中的现有工作来进行自动智能合约验证，重点介绍其薄弱环节。

以太坊和EVM字节码语言

以太坊是继比特币之后第二个广泛使用的加密货币，市值超过140亿美元。以太坊之所以能够脱颖而出，是因为其富有表现性的脚本语言，使得能够执行任意分布式程序。以太坊智能合约以共同执行的字节码存储在区块链上由网络参与者（也称为节点）根据以太坊虚拟机（EVM）在以太坊的执行环境对不同的客户进行实施。

智能合约的执行是以太坊共识协议的一部分，系统状态由共同维护的操作决定；防篡改公共分类账，拥有一系列区块链交易。交易不仅可以汇款，还可以触发合同执行。为了导出系统的数据，每个节点都在本地执行EVM指定的区块链中的交易。这些交易被组装成块，附加到区块链。

通过以下方式确保系统的正确性验证所有块的节点，通过工作量证明机制建立公平性。只有节点能够解决计算难题的才有资格提出决策，这增加了随机性提议者的选择，并阻止少数人从指导系统的演变。

以太坊系统的状态（称为全局状态），由所有虚拟帐户的状态及其在虚拟帐户中的余额组成。智能合约是特殊账户实体（合约账户）除了余额之外，还可以保存持久性存储和合同代码。而非合约（所谓的外部）帐户可以主动转移其部分对于其他帐户的余额，合同帐户完全受其代码约束，合约账户可以通过另一个账户的交易来激活然后执行其代码，可能会转移资金或刺激其他人的合同。同样，可以代表外部帐户创建合同或通过其他合同。我们将在下文中提及这样的内部合同起源于外部帐户的，并明确记录在区块链上。

EVM字节码语言支持用于说明区块链生态系统的指定指令。这些包含用于各种形式的汇款，合同调用和合同创建。最突出的是，CALL指令允许将资金转移到另一个账户上，如果收款人是合同帐户，则同时触发代码执行。其他特定域的字节码包括说明用于访问区块链环境，例如SSTORE和SLOAD用于读取和写入持久性合同存储的单元格。此外，指令集包含用于访问有关正在进行的（内部）事务（其调用方，输入或传递的值）的信息以及用于人员分发。

EVM是基于堆栈的机器，支持用于算术和堆栈操作的标准指令。合同的控制流程也受基于堆栈的体系结构的约束，有条件和无条件跳转指令允许在另一个程序位置恢复执行由堆栈上的值确定。虽然这些功能会使EVM字节码图灵完成，以强制终止EVM smart的执行合同受预先指定的天然气资源限制。当耗尽指令时，每条指令都会消耗大量气体，并且执行会异常停止。天然气预算由交易发起者确定，交易发起者将支付补偿封闭区矿工的有效消耗执行交易时的天然气量。由于低级别的性质EVM字节码，智能合约通常以高级语言编写（最著名的是Solidity语言）并编译为EVM字节码。

ZEUS——自动声静力分析器

出于（显性或隐式）可靠性要求，EVM字节码需要依赖分析工具Securify，静态分析器ZEUS用于Solidity，Solidity将依赖语法指导分析器NeuCheck ，以及基于字节码的工具可达性分析工具EtherTrust。

Securify支持EVM字节码级别的数据和控制流分析。因此它从合同字节码重建控制流图（CFG），并将其转换为SSA形式。基于这种结构化格式，它可以建模使用逻辑谓词立即获得数据和控制流的依存关系，并建立数据记录样式的逻辑规则以导出传递依存关系，使用增强的数据记录引擎Souffle自动计算。对于检查不同的安全属性，Securify根据派生谓词，足以证明一种特性（合规模式）或显示出要破坏的特性（违反模式）。

ZEUS首先通过将Solidity合同翻译成中间语言LLVM代码，然后使用现成的模型检查器来分析Solidity合同验证不同的安全属性。在翻译过程中，ZEUS使用Solidity语言的另一个中间层，它引入了抽象，并允许将假设和断言插入到表示合同安全要求的程序代码。ZEUS支持的属性可能会转换为此类断言检查结合其他针对特定物业的合同转换。

NeuCheck通过对合同进行模式匹配来分析Solidity合同语法图。为此，它将Solidity源代码转换为XML解析树。安全属性在此解析树上表示为模式，并且与遍历树的自定义算法匹配。

EtherTrust通过将字节码执行语义抽象为（特定的）逻辑含义来对EVM字节码实施可达性分析，因此称为Horn子句的逻辑谓词，代表逻辑的执行状态合同。安全属性表示为逻辑上的可达性查询谓词并由SMT求解器z3求解。

这部分我们介绍了以太坊及其EVM字节码语言与自动静态分析的工具，下篇我们将会重点总结我们在设计eThor的经验，并分享我们认为对提高效率和稳健性起到至关重要作用的组件与实施策略。