Making Smart Contracts Smarter

Making Smart Contracts Smarter

论文标题：(2016-CCS) Making Smart Contracts Smarter ——使智能合约更智能

论文引用：Luu L, Chu D H, Olickel H, et al. Making smart contracts smarter[C]//Proceedings of the 2016 ACM SIGSAC conference on computer and communications security. 2016: 254-269.

代码开源：oyente: An Analysis Tool for Smart Contracts

主要内容

在本文中，作者研究了在类似加密货币的开放式分布式网络中基于以太坊运行智能合约的安全性。并且介绍了几个安全性问题，在这些问题中，对手可以操纵智能合约的执行以获取利益。这些错误表明在理解底层平台的分布式语义方面存在细微的差距。作者提出了增强以太坊操作语义的方法，以减少合同的脆弱性。对于为现有的以太坊系统写智能合约的开发人员，构建了一个名为Oyente的符号执行工具来发现潜在的安全漏洞。

在19366份现有以太坊合同中，Oyente标记其中8833份为易受攻击的合同，其中包括TheDAO错误，该错误导致2016年6月损失了6000万美元。

背景知识：符号执行

符号执行是一种传统的自动化漏洞挖掘技术, 目前也被广泛用于智能合约的漏洞挖掘。符号执行引擎为目标代码提供符号化的虚拟运行环境, 将程序所需的外部输入抽象为取值不固定的符号值, 并通过不断求解路径约束, 来尽可能的探索程序分支。

符号执行的主要思想是把程序执行过程中不确定的输入转换为符号值, 以推动程序执行与分析我们以下面代码为例, 对符号执行的基本流程进行解释。图1对应的示例代码如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
contract sample{        
	uint  g_var;          
	function  foo1(uint  m, uint n) public{         
		if(m > n){                         
			g_var  =  m;         
		}else{                         
			g_var  =  n;         
		}     
	}         
	function  foo2(uint  x) public{
    	if(g_var  <  x){
        	g_var  =  x;         
         }     
	} 
}

无论是智能合约还是传统平台中的程序, 都可以被抽象为一棵执行树。在正常的执行流程中, 由于程序输入为定值, 每个条件判断都可以得到确定的答案, 因此仅有一条分支被探索。

而在符号执行中, 输入值为不定的符号变量, 当遇到条件判断时, 符号执行引擎会利用约束求解器对包含符号变量的表达式进行求解。对于所有有解的分支, 符号执行都会进行分析, 并记录路径中的约束。

在上图中, 合约调用的输入有两个, 一个是待调用的函数, 一个是函数的输入。对于图1中的路径 1 来说, 当程序执行到叶子节点时, 该路径的约束有两个: [Func == foo1, m > n], m和n皆为符号化的输入值。对于符号执行来说, 智能合约与传统程序的差异主要在于合约中全局变量的取值是不确定的。因此通常情况下除了输入值, 智能合约的全局变量也需要被处理为符号值。

设计实现

Oyente

Oyente是在论文发表之后一段时间才由melon.fund于2018年10月发布的一款为现有的以太坊智能合约开发人员构建的符号执行工具，以发现智能合约中潜在的安全漏洞。其基本介绍：

  1. 开发语言：Python
  2. 工具类型：静态分析工具
  3. 分析内容：EVM字节码
  4. 工具原理：Oyente将需要分析的合约的字节码和当前以太坊的全局状态作为输入，检测合约是否存在安全问题，并向用户输入有问题的符号路径。在这个过程中，使用Z3求解器来确定可满足性。
  5. 模块划分：包含 4 个核心组件, 控制流图生成器(CFG Builder), 探索器(Explorer), 分析器(Core Analysis)和验证器(Validator)。

image-20201029221903218

  • 控制流图生成器（CFGBuilder）：对合约进行预分析, 为合约构建基本的控制流图, 以基本块为节点, 跳转关系为边；然而部分跳转关系并不能由生成器完全确定。

  • 探索器（Explorer）：对智能合约进行符号执行, 并在执行过程中将这些信息补齐。探索器承担着收集合约信息的重要责任, 它本质上是一个循环, 依次执行合约控制流图中各个基本块的代码。它利用 Z3 求解器对合约中的条件跳转进行求解, 探索器根据求解结果决定对哪个分支进行分析, 当条件跳转的两个分支条件都有解时, 两个分支都会被探索。

  • 分析器（CoreAnalsis）：包含用于检测合同的子组件，这些合同是TOD，与时间戳相关或异常处理的异常。Explorer仅收集表现出不同的以太流的路径。 因此，根据当交易顺序改变时发出的以太币是否不同来检测合约是否为TOD。 同样，如果要发送的条件包括块时间戳，我们将检查合同是否与时间戳相关。 我们描述了我们如何执行以下分析

    • TOD（transaction-ordering dependent）检测。 Explorer返回一组路径以及每个路径对应的以太流。 因此，我们的分析将检查两条不同的路径是否有不同的以太流。 如果合同中有这样的痕迹对，Oyente会将其报告为TOD合同。
    • 时间戳依赖性检测。 我们使用特殊的符号变量来表示块时间戳。 请注意，块时间戳在执行期间保持不变。 因此，给定轨迹的路径条件，我们检查是否包含此符号变量。 如果合同的任何跟踪依赖于此符号变量，则将合同标记为与时间戳相关。
    • 错误处理的异常。 检测错误处理的异常很简单。 回想一下，如果被调用方产生了例外，它将0推入调用方的操作数堆栈。 因此，我们仅需要在每次调用后检查合同是否执行ISZERO指令（该指令检查堆栈的最高值是否为0）。 如果不是，则忽略被调用方中发生的任何异常。 因此，我们将此类合同标记为处理异常的合同。
    • 重入检测。 我们利用路径条件来检查重入漏洞。 在遇到的每个CALL，我们在执行CALL之前获取执行的路径条件。 然后，我们检查这个条件带有更新变量（例如存储值）是否仍然成立（即，是否可以再次执行call 指令）。 如果是这样，我们认为这是一个漏洞，因为被调用者有可能在完成调用之前重新执行调用操作。

  • 验证器（Validator）：试图消除误报。 例如，假设CoreAnalysis将一个合同标记为TOD，并且其两条迹线t1和t2表现出不同的以太流量，验证器将查询Z3以检查排序（t1，t2）和（t2，t1）是否都可行。 如果不存在这样的t1和t2，则将该案例视为误报。 但是，由于我们还没有完全模拟以太坊的执行环境，Validator还远远不够完善。 对于第6节中介绍的结果，我们采用尽力而为的 手动分析来确认安全漏洞。 换句话说，Oyente当前的主要用途是标记潜在的易受攻击的合同。 全面的误报检测将留待以后的工作。

总结评价

1、Oyente是最早关注到自动化合约漏洞挖掘的工作之一, 提供了一个实现较为精简的合约符号执行引擎；尽管 Oyente 的部分检测方案并不完善, 涉及的漏洞也不够全面, 但依旧作为开创性的工作, 为后续研究提供了很好的支持。

2、Oyente 在论文中介绍了对条件竞争、时间戳依赖、未校验返回值以及重入漏洞等四种合约漏洞的检测方案，并在开源代码中进一步补充了整数上溢、整数下溢、调用栈溢出等常见漏洞的检测代码。