自动化解题-Angr

在二进制领域有一些高大上的自动化分析工具，科学的使用它能够极大的提高分析效率，缩减分析任务的规模，本篇就是记录最热门的工具之一angr用法~

Z3

约束求解

微软的定理验证工具，就是约束求解的东西。约束求解就是对给定的符号一定的限制，然后求解出满足限制的具体值(一巴掌过来，不就是解方程组吗？)，例如给定x,y:x>1 x<y y<4，则可以求出x=2是它的一个解，这个过程就是约束求解，观察一类逆向题：”给定算法与输出，求输入”，一般来说这个给定的算法叫做加密算法，逆向要做的就是分析加密算法反推出解密算法，分析加密算法这里是读代码，而写解密代码就要考脑子想了，但若是使用约束求解就可以避免自己想，直接用工具就能求出。另外，约束求解给定的最简约束越多则运算速度越快，结果范围越小。

安装

pip install z3-solver

使用

1
2
3
4
5
6
7
8
9
10
11

import z3
x = z3.Int('x')
y = z3.Int('y')
solve(x > 2, y < 10, x + 2*y == 7) 
#新建求解器
s=Sovler()
#添加约束
s.add()
#求解
if s.check() == sat:
    print s.model()

这是最基本的用法，其中，在一开始定义了两个python变量x,y它的类型是z3.Int，此时就可以把它们当作数学中的未知数，在接下来新建求解器并添加约束或者直接使用solve添加约束并求解。

angr

它是一个易用的二进制分析套件，可以用于做动态符号执行和多种静态分析，现在来简单记录一下它的用法，使用时也可以使用ipython的class?查看帮助文档。详细的文档可以看这里。

符号执行 （Symbolic Execution）是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。[1]符号模拟技术（symbolic simulation）则把类似的思想用于硬件分析。符号计算（Symbolic computation）则用于数学表达式分析。

安装

1. 安装虚拟环境pip install virtualenvwrapper
2. 配置虚拟环境

   1 2 3 4

   mkdir $HOME/.ven #创建工作目录 vim $HOME/.bashrc #编辑启动项 export WORKON_HOME=$HOME/.ven #将这两项放入文件，开机自动运行 source /usr/local/bin/virtualenvwrapper.sh

3. 使用虚拟环境

   1 2 3 4

   mkvirtualenv env1 #创建环境 workon #列出已有环境 deactivate #退出环境 rmvirtualenv #删除环境

4. 安装angr

   1 2 3 4 5 6 7 8 9 10 11

   mkvirtualenv angr pip install ipython #非必要 #pip install matplotlib networks #画CFG的 pip install angr #安装angr-utils mkdir angr-dev cd angr-dev git clone https://github.com/axt/bingraphvis pip install -e ./bingraphvis git clone https://github.com/axt/angr-utils pip install -e ./angr-utils

   angr功能很多，最好使用ipython自动补全，在虚拟环境ipython可能会缺少部分库，重新安装即可。

   使用

   下面使用如下样例测试：

   1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21

   #include <stdio.h> #include <string.h> int main() { char passwd[] = "B3taMa0_Passwd_@Angr"; char input[30] ={0,}; puts("input passwd:"); scanf("%20s",input); int len = strlen(input); if(len == strlen(passwd)){ for(int i=0;i<len;i++){ if(input[i]!=passwd[i])goto error; } puts("success!"); }else{ error: puts("error!"); } return 0; }

   创建项目

   创建项目是使用angr的第一步，它会执行基本的分析操作。正常执行一个可执行文件，需要装载器按照其格式(如PE32或ELF)解析它并将其装载到内存中，其后CPU就可以直接执行它了；但是在做逆向分析时我们需要考虑的更多，即用同样的源码编译成的同样格式的可执行文件(如ELF)，编译的目标架构(如x64,i64,mips,arm等)不同它的指令也是不同的，而我们在分析程序时关注的是程序的语义，为了消除这种差异可以把不同的原始的机器指令转换为相同的中间指令，再分析它的语义，这样只需要编写分析中间代码的工具而不需要为每一种指令编写分析工具，将会省去很多重复的工作，以上也即angr创建一个项目的过程：装载二进制文件->转换二进制文件为中间语言->转换IR为语义描述->执行真正的分析。

   1 2	import angr proj = angr.Project('test', auto_load_libs=False,except_missing_libs=True)

   由于我们在分析二进制程序时更多的是关心程序本身逻辑而非其使用的开源库，所以对动态链接库可以依实际选择是否装载。当不加载时，将无法使用它的导出函数，程序将无法正常运行，解决办法就是使用SIM_PROCEDURES或者hook，因为我们不关心程序运行后的影响，我们只关心程序本身逻辑，所以可以使用虚假的函数代替真实的函数，虚假的函数只改变程序的状态，模拟原函数的功能，例如我们需要调用read(0,buf,30)读取数据到buf，那么可以在python层写个虚假函数，它直接改变buf这块内存的数据及相应寄存器，不进行真正的io操作，这样就避免了分析库函数造成的路径爆炸等问题，angr把这中虚假函数叫做SIM_PROCEDURES并且已经实现了部分常用的虚假库函数，若没有也可以字节写。另外使用hook也可以达到相同的效果(unicorn就是使用hook实现处理库函数调用的)。另外就是hook也很常用，用法如官方用例：

   1 2 3 4 5 6 7 8 9 10 11 12 13 14 15

   >>> stub_func = angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained'] # this is a CLASS >>> proj.hook(0x10000, stub_func()) # hook with an instance of the class >>> proj.is_hooked(0x10000) # these functions should be pretty self-explanitory True >>> proj.unhook(0x10000) >>> proj.hooked_by(0x10000) <ReturnUnconstrained> >>> @proj.hook(0x20000, length=5) ... def my_hook(state): ... state.regs.rax = 1 >>> proj.is_hooked(0x20000) True

   当项目创建完成，将能够得到很多有用信息，余下的操作都是根据这个项目实例来的：
   

   装载器

   它负责解析加载可执行程序，于是所有程序的信息与加载信息都可以从这里得到：
   
   如图，可以得到被装载的每个对象，对指定对象可以得到段与节区信息，也可以得到一些保护信息，获取符号信息。

   分析流图

   自己的版本好像和文档的不一样，暂时用不上，有时间再去研究吧。可以看https://docs.angr.io/built-in-analyses/cfg 发出来的控制流图还是挺好看的：

   1 2 3 4 5 6 7

   import angr from angrutils import * proj = angr.Project("test", load_options={'auto_load_libs':False}) main = proj.loader.main_object.get_symbol("main") start_state = proj.factory.blank_state(addr=main.rebased_addr) cfg = proj.analyses.CFGFast() plot_cfg(cfg, "test_cfg", asminst=True, remove_imports=True, remove_path_terminator=True)

   指令分析

   angr的其他分析功能全部都需要下加载要分析的可执行文件以后再初始化对应的类对象，为了方便angr提供了工厂类获取这些实例对象：
   
   而其中的block方法即可查看分析指令，它指定一个地址作为参数，返回地址所在方法实例：
   
   详细依然可使用ipython查看文档。

符号执行

这也是angr最重要的功能，它可以使用符号代替真实数据执行程序，出现分支即添加约束，路径也再加倍，最终探索到需要的路径时，就可以按照整个路径上的抽象语法树生成约束，使用求解引擎(如Z3)自动完成求解，得到能到此路径的输入。

angr可以指定一个地址开始执行，但是一个程序要正确执行直接给定任意地址是不行的，还需要给定此时的上下文(寄存器)及内存数据，angr把内存和所有寄存器信息合在一起称为一个状态集State，用它就可以表示程序执行的某个状态了，angr预置了三种状态起始也可以手动指定函数调用创建起始状态：

1
2
3
4

entry_state()           #最常用，从main object的entrypoint开始       
blank_state()           #所有数据还没有初始化，此时读取去数据会返回一个没有约束的符号变量
full_init_state()       #执行完所有初始化操作，跳转到main object 的ep
call_state()            #从指定函数开始，它默认以blank_state作为前置状态

我们可以通过状态看到程序的运行时数据，比如寄存器，内存，输入出调用栈等：

得到一个起始状态后就可以让程序从此状态开始符号执行了，而每执行一步将又会得到新的状态，angr使用simulation_manager来管理所有状态：

这里面最常用的就是explore，它能从当前状态开始探索路径，它有两个重要参数find后接地址或地址列表表明希望达到的地址，avoid恰恰相反表明不想要到达的地址，当执行此方法后，可以查看状态，found为找到到达find所指地址的路径，此时就可以使用约束求解得到到达该路径的输入了。至此，可以将样例的程序解出来了：

1
2
3
4
5
6
7
8

import angr
proj = angr.Project('test', auto_load_libs=False,except_missing_libs=True)  #程序将被载入到0x400000
entryState = proj.factory.entry_state()
sm = proj.factory.simulation_manager(entryState)
sm.explore(avoid=0x123A+0x400000,find=0x1228+0x400000)                      #通过ida得到的
if len(sm.found)>0:                                                         #存在为found的状态
    foundState = sm.found[0]                                                #取出第一个满足条件的解
    print foundState.posix.dumps(0)                                         #使用scanf是从stdin得到输入，所以dumps文件描述符0得到输入。

结果：

1
2
3
4

(angr) ➜  ~ python testAngr.py
WARNING | 2019-02-01 23:30:22,872 | angr.analyses.disassembly_utils | Your version of capstone does not support MIPS instruction groups.
WARNING | 2019-02-01 23:30:23,109 | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.
B3taMa0_Passwd_@Angr

约束求解

angr将抽象语法树转换为约束并求解，这是一个自动的过程，所以用户一般是不需要手动运用这个功能的，不过有时也需要用到，angr后端默认使用z3引擎求解。

数据定义

约束求解的整个运算对象是未知数，作为未知数它的值并不确定它只是一个符号，我们不能用传统的方法直接用定义普通变量来定义它，z3定义了对应的类，angr作为一套框架，为了方便使用不同的求解引擎，可以对这类符号极其运算做了抽象，由claripy模块暴露出抽象的接口，单独使用此模块的功能需要手动导入它，也可以从状态集里面获得sovler，sovler也可以定义符号与执行运算，以下介绍全是它的属性方法。另外，不同的符号代表的含义不同，他们的类型也根据实际变化，于是可以定义如下类型符号：

BVS即(bit vectors symbol)，用它来表示一个符号，第一个参数表示符号名，第二个参数表示这个符号的长度 单位bit。当它参与运算后，将会得到一颗抽象语法树，可以使用args和op属性遍历该树。
BVV即(bit vectors value)，用来表示一个明确值的整数，第一个参数为实际值，第二个参数表示值的长度。他可以直接与普通常数或同长度BVV进行四则运算，不同的BVV需要先进行位扩展再运算。
FPV即浮点值，用来表示一个明确值的浮点数，作为浮点数，它是不精确的而且有多种标准，需要用第二个参数指明。
FPS即浮点型符号，用来表示一个浮点型符号。

运算类型

可进行普通数学运算，默认比较运算会被当做无符号数，可以使用带SLE这类进行有符号数比较：

当然它也支持有符号除模等其它运算，详见文档。

求解

add()用于添加约束条件，satisfiable()用于查看是否有解，若有解可使用eval获取解，它的作用是将bitvector转换为python本地数据类型，它的参数指明要获取的是哪个未知数的解，参数也可以是多个未知数的表达式，这会取出相应未知数的解并进行运算再得值。

例子

见：https://github.com/angr/angr-doc/tree/master/examples?1549085924935

参考

https://docs.angr.io