Angr学习记录

binary

Angr符号执行

参考：http://www.freebuf.com/sectool/143056.html
https://github.com/a7vinx/angr-doc-zh_CN/

Angr简介

Angr的含义

Angr是一个二进制代码分析工具，能够自动化完成二进制文件的分析,执行动态的符号执行(如Mayhem,KIEE等)。众所周知的是，在二进制代码中寻找并且利用漏洞是一项非常具有挑战性的工作，它的挑战性主要在于人工很难直观的看出二进制代码中的数据结构、控制流信息等。Angr的出现便使得这个问题变得易于解决。Angr是一个基于python的二进制漏洞分析框架,对二进制文件分析，并找到漏洞。使得漏洞挖掘的效率进一步得到提高。基于符号执行的fuzz工具driller就结合了Angr和AFL。

Angr的执行

  1. 将二进制程序利用CLE装载入Angr的分析系统中
  2. 将二进制程序转换为中间语言(Intermediate representation,IR)
  3. 将IR转换为语义较强的表达形式，形如这个程序做了什么，并非它是什么。
  4. 执行进一步的分析，比如，完整的或者部分静态分析(依赖关系分析，程序块分析)、程序空间的符号执行探索(挖掘漏洞)、一些对于上面方式的结合

Angr的安装

Angr是Python下的一个库，目前只在python2下受到支持，相信python3以后也会支持。所以利用python的方法就可以进行安装了，但是关键在于Angr的依赖需要解决：

sudo apt-get install python-dev libffi-dev build-essential virtualenvwrapper

依赖结束后执行如下指令即可完成安装：

mkvirtualenv angr && pip install angr

Angr学习

嗯，幻想一个场景，一场ctf比赛，我门是选手，点开赛题，一道reverse题提供了一个二进制附件名为r100,ok,开始做题。

Angr之装载模块

创建对象

Project意为项目，这里angr的而金子装载组件是CLE，负责将二进制对象及其依赖的库以及易于对其进行操作的方式交给angr的其他组件。Project就是加载二进制文件的方法。就像做pwn题时候我们使用ELF加载题目一样，道理都是一样的。

import angr
p = angr.Project('./r100')

信息查询

使用上述方法之后就已经把r100这个二进制文件进行了加载。这时候我们便可以得到很多关于这个二进制文件的信息了。

p.entry //二进制文件的入口点

p.loader.min_addr()/p.loader.max_addr() //二进制文件内存空间中的最小地址和最大地址

p.filename //二进制文件的名称，即r100

程序交互

loader方法代表了已经装载了的和映射到内存空间中的CLE二进制对象。每一种二进制对象都是由一种可以处理这种文件类型的后端装载器装载，比如ELF就是用以装载ELF文件。

CLE的交互指令如下：

p.loader //一个CLE装载器对象

p.loader.shared_objects //这是一个字典，包含已经作为二进制文件的一部分而装载的对象(种类取决于后端装载器)

p.loader.memory[b.loader.min_addr()] //这是装载后的进程的内存空间，它包含具体的地址与对应的值

p.loader.addr_belongs_to_object(b.loader.max_addr()) //返回映射在指定地址的二进制对象。

p.loader.find_symbol_got_entry(‘__libc_start_main’) //获取二进制文件的got表地址

与独立的二进制对象交互：

p.loader.main_bin.deps //这里获取程序依赖的库名列表，通过读取ELF文件的dynamic section的DT_NEEDED域获取。 注：dynamic sections下的NEEDED元素保存了以NULL结尾的字符串表的偏移量，这些字符串都是所依赖库的名字。

p.loader.main_bin.memory //这是关于主二进制对象的内存内容的dict

p.loader.shared_objects[‘libc.so.6’].imports //这是一个装载的libc所需的导入条目的dict(name–>ELFRelocation)

p.loader.main_bin.imports 这一个是主二进制对象所需的导入条目的dict(name–>ELFRelocation),地址通常为0.

装载选项

CLE工作时会默认地尝试装载二进制文件所需的依赖（比如libc.so.6等），除非装载选项中进行设置auto_load_libs为False。当装载库文件的时候，如果无法找到，装载器会默认忽略产生的错误并且标记所有关于那个库的依赖为已解决的状态。

装载选项传递是以dict形式进行传递。传递给Project后会转传给CLE。如上所示，如果我们想要设置选项为不装载依赖库，则可以使用如下指令：

p=angr.Project('./r100',load_options={"auto_load_libs":Flase})

除此以外，其他的装载选项列举如下：

load_options[‘force_load_libs’] = [‘libleet.so’] //无论是否是目标二进制文件所需要的，强制装载的库的list

load_options[‘skip_libs’] = [‘libc.so.6’] //需要跳过的库的list

load_options[‘main_opts’] = {‘backend’: ‘elf’} //装载主二进制文件时的选项

load_options[‘lib_opts’] = {‘libc.so.6’: {‘custom_base_addr’: 0x13370000}} //映射库名到其装载时需要使用的选项dict的dict

load_options[‘custom_ld_path’] = [‘/etc/libs’] //可以进行额外搜索的路径list

load_options[‘ignore_import_version_numbers’] = False //是否将文件名中版本号不同的库视作相同的，比如libc.so.6和libc.so.0

load_options[‘rebase_granularity’] = 0x1000 //在重定位共享对象的基址的时候需要使用的对齐值

load_options[‘except_missing_libs’] = True //如果找不到一个库，抛出一个异常（默认行为是忽略未找到的库）

下面两个选项被应用于每一个对象并且覆盖CLE的自动检测。它们可以通过main_opts或者lib_opts来应用。

load_options[‘main_opts’]={‘custom_base_addr’:0x4000} //装载二进制文件的基址为0x4000

load_options[‘main_opts’]={‘backend’:’elf’} //指定对象的后端装载器(这里指定为elf)

上面两者可同时设置，如下所示：

load_options[‘main_opts’]={‘backend’:’elf’,’custom_base_addr’:0x40000}

后端装载器选项

CLE集成了ELF,PE，CGC及ELF核心转储文件的后端支持，像IDA一样可以将文件装载。在CLE运作时，会自动检测需要使用的后端，当然如果已经知晓文件的结构信息，也可进行手动指定。关键字backend指定后端，custom_arch关键字指定架构。

load_options[‘main_opts’] = {‘backend’:’elf’,’custom_arch’:’i386’}

load_options[‘lib_opts’] = {‘libc.so.6’:{‘backend’：’elf’}}

后端关键字 描述 是否需要custom_arch
elf 基于PyELFTools的ELF装载器 no
pe 基于PEFile的PE装载器 no
cgc Cyber Grand Challenge文件的装载器 no
backedcgc 支持指定内存和寄存器支持CGC文件装载器 no
elfcore ELF核心转储文件的装载器 no
ida 启动IDA来解析文件 yes
blob 装载文件到内存中作为一个平坦的镜像 yes

Angr之求解模块

Angr的魅力不在于它是一个模拟器，而是符号执行功能。当它拥有一个符号而并非一个变量或是一个定值。对这个符号进行一系列的算术运算，所有运算整合成为一个操作树,称之为抽象语法树（AST）。同时AST可在后面转换为SMT求解器的约束。比如说python下的另一个库z3，已知操作序列的输出，求输入的值。

继续假设r100程序所需的输入是来自指令行，我们装载r100之后，就可以就这个值进行构造。
开头三部曲：

import angr, monkeyhex
proj = angr.Project('./r100')
state = proj.factory.entry_state()

BVV

Bitvertor是一个位序列，用算术的有界整数进行语义解释，它的缩写就是BV了。

BVV的作用则是定义一个指定的value，如下所示指定64位的1与100以及27位的9：

one = state.solver.BVV(1,64)        //output of one:<BV64 0x1>
hundred = state.solver.BVV(100,64) //output of hundred:<BV64 0x64>
new_nine = state.solver.BVV(9,27) //output of new_nine:<BV27 0x9>

既然这里指定的是value，又是有界的整数，那么相同位的值自然是可以进行算法操作的：

one + hundred ：<BV64 0x65>
hundred + 0x21: <BV64 0x85>
hundere - one*200 :<BV64 0xFFFFFFFFFFFFFF9C>

不同位的值如果想要进行操作，则必须将低位数的值进行拓展到与高位值一致才可,有两种方法：

  1. zero_extend:使用给定的数量的零在左侧填充位向量。
  2. sign_extend:与上者相反，填充高位。

这里想要把27位的值与64位的值进行操作的话，则需要将27位拓展填充到64位：

new_nine.zero_extend(64-27)       //output:<BV64 0x9>
one + new_nine.zero_extend(64-27) //output:<BV64 0xA>

BVS

BVS的作用则是定义一个符号symbol，如下所示指定64位下的符号x与y:

x=state.solver.BVS("x",64) //output:<BV64 x_0_64>
y=state.solver.BVS("y",64) //output:<BV64 y_1_64>

这里可以看到输出的x,y符号都被命名了，我们可以看出来，X_X_X,第一个表示符号名称，第二个是符号排序位置，第三个则是符号的位数。

不论是x还是y现在都是符号性的变量了，但是依旧是可以进行算数运算的，得到的不是一个数字，而是一个AST。

x + one          //<BV64 x_0_64 + 0x1>
(x + one) / 2    //<BV64 (x_0_64 + 0x1) / 0x2>
x - y             //<BV64 x_1_64 - y_1_64>

AST

这里的x,y,one。只要是bitvector都是一个AST，即使操作只有1层。那么AST如何处理？

每一个AST都有一个.op和.args。通俗的来说，op就是指出两个符号或值在做些什么，输出是一个字符串。args则是执行操作时候的输入。

tree = (x + 1) / (y + 2)  //output of tree:<BV64 (x_0_64 + 0x1) / (y_1_64 + 0x2)>
tree.op                   //'__div__'
tree.args                  //(<BV64 x_0_64 + 0x1>, <BV64 y_1_64 + 0x2>)
tree.args[0].op              //'__add__'
tree.args[0].args          //(<BV64 x_0_64>, <BV64 0x1>)
tree.args[0].args[1].op   //'BVV'
tree.args[0].args[1].args //(1, 64)

符号约束

如果将两个类型相似的AST进行比较操作依然会产生一个AST而非bitvector，而是符号布尔类型值。

x == 1                     //<Bool x_0_64 == 0x1>
x == one                   //<Bool x_0_64 == 0x1>
x > 2                      //<Bool x_0_64 > 0x2>
x + y == hundred + 5       //<Bool (x_0_64 + y_1_64) == 0x69>
hundred > 5                   //<Bool True>
hundred > -5               //<Bool False>

上述有一个奇怪的地方，hundred值是正整数，与-5相比应该是True，可为什么返回的是False呢？因为默认情况下的是无符号类型的比较，那么-5就被强制转换为了,自然大于100.

那么在if 或者是while语句中则不能直接使用变量之间的比较，可能无法得到具体的真值。这里可以这样使用。

yes = one == 1 //必然事件
no = one == 2 //不可能事件
maybe = x == y //可能事件
state.solver.is_true(yes) //Ture
state.solver.is_false(yes) //False
state.solver.is_true(no) //False
state.solver.is_false(no) //True
state.solver.is_true(maybe) //False
state.solver.is_false(maybe) //False

添加约束

当我们对r100进行分析之后，我们也许可以判断出所要得到的值的一些信息，比如长度，字符的Ascii大小等。那么为了增加效率，减少错误尝试。便可以认为添加约束。举个例子：

state.solver.add(x > y)      //约束x>y
state.solver.add(y > 2)         //约束y>2
state.solver.add(10 > x)     //约束x<10
state.solver.eval(x)         //求x满足条件的最小值为4

如果像Z3那样已知算法和输出结果求解输入值，就可写成如下格式：
state = proj.factory.entry_state() //创建对象得到入口点
input = state.solver.BVS(‘input’, 64) //定义一个符号
operation = (((input + 4) * 3) >> 1) + input //操作
output = 200 //定义输出值
state.solver.add(operation == output) //添加约束，操作后值等于输出值
state.solver.eval(input) //求解input

此解决方案只适用于比特向量，而非整数域。有的时候在使用时也会不小心添加有矛盾或者不合逻辑的约束，可以使用如下命令进行检测，以防报错：

state.satisfiable()     //True/False

浮点数

FPV及FPS

与BVV/BVS类似，可以使用FPV（float point valuse）及FPS(float point symbols)创建。

a = state.solver.FPV(3.2, state.solver.fp.FSORT_DOUBLE) //<FP64 FPV(3.2, DOUBLE)>
b = state.solver.FPS('b', state.solver.fp.FSORT_DOUBLE) //<FP64 FPS('FP_b_0_64', DOUBLE)>
a + b      //<FP64 fpAdd('RNE', FPV(3.2, DOUBLE), FPS('FP_b_0_64', DOUBLE))>
a + 4.4    //<FP64 FPV(7.6000000000000005, DOUBLE)>
b + 2 < 0  //<Bool fpLT(fpAdd('RNE', FPS('FP_b_0_64', DOUBLE), FPV(2.0, DOUBLE)), FPV(0.0, DOUBLE))>

raw_to_bv()与raw_to_fp()

BV与FP之间也是可以进行相互转换的，如下所示:

a.raw_to_bv()                         //<BV64 0x400999999999999a>
b.raw_to_bv()                         //<BV64 fpToIEEEBV(FPS('FP_b_0_64', DOUBLE))>
state.solver.BVV(0, 64).raw_to_fp()   //<FP64 FPV(0.0, DOUBLE)>
state.solver.BVS('x', 64).raw_to_fp() //<FP64 fpToFP(x_1_64, DOUBLE)>

val_to_bv()与val_to_fp()

第二中转换方法必须以目标值的大小或者种类作为参数：

a                            //<FP64 FPV(3.2, DOUBLE)>
a.val_to_bv(12)                 //<BV12 0x3>
a.val_to_bv(12).val_to_fp(state.solver.fp.FSORT_FLOAT)  //<FP32 FPV(3.0, FLOAT)>

运算求解

前面我们已经提及了solve下的eval，使用这个进行求解。它还有其他求解模式如下：

  1. solver.eval(expression) 将给出一个给定表达式的可能解决方案。
  2. solver.eval_one(expression) 将为您提供给定表达式的解决方案，或者如果可能有多个解决方案则抛出错误。
  3. solver.eval_upto(expression, n) 将为您提供最多n个给定表达式的解决方案，如果可能少于n，则返回少于n个。
  4. solver.eval_atleast(expression, n) 将给出给定表达式的n个解决方案，如果可能少于n则抛出错误。
  5. solver.eval_exact(expression, n) 将为您提供给定表达式的n个解决方案，如果少于或多于可能，则抛出错误。
  6. solver.min(expression) 将为您提供给定表达式的最小可能解决方案。
  7. solver.max(expression) 将为您提供给定表达式的最大可能解决方案。

在这些模式求解中，我们对结果可以进行规定，参数关键字如下两种：

  1. extra_constraints可以作为约束元组传递。此评估将考虑这些约束，但不会添加到状态。
  2. ast_to可以传递数据类型以将结果转换。目前只能转换为str，这将导致该方法返回基础数据的字节表示。例如，state.solver.eval(state.solver.BVV(0x41424344, 32), cast_to=str)将返回”ABCD”。

Angr之程序状态

在程序运作的过程中，内存以及寄存器的信息是很重要的，这里如果对程序加载过后，即可或得寄存器或是内存中的相关信息，并可以实现拷贝造作。

state.regs.rbp = state.reps.rsp                                        //拷贝rsp到rbp
state.mem[0x1000].uint64_t = state.regs.rdx                            //储存rdx的信息到0x1000
state.regs.rbp = state.mem[state.regs.rbp].uint64_t.resolved        //清楚rbp
state.regs.rax += state.mem[state.regs.rsp + 8].uint64_t.resolved    //add rax, qword ptr [rsp + 8]

state.reg后面接寄存器名即可查询寄存器的信息或者是对数据进行操作;

state.mem用于从内存加载类型化数据，但是如果想在在内存范围内进行原始加载或者存储的话就比较麻烦。可以使用state.memory解决这个问题。

s = proj.factory.blank_state()                     //创建一个空白状态
s.memory.store(0x4000, s.solver.BVV(0x1234, 64)) //存储数据到0x1234
s.memory.load(0x4004, 6) # load-size is in bytes //加载0x4004处的数据，返回<BV48 0x89abcdef0123>

前面所涉及的装载，factory意味工厂，里面后集中状态如下：

  1. .blank_state()构造一个“空白状态”，其大部分数据未初始化。访问未初始化的数据时，将返回无约束的符号值。
  2. .entry_state() 构造一个准备在主二进制文件入口点执行的状态。
  3. .full_init_state()构造一个准备通过任何需要在主二进制文件入口点之前运行的初始化程序执行的状态，例如，共享库构造函数或预初始化程序。完成这些后，它将跳转到入口点。
  4. .call_state() 构造一个准备执行给定函数的状态。

Angr之Simulation_Manager

Angr中最重要的就是Simulation_Manager，它允许同时控制状态组的符号执行，应用探索策略来探索程序的状态空间。

步进

和gdb或者od的动态调试类似，我们想要探索一个程序除了让他自动执行，我们也可以控制执行。通过一个基本块将给定存储中的所有状态向前步进。

import angr
proj = angr.Project('examples/fauxware/fauxware', auto_load_libs=False)
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.active                        //<SimState @ 0x400580>

simgr.step()
simgr.active                        //[<SimState @ 0x400540>]

如果在符号执行过程中遇到了分支情况的话，两个后继状态都会出现在储存当中，并且可以同步两个状态。但是如果不太注重中间过程的分析的话。可以直接使用run进行操作：

#使用step
while len(simgr.active) == 1:
   simgr.step()

simgr                //<SimulationManager with 2 active>
simgr.active        //[<SimState @ 0x400692>, <SimState @ 0x400699>]

#使用run
simgr.run()
simgr                //<SimulationManager with 3 deadended>

Stash Management

理解为存储管理，为了使状态与存储空间间调配移动，可以使用move(),那么这里就要指定，从哪儿来，到哪儿去，要做什么。及from_stash，to_stash以及filter_func（可选，默认是将一切）。例如，移动输出中具有特定字符串的所有内容：

simgr.move(from_stash='deadended', to_stash='authenticated', filter_func=lambda s: 'Welcome' in s.posix.dumps(1))
simgr          //output:<SimulationManager with 2 authenticated, 1 deadended>

这里就是将带有Welcome字符的所有输出进行存储，新建的存储名为’authenticated’。得到的存储实际上是一个列表，可以通过迭代进行逐个访问。当然，如果在存储名前加上one_,那么将会返回存储空间中的第一个状态，如果加的是mp_,那么将会返回多个存储信息。

for s in simgr.deadended + simgr.authenticated:
    print hex(s.addr)
//output:0x1000030
         0x1000078
         0x1000078

simgr.one_deadended    //output: <SimState @ 0x1000030>
simgr.mp_authenticated //output: MP([<SimState @ 0x1000078>, <SimState @ 0x1000078>])

除了deadended，还有其他的几种存储类型如下所示：

类型 描述
active 除非指定了备用存储，否则默认执行步进状态
deadended 程序遇到错误停止，正常结束或者是指令指针无效等。状态转到退出的存储
pruned 使用时LAZY_SOLVES，除非绝对必要，否则不会检查状态是否满足。当存在状态时发现状态不满LAZY_SOLVES时，遍历状态层次结构以识别其历史上最初变得不饱和的状态。
unconstrained 标志为不受约束的状态，由用户数据或某些其他符号数据源控制的指令指针放置在此处
unsat 标志为不可满足的状态，即具有矛盾的约束

上述方法的利用可以在这里这里这里看到使用方式。

小结

工欲善其事必先利其器，这里把Angr常用常见的方法都进行了学习总结，下面就要结合实例进行熟练了。

Title:Angr学习记录

Author:M1s5p

Created:2018-09-29, 10:30:37

Updated:2018-09-30, 17:20:38

Full URL:http://xq.dropsec.xyz/2018/09/29/Angr学习记录/

License: "CC BY-NC-SA 4.0" Keep Link & Author if Distribute.

Contents
  1. 1. Angr简介
    1. 1.1. Angr的含义
    2. 1.2. Angr的执行
    3. 1.3. Angr的安装
  2. 2. Angr学习
    1. 2.1. Angr之装载模块
      1. 2.1.1. 创建对象
      2. 2.1.2. 信息查询
      3. 2.1.3. 程序交互
      4. 2.1.4. 装载选项
      5. 2.1.5. 后端装载器选项
    2. 2.2. Angr之求解模块
      1. 2.2.1. BVV
      2. 2.2.2. BVS
      3. 2.2.3. AST
      4. 2.2.4. 符号约束
      5. 2.2.5. 添加约束
      6. 2.2.6. 浮点数
        1. 2.2.6.1. FPV及FPS
        2. 2.2.6.2. raw_to_bv()与raw_to_fp()
        3. 2.2.6.3. val_to_bv()与val_to_fp()
      7. 2.2.7. 运算求解
    3. 2.3. Angr之程序状态
    4. 2.4. Angr之Simulation_Manager
      1. 2.4.1. 步进
      2. 2.4.2. Stash Management
  3. 3. 小结
|