sup-009 符号化执行与Z3约束

Posted at 2019-10-16 reference 

符号化执行与Z3约束

0.符号化执行简介

首先我们需要明白，什么是符号化执行？符号化执行，简单来说就是一种自动化逆向的手段，具体实现过程：

将输入的参数变成未知数，众所周知输入的参数不同会导致在某些if处使程序导向完全不同的方向，进而影响结果。而如果我们将每次程序的抉择看作是一个方程，那么从我们希望的结果往回倒推，就能得到一组方程组，如果解方程就能得到我们需要的结果。

不过符号执行所面临的最大的困境就是，每次抉择会派生出两个及以上的分支，导致最后的状态数是指数级增长的，如果程序里面有大型的for循环效率可能就会非常低。

1. angr的安装

虽然说一般来说安装板块只要参考官方文档就不会有问题，但是自己安装angr的时候确实的遇到了许多问题，所以这里也是稍微记录一下。

虚拟环境很重要啊。记得保证自己的python3装了virtualenv这个模块，然后要按照下面的方式在一个虚拟环境中安装angr这个库。因为有可能会跟你的现有的库产生冲突。

mkdir angr_use
cd angr_use
virtualenv angr
source angr/bin/activate
pip install angr
deactivate#退出指令

2.angr的使用

graph TD
fa[angr]-->a1
fa--> son1[loader]
fa-->son2[analyses]
a1[factory]-->a2[blocks]
a1--> a3[states]
son1-->a3
a1--> a4[simulation_manager]
a4-->a5[stash]
a4-->a6[execution engine]
a3-->b1[successors]
a3-->b2[solver]

Loader: 总之就是加载的一个东西，包含了程序的一些基本信息，感觉没什么用呢

factory: angr做的函数封装，要用的话基本上用的就是这玩意了

​ blocks:angr 的代码分析是通过将程序划分成不同的块来进行实现的。使用factory.block(addr)可以生成addr处开始的block

​ states: 全称是simulated program state ,也就是一个虚拟的程序状态。angr用state这个类来存储一个程序某一时刻的虚拟状态，比如寄存器、内存什么的。为了存储寄存器，angr会使用一个叫做bitvector的玩意，简写就是BV。这玩意是可以用eval变成一个int的。使用BV的一个重要的目的就是为了符号执行，这样我们可以给某个变量一个变量名而非一个具体值。

​ simulation manager: 东西如其名，就是一个模拟的玩意。你可以使用一个state或者一个list的state来创建一个simulation manager。你想要得到结果就需要让程序实际地跑起来，就需要这个玩意。

Analyses: 给了一票的分析函数。这里的分析函数输出的是类似数据流图之类的东西，需要的时候再去查阅好了。

CLE

（can load everything): 看名字就懂了，一个可以装一切的loader。另外angr是可以安装在windows上执行的。虽然不知道能不能在windows上分析一个linux文件，但似乎angr也给出了分析pe文件的函数。不过这个loader可以用于获取文件中函数的地址，还可以拿到各种段地址什么的。其次的就是对各种project和object进行操作了，看上去应该能用来得到类似于system函数的地址。

关于Project的一些选项：

• auto_load_libs:是否自动加载共享库。
• except_missing_libs:没找到共享库就丢个错出来
• force_load_libs:强制装载,
• skip_libs:跳过就完事了
• ld_path：给一个地址让程序去找找看共享库

solver

首先是有关bitvector的使用。solver是基于state的，生成bv时可以使用state.solver.BVV(num,bit)来实现，你可以任意规定位数，并且可以进行零扩展或者符号扩展，使用zero_extend(num)sign_extend(num)来实现拓展。如果你需要设置一个固定位数的变量则需要使用BVS('varname',bit)来实现。bitvector的比较中会将负数当作无符号数来进行。所以需要用SGT()函数。（signed greater-than)的缩写。相似的还有SGE()SLE()SLT()UGE()UGT()ULE()ULT()这几个。有关浮点数的部分说实话感觉用到再说吧，既然你要用浮点数也要同样承受浮点数的精度丢失问题。

angr的solver engine是单独取名叫Claripy的东西，所以用的时候一般都要包括这个包。

​ 关于eval的使用：eval会给出一个可能解，但是还有其他的用法：

• solver.eval_one(expression)

• solver.eval_upto(expresssion,n)

• solver.eval_atleast(expression,n)

• solver.eval_exact(expression,n)

• solver.eval_min(expression)

• solver.eval_max(expression)

  同时还有一个参数extra_constraints 和cast_to。extra_constraints会给当前的解提供额外的约束而不加到state当中。cast_to可以设置为int 或bytes来控制输出形式。

state

状态这玩意也没什么好说的

• .blank_state()用空白状态创建，即数据都没初始化

• .entry_state()构造一个停在入口点的状态

• .full_init_state()执行了一系列初始化工作，比如共享库构造函数或预初始化程序

• .call_state()构造一个准备去执行某个函数的状态。

  可以传进去的参数：

  addr来指定确切的地址

  args来传递参数list，env来传递环境变量的dictionary

  可提供argc给entry_state&full_init_state,但不得多于传入args的个数

state这玩意可以各种回溯历史，或者复制或查看堆栈，还有各种对内存的操作。

simulation manager

这玩意可以说是核心中的核心部件了。利用它生成的状态都被存在stash中，默认生成的是active stash。除此之外还有deadended pruned uncontained unsat

• .step() 向前前进一个块

• .run()直接执行到底

• .explore()可以执行find和avoid，进行剪枝

  然后你可以给搜索提供一些优先的参数，比如按照DFS顺序、监控内存、控制步数控制循环什么的

execution engine

angr的底层实现，靠一系列的引擎来实现不同的操作。而对一个状态，为了实现每个引擎挨个尝试，你可以使用project.factory.successors(state,**kwargs)。而后继状态（successor state)分为五类：

• successors: 就是一般的后继了，如果一个正常执行且可能性小于256的后继就会归在其中
• unsat_successors:不满足的后继，往往是出现了错误的
• flat_successors:如果一个状态是含有指针的，那么会将它扁平化，即将每个不同的指针值均作为一种后继，然而最多只会是256个
• unconstrained_successors:如果一个指令指针的解多于256种，往往是因为其数据不受约束（栈溢出什么的），所以会将其放在其中。
• all_successors：看名字就知道是前面几个的集合体。

除此之外angr也提供了一套完整的打断点的方法，你可以侦测各种情况来下断点，不过这玩意实在是有点复杂……可能性太多，而且你用符号执行的时候也不一定会用到，目前先暂时搁置。

3.angr代码示例

一个不需要提前输入参数的模板：

import angr
proj = angr.Project('./filename',auto_load_libs=False)
state = proj.factory.entry_state()
simgr=proj.factory.simgr(state)
simgr.explore(find=0x400844,avoid=0x400855)
print simgr.found[0].posix.dumps(0)

需要提供参数的模板：

import angr,claripy
proj = angr.Project('./filename',auto_load_libs=False)
argv1 = claripy.BVS('argv1',50*8)
state = proj.factory.entry_state(args=['./filename',argv1])
simgr = proj.factory.simgr(state)
simgr.explore(find=0x400602,avoid=0x40060E)
print (simgr.found[0].solver.eval(argv1,cast_to=bytes))

分步骤的angr使用指南

1. import angr
   proj = angr.Project('')
   

4. Z3约束

使用时的代码模板：

from z3 import *
input=[BitVec('input_%d'%i,8) for i in range(32)]#char input[32]
s=Solver()
s.add(.....)
if s.check!=sat:
    print('unsat')
else:
    m=s.model()
    print(m)
    print(repr("".join([chr(m[input[i]].as_long())for i in range(32)])))