欢迎来到 黑吧安全网 聚焦网络安全前沿资讯,精华内容,交流技术心得!

区块链安全——以太坊智能合约静态分析

来源:本站整理 作者:佚名 时间:2019-01-10 TAG: 我要投稿
结合反编译代码和基本块的划分,我们不难得出所有边的集合E:
{‘基本块1’: [‘基本块2′,’基本块3’],‘基本块2’: [‘基本块3′,’基本块4’],‘基本块3’: [‘基本块11’],‘基本块4’: [‘基本块5′,’基本块6’],‘基本块5’: [‘基本块11’],‘基本块6’: [‘基本块8’],‘基本块7’: [‘基本块8’],‘基本块8’: [‘基本块9′,’基本块10’],‘基本块9’: [‘基本块11’],‘基本块10’: [‘基本块7’]}
我们把边的集合E用python中的dict类型表示,dict中的key是基本块,key对应的value值是一个list。还是以基本块1为例,因为基本块1存在基本块1->基本块2和基本块1->基本块3两条边,所以’基本块1’对应的list值为[‘基本块2′,’基本块3’]。
3.4 构建控制流图
在前两个小节中我们构建完成了基本块和边,到此构建控制流图的准备工作都已完成,接下来我们就要把基本块和边整合在一起,绘制完整的控制流图。

控制流图
上图就是完整的控制流图,从图中我们可以清晰直观的看到基本块之间的跳转关系,比如基本块1是条件跳转,根据条件是否成立跳转到不同的基本块,于是就形成了两条边。基本块2和基本块1类似也是条件跳转,也会形成两条边。基本块6是直接跳转,所以只会形成一条边。
在该控制流图中,只有一个起始块(基本块1)和一个结束块(基本块11)。当流程走到基本块11的时候,表示整个流程结束。需要指出的是,基本块11中只包含一条指令STOP。
3.5 总结
本章先介绍了控制流图中的基本概念,之后根据基本块的构建原则完成所有基本块的构建,接着结合反编译代码分析了基本块之间的跳转关系,画出所有的边。当所有的准备工作完成后,最后绘制出控制流图。在下一章中,我们将对构建好的控制流图,采用z3对其进行约束求解。
 
第四章 从控制流图开始约束求解
在本章中我们将使用z3对第三章中生成的控制流图进行约束求解。z3是什么,约束求解又是什么呢?下面将会给大家一一解答。
约束求解:求出能够满足所有约束条件的每个变量的值。
z3: z3是由微软公司开发的一个优秀的约束求解器,用它能求解出满足约束条件的变量的值。
从3.4节的控制流图中我们不难发现,图中用菱形表示的跳转条件左右着基本块跳转的方向。如果我们用变量表示跳转条件中的输入数据,再把变量组合成数学表达式,此时跳转条件就转变成了约束条件,之后我们借助z3对约束条件进行求解,根据求解的结果我们就能判断出基本块的跳转方向,如此一来我们就能模拟整个程序的执行。
接下来我们就从z3的基本使用开始,一步一步的完成对所有跳转条件的约束求解。
4.1 z3的使用
我们以z3的python实现z3py为例介绍z3是如何使用的[3]。
4.1.1 基本用法
from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y 10, x + 2*y == 7)
在上面的代码中,函数Int(‘x’)在z3中创建了一个名为x的变量,之后调用了solve函数求在三个约束条件下的解,这三个约束条件分别是x > 2, y
[y = 0, x = 7]
实际上满足约束条件的解不止一个,比如[y=1,x=5]也符合条件,但是z3在默认情况下只寻找满足约束条件的一组解,而不是找出所有解。
4.1.2 布尔运算
from z3 import *
p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(Implies(p, q), r == Not(q), Or(Not(p), r))
上面的代码演示了z3如何求解布尔约束,代码的运行结果如下:
[q = False, p = False, r = True]
4.1.3 位向量
在z3中我们可以创建固定长度的位向量,比如在下面的代码中BitVec(‘x’, 16)创建了一个长度为16位,名为x的变量。
from z3 import *
x = BitVec('x', 16)
y = BitVec('y', 16)
solve(x + y > 5)
在z3中除了可以创建位向量变量之外,也可以创建位向量常量。下面代码中的BitVecVal(-1, 16)创建了一个长度为16位,值为1的位向量常量。
from z3 import *
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print simplify(a == b)
4.1.4 求解器
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add(x > 10, y == x + 2)
print s
print s.check()
在上面代码中,Solver()创建了一个通用的求解器,之后调用add()添加约束,调用check()判断是否有满足约束的解。如果有解则返回sat,如果没有则返回unsat
4.2 使用z3进行约束求解
对于智能合约而言,当执行到CALLDATASIZE、CALLDATALOAD等指令时,表示程序要获取外部的输入数据,此时我们用z3中的BitVec函数创建一个位向量变量来代替输入数据;当执行到LT、EQ等指令时,此时我们用z3创建一个类似If(ULE(xx,xx), 0, 1)的表达式。
4.2.1 生成数学表达式
接下来我们以3.2节中的基本块1为例,看看如何把智能合约的指令转换成数学表达式。
在开始转换之前,我们先来模拟下以太坊虚拟机的运行环境。我们用变量stack=[]来表示以太坊虚拟机的栈,用变量memory={}来表示以太坊虚拟机的内存,用变量storage={}来表示storage。
基本块1为例的指令码如下:
00000: PUSH1 0x80
00002: PUSH1 0x40
00004: MSTORE
00005: PUSH1 0x04
00007: CALLDATASIZE
00008: LT
00009: PUSH1 0x3e
0000b: JUMPI
PUSH指令是入栈指令,执行两次入栈后,stack的值为[0x80,0x40]
MSTORE执行之后,stack为空,memory的值为{0x40:0x80}
CALLDATASIZE指令表示要获取输入数据的长度,我们使用z3中的BitVec(“Id_size”,256),生成一个长度为256位,名为Id_size的变量来表示此时输入数据的长度。

上一页  [1] [2] [3] [4] [5] [6] [7] [8] [9]  下一页

【声明】:黑吧安全网(http://www.myhack58.com)登载此文出于传递更多信息之目的,并不代表本站赞同其观点和对其真实性负责,仅适于网络安全技术爱好者学习研究使用,学习中请遵循国家相关法律法规。如有问题请联系我们,联系邮箱admin@myhack58.com,我们会在最短的时间内进行处理。
  • 最新更新
    • 相关阅读
      • 本类热门
        • 最近下载