Catalog

[TOC]

Papers Link

TEETHER:Gnawing at Ethereum to Automatically Exploit Smart Contracts

Introduction

Motivation

Background

​ 以太坊是继比特币之后第二大的的区块链实现平台，提供了图灵完备的编程语言Solidity进行区块链应用的编写。这也造成了给攻击者途径去进行攻击。在本论文中考虑如何在给定的智能合约当中自动的生成合约漏洞。

Literature Review

已经存在很多种工具对智能合约进行漏洞的检测：

1. OYENTE：利用符号执行的方法对智能合约进行漏洞检测
2. ZEUS：将智能合约编译后的字节码转换了中间语言LLVM，然后进行漏洞检测
3. SmartCheck：将智能合约源代码转换了XML，利用XPath方法对智能合约进行漏洞检测

Research Niche

​ 因为智能合约一旦部署就不能修改，这就导致软件漏洞以及巨大的经济损失，事实上到2015为止，这些问题就导致了数千万美元的经济损失。随着以太坊的流行，这种影响会变得越来越大。

Work

Research Objectives

本文的主要目的：

1. 给智能合约漏洞提供一种通用的定义
2. 对由漏洞的智能合约自动生成能够造成攻击的路径方法。

Challenge

1. 如何去构造智能合约的CFG图
2. 如何去查找和搜索关键路径
3. 如何生成关键路径的约束问题
4. 如何更短的时间内对约束进行求解
5. 如何对在符号执行中处理Hash的问题

Insight

检测工具的核心方法：符号执行

Research summary

具体流程如下：

1. 首先对收集智能合约的字节码
2. 对字节码形式的智能合约进行CFG构图
3. 之后在CFG图中扫描寻找关键指令集
4. 每当扫描到关键指令时，进行关键路径构造
5. 根据关键路径生成路径约束——即符号执行的相关内存
6. 最后使用Z3求解器对约束进行求解。

Evaluation

Evaluation Summary

本文作者与现有的漏洞检测工具进行比较：

1. 与OYENTE进行比较
   • OYENTE只是考虑了个别特殊的漏洞，其中许多漏洞只能让而已的矿工所利用。
   • OYENTE只对漏洞进行检测，并没有生成一条可触发漏洞的例子
2. 与ZEUS进行比较
   • 与OYENTE一样，ZEUS只是提供已知道的漏洞
   • ZEUS编写的约束必须要在知道源代码的情况下编写
   • ZEUS发现的策略违反并不意味着这份合约真正存在漏洞

Implications

因此得出，TEETHER的优点：

1. 对已知或者未知的漏洞进行检测
2. 仅在提供字节码的情况下也能对合约进行检测
3. 检测出这些漏洞自动生成用例，有助于开发者发现漏洞与修复漏洞

Novelty

Contributions

1. 基于EVM底层的指令集，给出了智能合约漏洞的一般定义
2. 在仅仅提供智能合约字节码的基础上，如果自动生成可运行的漏洞。并解决符号执行中的Hash值的问题
3. 我们对38757分独立的合约进行了漏洞检查与分析

Limitations

1. 对漏洞的定义太广，凡是合约中包含指令集CALL、SELFDESTRUCT、CALLCODE、DELEGATECALL都被认为是脆弱的合约，因此关键路径的寻找空间过大
2. 耗时是此工具的最大限制，由于寻找解的时间过长，实验中，理应完成38757份合约的检测，但33195份合于在指定的时间内检测完毕

Key Concepts

符号执行(Symbolic execution)

​ 符号执行是一种程序分析技术，它可以通过分析程序来让特定代码区域执行的输入。顾名思义，使用符号执行分析一个程序时，该程序使用符号值作为输入，而非一般执行程序时使用的具体值。在打到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。

Z3

​ Z3是由微软公司开发的一个优秀的SMT求解器(也就是定理证明器)，它能够检查逻辑表达式的可满足性。python有库进行调用。

​ 解释：函数 Int(‘x’) 创建了一个Z3的整型变量x，求解函数求解一个约束(constraints)系统。本例创建了两个变量x和y，和三个约束，Z3Py和Python一样，使用 = 来赋值，使用 < , <=, >, >=, == 和 != 来比较。

​ 上述的输出为：[ x = 3 , y = 2 ]

A*算法具体参考

输入：起点（初始状态）和终点（目标状态），以及两点间所有可能的路径，以及涉及到的中间节点（中间状态），每两个节点间的路径的代价。（一般还需要某种启发函数，即从任意节点到终点的近似代价，启发函数能够非常快速的估算出该代价值。）

输出：输出是从起点到终点的最优路径，即代价最小。同时，好的启发函数将使得这一搜索运算尽可能高效，即搜索尽量少的节点/可能的路径。

公式：f(n)=g(n)+h(n)

• f(n) 是从初始状态经由状态n到目标状态的代价估计
• g(n) 是在状态空间中从初始状态到状态n的实际代价
• h(n) 是从状态n到目标状态的最佳路径的估计代价

Solidity——mapping类型

​ 提供一种键值对的映射关系存储结构，定义方式为mapping(_KeyType=>_KeyValue)。如：mapping( uint => string) idName;

​ 值得注意的是，在映射表中，并不存储键的数据，仅仅存储它的keccak256哈希值，这个哈希值在查找值时需要用到。正因如此，映射是没有长度的，也没有键集合和值集合的概念

The End

广州市云计算安全与测评技术重点实验室

华南师大-唯链区块链技术与应用联合实验室

粤港澳大湾区区块链应用推广中心

广东省计算机学会区块链专委会

相关内容分享只作为学术讨论，仅供访问者使用参考。我们尊重相关版权人的权利，但受限于篇幅、技术等客观因素，不保证所有信息、文本、图形、链接及其它项目的绝对准确性、绝对完整性和完整备注他人权利。我们尽最大的努力保证内容的科学性和严谨性等，但我们对使用上述内容而产生的相关后果不承担任何商业和法律责任

---

• ← Previous Post
• Next Post →