Making Smart Contracts Smarter

这篇工作发表于big4 CCS16，一作是来自NUS的Loi Luu

本文针对以太坊智能合约的安全问题展开研究，介绍了智能合约运行时的若干安全问题。作为改进，提出了增强以太坊的操作语义的方法，使智能合约更不容易受到攻击。

对于智能合约开发者，本文提出了Oyente，采用符号执行的方法进行智能合约潜在安全漏洞的查找。实验部分针对19366个合约进行分析，Oyente标记了8833个合约为有风险的。

同时还讨论了几个案例研究中其他攻击的严重程度，这些案例研究有源代码可用，并在主要的以太坊网络中确认了攻击。

Introduction

区块链用户通过向智能合约地址发布交易（交易的接受者是合约地址）来调用合约，当交易被确认后，所有参与者在当前区块链的状态下，以交易负载作为输入执行合约代码，通过共识协议对输出和合约的下一个状态达成一致

过去6个月，约15000个智能合约在以太坊中部署

智能合约的安全问题

不同于传统的分布式应用，以太坊网络是无授权的

任意敌手可能能够操纵合约执行（允许矿工选择打包哪些交易，交易的顺序，区块时间戳）

不像传统的分布式应用可以通过发布补丁来修复错误，智能合约是不可逆转、不可篡改的

因此，设计安全的智能合约系统和合约部署前的正确性推理都是至关重要的

作者认为出现安全问题的原因是合约编写者对底层执行语义的假设与智能合约系统的实际语义之间存在语义差距。

对于时间戳依赖和交易顺序依赖攻击，作者认为他们是第一个提出这个问题的团队；对于其他一些前人已经提出的问题（异常处理和逻辑漏洞），本文分析了这些攻击的影响

本文的工作强调了智能合约语义中微妙或缺失的抽象，这些抽象导致开发人员产生了虚假的安全感。我们提出了对以太坊协议的改进，这些改进不需要对现有智能合约进行更改，然而这种更改需要所有客户端更新，实际不太可能部署。因此提出了Oyente进行部署前的漏洞检测。

Oyente针对以太坊智能合约进行符号验证，直接采用字节码，不需要高层的表达（Solidity，Serpent），因为以太坊本身只存储合约的EVM字节码

贡献

列出了以太坊智能合约新类型的安全漏洞
形式化了以太坊智能合约的语义，为列出的漏洞给出了修改建议
提出了Oyente，一种采用符号执行检测以太坊智能合约漏洞的工具
在真实的以太坊合约上运行了Oyente，并确认了攻击

BACKGROUND

Consensus Protocol

区块链的状态$\sigma$是地址到账户的映射，地址为$\gamma$的账户的状态是$\sigma [\gamma]$

不同于比特币账户仅持有币，以太坊地址支持智能合约账户，包括币、EVM字节码和永久私有存储

从概念上，以太坊可以理解为一种基于交易的状态机，$\sigma \mathop{\to}\limits^T \sigma’ $

Smart Contracts in Ethereum

一个智能合约的状态包括：

私有存储
余额：ether的数量

用户通过向合约地址发送交易（以太币+输入）来调用合约

以太坊字节码的每一条指令均有预先定义的gas，当用户发送交易调用合约时，需要向矿工支付gas进行补偿。交易发送这设置gasLimit和gasPrice。如果实际的gas消耗大于gasLimit，仍然会被扣除gasLimit的gas然后不执行。

SECURITY BUGS IN CONTRACTS

Transaction-Ordering Dependence

考虑到区块内包含若干交易，如果存在新的区块内包含对同一个合约的两次调用，用户无法得知自己调用时合约的状态，只有打包的矿工可以决定交易的顺序，也就是状态的更新顺序

考虑两个交易分别由owner和任意参与者发起，交易顺序决定了参与者拿到的ether的数量
- 如果owner恶意，观察到有交易调用合约时，将奖励修改为0，有一定概率会获利
- 和miner合谋就更容易获利了

Timestamp Dependence

其中的other contract variables like Last_payout which contribute to the generation of the random seed are also known.

Mishandled Exceptions

根据合约调用的方式，被调用合约中的异常可能会传播到调用者，也可能不会传播到调用者。

比如send后应检查返回值

国王被替代后会获得补偿，但是如果15行的send失败，会导致当前的国王失去补偿

一般发生在向动态地址发送ether，不知道该支付的gas。

Deliberately exceeding the call-stack depth limit

EVM限制调用栈深度为1024，如果通过call和send调用其他合约，栈深度加一

恶意敌手可以故意使得15行的send失败，但是无法获利

Reentrancy Vulnerability

TOWARDS A BETTER DESIGN

轻量化的定义捕捉了以太坊的关键

Operational Semantics of Ethereum

全局区块链的状态可以定义为$,\sigma$是状态，$\varGamma$是新交易集合

矿工形成和验证区块的操作如图所示。一次只有一个“当选领袖”成功执行Propose规则。领导者广播块B后，其他矿工使用Accept规则

安全问题：leader可能任意选择时间戳，存在TOD漏洞

以太坊中交易执行会访问三类空间：

操作数LIFO的栈
辅助内存$l$，无限增长的数组
合约的长期存储$str$，长期存储是持久性的，并且在交易之间保留其值。这使其适合存储需要在多次调用合约之间持久存在的数据。

定义虚拟机的执行状态 $\mu=,A$是调用栈

将交易抽象为一个三元组$$,$id$是调用合约的标识符，$v$是要存储进合约的金额，$l$是输入的参数

交易满足两个语义上的性质：

原子性：每个交易要么全部失败，要么全部执行。all or nothing
一致性：交易保证区块链系统从一个有效的状态到另一个有效的状态

本文将EVM抽象成了ETHERLITE，它是一个带有存储和一些类似以太坊的特性的堆栈机器。EtherLite的指令包括

call本质上类似于远程程序执行，第二行是调用栈溢出出现异常的情况；第二个return是正确返回的情况，EXC是返回异常

观察规则TX-EXCEPTION和EXC，前者仅放弃执行，后者返回0；因此交易不满足原子性

剩余3个指令：

suicide：将所有ether转移给接收者，终止当前合约；类似于call但不是call
create：创建新的和余额账户，接受3个参数；成功后返回合约的地址，失败返回flag 0;考虑如果合约初始化正在执行，但是没有实际的代码段；初始化失败，导致出现了zombie账户，存入的ether全部锁定，会破坏一致性
- 创建新的地址，分配存储，指定的ether存入该地址
- 初始化合约的存储
- 代码段存入合约
getstate：抽象指令，获得当前区块的时间戳，区块id等

Recommendations for Better Semantics

解决TOD——Guarded Transaactions

保证合约的调用结果不依赖于交易顺序

额外增加了保护条件$g$，即异常通过时需要满足$g$，如果$g$不满足，抛弃当前交易，默认为true，满足向后兼容

例子：在Puzzle合约中，用户发布交易可以指定$g\equiv(reward==R)$

“保护交易（guarded transactions）”类似于大多数现代处理器支持的“比较和交换（CAS）”指令。CAS是一个标准的多线程同步原语，而“保护事务”为以太坊提供了相同的能力。

确定性时间戳

允许合约获取区块时间戳实际上是一个冗余的特征，导致合约容易被敌手利用

时间戳一般用为以下2个途径：

作为确定性的随机种子：并不明智，熵太低，容易被操纵；作者给出了2个解决方案randao/randao: RANDAO: A DAO working as RNG of Ethereum (github.com)和On Bitcoin as a public randomness source (iacr.org)（从挖出的区块中提取熵的机制）
作为分布式网络中的全局时间

作者建议用区块的编号（索引）作为全局时钟，以太坊约12s产生一个区块

$timestamp - lastTime > 24 hours\to blockNumber - lastBlock > 7,200$

更好的异常处理

任何时候都检查返回值，目前Solidity编译器插入代码段进行异常转发，但是在call和send中不会增加

因此可以在EVM中增加throw和catch的指令，需要更新客户端

THE Oyente TOOL

Overview

之前提出的better design需要所有客户端更新，因此实际部署的可能性不高。因此作者提出了部署前的安全检查工具Oyente，能够实现

开发者写出更安全的合约
用户避免调用危险的合约

符号执行将程序变量的值表示为输入符号值的符号表达式。每个符号路径都有一个路径条件，它是一个公式，通过累积输入符号值必须满足的约束条件来构建。如果路径条件不可满足，则路径是不可行的。否则，路径是可行的。

静态地对程序进行推理，动态执行需要模拟EVM的运行，比传统的静态污点分析和一般的数据流分析的精度更高

输入包括字节码和以太坊的状态，输出合约是否有漏洞（3类），并输出有问题的符号路径

CFG作者期望后续可以作为交互式的debugger

Oyente解释EVM指令集，以准确地映射指令到约束条件，bit级准确度。

模块化设计：

CFGBuilder：构造CFG
Explorer：主要部分，符号化执行合约，输出发送给下一个模块
CoreAnalysis：采用逻辑匹配漏洞
Validator：筛选部分假阳

Implemantation

python 4000行代码

采用 Z3Prover/z3: The Z3 Theorem Prover (github.com)作为求解器判断可满足性

CFGBuilder：构建一个主要的控制流图，其中包含所有基本块作为节点，以及一些代表跳转的边，其目标可以通过在相应源节点上进行本地调查来确定。但是，在此阶段无法静态确定某些边，因此它们在后续的符号执行过程中动态构建。
Explorer：主要部分，从CFG入口开始，核心是一个解释器循环，获取要运行的状态，然后在该状态的上下文中符号执行单个指令。这个循环一直持续，直到没有剩余状态，或者达到用户定义的超时。
- 查询Z3来确定分支条件是否满足，进行条件跳转；
- 如果2个分支都满足，采用深度优先的方法都执行
- 解释阶段末，产生若干符号路径，Z3用于消除不可达的路径
CoreAnalysis：采用逻辑匹配漏洞，检查是否存在3类漏洞，目前仅分析有明确ehter流的路径
- TOD：当交易顺序改变后，发送ehter不同；即两条trace的ehter flow不一样
- 时间戳依赖漏洞：发送的条件包括时间戳，检测时时间戳不变，给定trace检查是否有时间戳
- 异常处理：被调用的合约异常时将0压入调用者的操作符栈，仅每次call后检查合约运行结果是否为0
- 重入漏洞：遇到每个call时，获得执行call前路径的条件；检查使用更新变量（例如存储值）的条件后是否依然满足。如果是，认为这是一个漏洞，因为被调用者可以在完成调用之前重新执行调用。
Validator：筛选部分假阳
- 询问Z3检查路径是否可达
- 不太完备，还需要手工进行假阳的分析