@ -6,8 +6,9 @@
- [快速入门 ](#快速入门 )
- [二进制文件加载器 ](#二进制文件加载器 )
- [求解器引擎 ](#求解器引擎 )
- [程序状态 ](#程序状态 )
- [模拟管理器 ](#模拟管理器 )
- [VEX IR 翻译器 ](#vex-ir-翻译 )
- [体系结构信息收集 ](#体系结构信息收集 )
- [CTF 实例 ](#ctf-实例 )
- [参考资料 ](#参考资料 )
@ -18,13 +19,15 @@
## 安装
```shell
```
```
强烈建议在虚拟环境中安装 angr， （ ） 你 肯定不希望 angr 的依赖覆盖掉官方的共享库。
对于大多数 *nix系统， `mkvirtualenv angr && pip install angr` 安装就好了。
强烈建议在虚拟环境中安装 angr， （ ） ，开一个隔离的环境就好了：
```
$ sudo pip install angr
```
如果这样安装失败的话，那么你可以按照下面的顺序从 angr 的官方仓库安装：
```text
@ -55,12 +58,12 @@ WARNING | 2017-12-08 10:46:58,836 | cle.loader | The main binary is a position-i
```
这样就得到了二进制文件的各种信息，如：
```python
>>> proj . filename
>>> proj . filename # 文件名
'/bin/true'
>>> proj . arch
>>> proj . arch # 一个 archinfo.Arch 对象
< Arch AMD64 ( LE ) >
>>> hex ( proj . entry )
'0x4013b 0'
>>> hex ( proj . entry ) # 入口点
'0x40137 0'
```
程序加载时会将二进制文件和共享库映射到虚拟地址中，
@ -68,14 +71,25 @@ WARNING | 2017-12-08 10:46:58,836 | cle.loader | The main binary is a position-i
>>> proj . loader
< Loaded true , maps [ 0x400000 : 0x5008000 ] >
```
所有对象文件如下，其中二进制文件是 main object：
所有对象文件如下，其中二进制文件本身 是 main_ object，然后还可以查看对象文件的相关信息 ：
```
[<ELF Object true, maps [0x400000:0x60721f]>, <ELF Object libc-2.26.so, maps [0x1000000:0x13b78cf]>, <ELF Object ld-2.26.so, maps [0x2000000:0x22260f7]>, <ELFTLSObject Object cle##tls, maps [0x3000000:0x300d010]>, <ExternObjec t O bject cle##externs, maps [0x4000000:0x4008000]>, <KernelObject Object cle##kernel, maps [0x5000000:0x5008000]>]
for obj in proj.loader.all_objects:
... prin t o bj
...
<ELF Object true, maps [0x400000:0x60721f]>
<ELF Object libc-2.27.so, maps [0x1000000:0x13bb98f]>
<ELF Object ld-2.27.so, maps [0x2000000:0x22260f7]>
<ELFTLSObject Object cle##tls, maps [0x3000000:0x300d010]>
<ExternObject Object cle##externs, maps [0x4000000:0x4008000]>
<KernelObject Object cle##kernel, maps [0x5000000:0x5008000]>
>>> proj.loader.main_object
<ELF Object true, maps [0x400000:0x60721f]>
>>> proj.loader.main_object.pic
True
>>> hex( proj.loader.main_object.min_addr)
'0x400000'
>>> hex(proj.loader.main_object.max_addr)
'0x60721f'
>>> proj.loader.main_object.execstack
False
```
通常我们在创建工程时选择关闭 `auto_load_libs` 以避免 angr 加载共享库：
```
@ -87,62 +101,68 @@ WARNING | 2017-12-08 11:09:28,629 | cle.loader | The main binary is a position-i
`project.factory` 提供了很多类对二进制文件进行分析，它提供了几个方便的构造函数。
`project.factory.block()` 用于从给定地址解析一个 basic block：
`project.factory.block()` 用于从给定地址解析一个 basic block，对象类型为 Block ：
```python
>>> block = proj . factory . block ( proj . entry ) # 从程序头开始解析一个 basic block
>>> block
< Block for 0x4013b 0 , 42 bytes >
>>> block . pp () # pretty-print，
0x4013b 0 : xor ebp , ebp
0x4013b 2 : mov r9 , rdx
0x4013b 5 : pop rsi
0x4013b 6 : mov rdx , rsp
0x4013b 9 : and rsp , 0xfffffffffffffff0
0x4013b d : push rax
0x4013b e : push rsp
0x4013b f : lea r8 , qword ptr [ rip + 0x32c a ]
0x4013c 6 : lea rcx , qword ptr [ rip + 0x325 3 ]
0x4013c d : lea rdi , qword ptr [ rip - 0xe4 ]
0x4013d 4 : call qword ptr [ rip + 0x205b2 6 ]
< Block for 0x40137 0 , 42 bytes >
>>> block . pp () # 打印
0x40137 0 : xor ebp , ebp
0x40137 2 : mov r9 , rdx
0x40137 5 : pop rsi
0x40137 6 : mov rdx , rsp
0x40137 9 : and rsp , 0xfffffffffffffff0
0x40137 d : push rax
0x40137 e : push rsp
0x40137 f : lea r8 , qword ptr [ rip + 0x32d a ]
0x40138 6 : lea rcx , qword ptr [ rip + 0x326 3 ]
0x40138 d : lea rdi , qword ptr [ rip - 0xe4 ]
0x40139 4 : call qword ptr [ rip + 0x205b7 6 ]
>>> block . instructions # 指令数量
11
>>> block . instruction_addrs # 指令地址
[ 4199344 L , 4199346 L , 4199349 L , 4199350 L , 4199353 L , 4199357 L , 4199358 L , 4199359 L , 4199366 L , 4199373 L , 4199380 L ]
[ 4199280 L , 4199282 L , 4199285 L , 4199286 L , 4199289 L , 4199293 L , 4199294 L , 4199295 L , 4199302 L , 4199309 L , 4199316 L ]
```
另外，还可以将 b lock 对象转换成其他形式：
另外，还可以将 B lock 对象转换成其他形式：
```python
>>> block . capstone
< CapstoneBlock for 0x4013b 0 >
< CapstoneBlock for 0x40137 0 >
>>> block . capstone . pp ()
>>> block . vex
< pyvex . block . IRSB object at 0x7fe526b98670 >
IRSB < 0x2a bytes , 11 ins . , < Arch AMD64 ( LE ) >> at 0x401370
>>> block . vex . pp ()
```
程序的执行需要初始化一个 `SimState` 对象：
程序的执行需要初始化一个模拟程序状态的 `SimState` 对象：
```python
>>> state = proj . factory . entry_state ()
>>> state
< SimState @ 0x4013b 0 >
< SimState @ 0x40137 0 >
```
该对象包含了程序的内存、寄存器、文件系统数据等：
该对象包含了程序的内存、寄存器、文件系统数据等等模拟运行时动态变化的数据，例如 ：
```python
>>> state . regs . rip
< BV64 0x4013b 0>
>>> state . regs # 寄存器名对象
< angr . state_plugins . view . SimRegNameView object at 0x7f126fdfe81 0>
>>> state . regs . rip # BV64 对象
< BV64 0x401370 >
>>> state . regs . rsp
< BV64 0x7fffffffffeff98 >
>>> state . regs . rsp . length # BV 对象都有 .length 属性
64
>>> state . regs . rdi
< BV64 reg_48_0_64 { UNINITIALIZED } > # 符号变量，它是符号执行的基础
>>> state . mem [ proj . entry ] . int . resolved
< BV64 reg_48_0_64 { UNINITIALIZED } > # BV64 对象， 符号变量
>>> state . mem [ proj . entry ] . int . resolved # 将入口点的内存解释为 C 语言的 int 类型
< BV32 0x8949ed31 >
```
这里的 BV， ， 用于表示 angr 里的 CPU 数据。下面是 python int 和 bitvectors 之间的转换：
这里的 BV， ， 可以理解为一个比特串，用于在 angr 里表示 CPU 数据。看到在这里 rdi 有点特殊，它没有具体的数值，而是在符号执行中所使用的符号变量，我们会在稍后再做讲解。
下面是 Python int 和 bitvectors 之间的转换：
```python
>>> bv = state . solver . BVV ( 0x1234 , 32 )
>>> bv = state . solver . BVV ( 0x1234 , 32 ) # 创建值 0x1234 的 BV32 对象
>>> bv
< BV32 0x1234 >
>>> hex ( state . solver . eval ( bv ))
>>> hex ( state . solver . eval ( bv )) # 将 BV32 对象转换为 Python int
'0x1234'
>>> bv = state . solver . BVV ( 0x1234 , 64 )
>>> bv
@ -150,66 +170,111 @@ WARNING | 2017-12-08 11:09:28,629 | cle.loader | The main binary is a position-i
>>> hex ( state . solver . eval ( bv ))
'0x1234L'
```
使用 bitvectors 来设置寄存器和内存的值，当直接传入 python int 时， ：
于是 bitvectors 可以进行数学运算 ：
```python
>>> one = state . solver . BVV ( 1 , 64 )
>>> one_hundred = state . solver . BVV ( 100 , 64 )
>>> one_hundred + one # 位数相同时可以直接运算
< BV64 0x65 >
>>> one_hundred + one + 0x100
< BV64 0x165 >
>>> state . solver . BVV ( - 1 , 64 ) # 默认为无符号数
< BV64 0xffffffffffffffff >
>>> five = state . solver . BVV ( 5 , 27 )
>>> five
< BV27 0x5 >
>>> one + five . zero_extend ( 64 - 27 ) # 位数不同时需要进行扩展
< BV64 0x6 >
>>> one + five . sign_extend ( 64 - 27 ) # 或者有符号扩展
< BV64 0x6 >
```
使用 bitvectors 可以直接来设置寄存器和内存的值，当传入的是 Python int 时， ：
```python
>>> state . regs . rsi = state . solver . BVV ( 3 , 64 )
>>> state . regs . rsi
< BV64 0x3 >
>>> state . mem [ 0x1000 ] . long = 4
>>> state . mem [ 0x1000 ] . long = 4 # 在地址 0x1000 存放一个 long 类型的值 4
>>> state . mem [ 0x1000 ] . long . resolved # .resolved 获取 bitvectors
< BV64 0x4 >
>>> state . mem [ 0x1000 ] . long . concrete # .concrete 获得 p ython int
>>> state . mem [ 0x1000 ] . long . concrete # .concrete 获得 P ython int
4 L
```
初始化的 state 可以经过模拟执行得到一系列的 states， s imulation 管理器 的作用就是对这些 states 进行管理：
初始化的 state 可以经过模拟执行得到一系列的 states， 模拟管理器（ imulation Managers） 的作用就是对这些 states 进行管理：
```python
>>> simgr = proj . factory . simulation_manager ( state )
>>> simgr
< SimulationManager with 1 active >
>>> simgr . active
[ < SimState @ 0x4013b 0 > ]
>>> simgr . step () # 模拟一个 basic block 的执行
>>> simgr . active # 当前 state
[ < SimState @ 0x40137 0 > ]
>>> simgr . step () # 模拟执行 一个 basic block
< SimulationManager with 1 active >
>>> simgr . active # 模拟状态 被更新
[ < SimState @ 0x1020e 80 > ]
>>> simgr . active # 当前 state 被更新
[ < SimState @ 0x1022f 80 > ]
>>> simgr . active [ 0 ] . regs . rip # active[0] 是当前 state
< BV64 0x40462 0 >
>>> state . regs . rip # 但原始的 state 没有变
< BV64 0x4013b 0 >
< BV64 0x1022f8 0 >
>>> state . regs . rip # 但原始的 state 并 没有改 变
< BV64 0x40137 0 >
```
`p roject.analyses` 提供了大量函数用于程序分析。
angr 提供了大量函数用于程序分析，在这些函数在 `P roject.analyses. ` ，例如：
```python
>>> cfg = p . analyses . CFGFast () # 得到 control-flow graph
>>> cfg
< CFGFast Analysis Result at 0x7f4626f1509 0 >
< CFGFast Analysis Result at 0x7f1265b6265 0 >
>>> cfg . graph
< networkx . classes . digraph . DiGraph object at 0x7f462316ef9 0 > # 详细内容 请查看 networkx
< networkx . classes . digraph . DiGraph object at 0x7f1265e7731 0 > # 详情 请查看 networkx
>>> len ( cfg . graph . nodes ())
937
>>> entry_node = cfg . get_any_node ( proj . entry ) # 得到给定地址的节点
934
>>> entry_node = cfg . get_any_node ( proj . entry ) # 得到给定地址的 CFGNode
>>> entry_node
< CFGNode 0x4013b 0 [ 42 ] >
< CFGNode 0x40137 0 [ 42 ] >
>>> len ( list ( cfg . graph . successors ( entry_node )))
2
```
如果要想画出图来，还需要安装 matplotlib，
如果要想画出图来，还需要安装 matplotlib。
```python
>>> import networkx as nx
>>> import matplotlib
>>> matplotlib . use ( 'Agg' )
>>> import matplotlib.pyplot as plt
>>> nx . draw ( cfg . graph ) # 画图
>>> plt . show () # 显示
>>> plt . savefig ( 'temp.png' ) # 保存
```
#### 加载二进制文件
`cle.loader.Loader` ，它导入所有的对象文件并导出一个进程内存的抽象。类 `cle.backends` 是加载器的后端，根据二进制文件类型区分为 `cle.backends.elf` 、`cle.backends.pe` 、`cle.backends.macho` 等。
加载对象文件和细分类型如下 ：
首先我们来看加载器的一些常用参数 ：
- `auto_load_libs` ：是否自动加载主对象文件所依赖的共享库
- `except_missing_libs` ：当有共享库没有找到时抛出异常
- `force_load_libs` ：强制加载列表指定的共享库，不论其是否被依赖
- `skip_libs` ：不加载列表指定的共享库，即使其被依赖
- `custom_ld_path` ：可以到列表指定的路径查找共享库
如果希望对某个对象文件单独指定加载参数，可以使用 `main_ops` 和 `lib_opts` 以字典的形式指定参数。一些通用的参数如下：
- `backend` ：使用的加载器后端，如："elf", "pe", "mach-o", "ida", "blob" 等
- `custom_arch` ：使用的 archinfo.Arch 对象
- `custom_base_addr` ：指定对象文件的基址
- `custom_entry_point` ：指定对象文件的入口点
举个例子：
```python
>>> proj . loader . all_objects # 所有对象文件
[ < ELF Object true , maps [ 0x400000 : 0x60721f ] > , < ELF Object libc - 2.26 . so , maps [ 0x1000000 : 0x13b78cf ] > , < ELF Object ld - 2.26 . so , maps [ 0x2000000 : 0x22260f7 ] > , < ELFTLSObject Object cle ##tls, maps [0x3000000:0x300d010]>, <ExternObject Object cle##externs, maps [0x4000000:0x4008000]>, <KernelObject Object cle##kernel, maps [0x5000000:0x5008000]>]
angr . Project ( main_opts = { 'backend' : 'ida' , 'custom_arch' : 'i386' }, lib_opts = { 'libc.so.6' : { 'backend' : 'elf' }})
```
加载对象文件和细分类型如下：
```
... print obj
...
<ELF Object true, maps [0x400000:0x60721f]>
<ELF Object libc-2.27.so, maps [0x1000000:0x13bb98f]>
<ELF Object ld-2.27.so, maps [0x2000000:0x22260f7]>
<ELFTLSObject Object cle##tls, maps [0x3000000:0x300d010]>
<ExternObject Object cle##externs, maps [0x4000000:0x4008000]>
<KernelObject Object cle##kernel, maps [0x5000000:0x5008000]>
```
- `proj.loader.main_object` ：主对象文件
- `proj.loader.shared_objects` ：共享对象文件
@ -220,24 +285,450 @@ WARNING | 2017-12-08 11:09:28,629 | cle.loader | The main binary is a position-i
通过对这些对象文件进行操作，可以解析出相关信息：
```python
>>> obj = proj . loader . main_object
>>> hex ( obj . entry ) # 入口地址
'0x4013b0'
>>> obj
< ELF Object true , maps [ 0x400000 : 0x60721f ] >
>>> hex ( obj . entry ) # 入口地址
'0x401370'
>>> hex ( obj . min_addr ), hex ( obj . max_addr ) # 起始地址和结束地址
( '0x400000' , '0x60721f' )
>>> obj . segments # segments
< Regions : [ < ELFSegment offset = 0x0 , flags = 0x5 , filesize = 0x6094 , vaddr = 0x400000 , memsize = 0x6094 > , < ELFSegment offset = 0x6c10 , flags = 0x6 , filesize = 0x470 , vaddr = 0x606c10 , memsize = 0x610 > ] >
>>> obj . sections # sections
< Regions : [ < Unnamed | offset 0x0 , vaddr 0x400000 , size 0x0 > , <. interp | offset 0x23 8, vaddr 0x400238 , size 0x1c > , <. note . ABI - tag | offset 0x254 , vaddr 0x400254 , size 0x20 > , ... etc
>>> for seg in obj . segments : # segments
... print seg
...
< ELFSegment offset = 0x0 , flags = 0x5 , filesize = 0x5f4 8, vaddr = 0x400000 , mem size= 0x5f48 >
< ELFSegment offset = 0x6c30 , flags = 0x6 , filesize = 0x450 , vaddr = 0x606c30 , memsize = 0x5f0 >
>>> for sec in obj . sections : # sections
... print sec
...
< Unnamed | offset 0x0 , vaddr 0x400000 , size 0x0 >
<. interp | offset 0x238 , vaddr 0x400238 , size 0x1c >
<. note . ABI - tag | offset 0x254 , vaddr 0x400254 , size 0x20 >
<. note . gnu . build - id | offset 0x274 , vaddr 0x400274 , size 0x24 >
... etc
```
根据需要解析 我们需要的信息 ：
根据地址查找 我们需要的东西 ：
```python
>>> ob j . find_segmen t_containing( obj . entry ) # 包含给 定地址的 segments
< ELFSegment offset = 0x0 , flags = 0x5 , filesize = 0x6094 , vaddr = 0x400000 , memsize = 0x6094 >
>>> obj . find_section_containing ( obj . entry ) # 包含给定地址的 sections
<. text | offset 0x12f0 , vaddr 0x4012f0 , size 0x33c9 >
>>> pr oj. loader . find_objec t_containing( 0x400000 ) # 包含指 定地址的 object
< ELFObject true , maps [ 0x400000 : 0x60721f ] >
>>> free = proj . loader . find_symbol ( 'free' ) # 根据名字或地址在 project 中查找 symbol
>>> free
< Symbol "free" in libc . so .6 at 0x1083ab0 >
>>> free . name # 符号名
u 'free'
>>> free . owner_obj # 所属 object
< ELF Object libc - 2.27 . so , maps [ 0x1000000 : 0x13bb98f ] >
>>> hex ( free . rebased_addr ) # 全局地址空间中的地址
'0x1083ab0'
>>> hex ( free . linked_addr ) # 相对于预链接基址的地址
'0x83ab0'
>>> hex ( free . relative_addr ) # 相对于对象基址的地址
'0x83ab0'
>>> free . is_export # 是否为导出符号
True
>>> free . is_import # 是否为导入符号
False
>>> obj . find_segment_containing ( obj . entry ) # 包含指定地址的 segment
< ELFSegment offset = 0x0 , flags = 0x5 , filesize = 0x5f48 , vaddr = 0x400000 , memsize = 0x5f48 >
>>> obj . find_section_containing ( obj . entry ) # 包含指定地址的 section
<. text | offset 0x12b0 , vaddr 0x4012b0 , size 0x33d9 >
>>> main_free = obj . get_symbol ( 'free' ) # 根据名字在当前 object 中查找 symbol
>>> main_free
< Symbol "free" in true ( import ) >
>>> main_free . is_export
False
>>> main_free . is_import
True
>>> main_free . resolvedby # 从哪个 object 获得解析
< Symbol "free" in libc . so .6 at 0x1083ab0 >
>>> hex ( obj . linked_base ) # 预链接的基址
'0x0'
>>> hex ( obj . mapped_base ) # 实际映射的基址
'0x400000'
```
通过 `obj.relocs` 可以查看所有的重定位符号信息，或者通过 `obj.imports` 可以得到一个符号信息的字典：
```python
>>> for imp in obj . imports :
... print imp , obj . imports [ imp ]
...
strncmp < cle . backends . elf . relocation . amd64 . R_X86_64_GLOB_DAT object at 0x7faf8301b110 >
lseek < cle . backends . elf . relocation . amd64 . R_X86_64_GLOB_DAT object at 0x7faf8301b7d0 >
malloc < cle . backends . elf . relocation . amd64 . R_X86_64_GLOB_DAT object at 0x7faf8301be10 >
>>> obj . imports [ 'free' ] . symbol # 从重定向信息得到导入符号
< Symbol "free" in true ( import ) >
>>> obj . imports [ 'free' ] . owner_obj # 从重定向信息得到所属的 object
< ELF Object true , maps [ 0x400000 : 0x60721f ] >
```
这一部分还有个 hooking 机制，用于将共享库中的代码替换为其他的操作。使用函数 `proj.hook(addr, hook)` 和 `proj.hook_symbol(name, hook)` 来做到这一点，其中 `hook` 是一个 SimProcedure 的实例。通过 `.is_hooked` 、`.unhook` 和 `.hooked_by` 来进行管理：
```python
>>> stub_func = angr . SIM_PROCEDURES [ 'stubs' ][ 'ReturnUnconstrained' ] # 获得一个类
>>> stub_func
< class ' angr . procedures . stubs . ReturnUnconstrained . ReturnUnconstrained '>
>>> proj . hook ( 0x10000 , stub_func ()) # 使用类的一个实例来 hook
>>> proj . is_hooked ( 0x10000 )
True
>>> proj . hooked_by ( 0x10000 )
< SimProcedure ReturnUnconstrained >
>>> proj . hook_symbol ( 'free' , stub_func ())
17316528
>>> proj . is_symbol_hooked ( 'free' )
True
>>> proj . is_hooked ( 17316528 )
True
```
当然也可以利用装饰器编写自己的 hook 函数：
```python
>>> @proj.hook ( 0x20000 , length = 5 ) # length 参数可选，表示程序执行完 hook 后跳过几个字节
... def my_hook ( state ):
... state . regs . rax = 1
...
>>> proj . is_hooked ( 0x20000 )
True
```
#### 求解器引擎
从前面的内容中我们已经知道 bitvectors 是一个比特串，并且看到了 bitvectors 做的一些具体的数学运算。其实 bitvectors 不仅可以表示具体的数值，还可以表示虚拟的数值，即符号变量。
```python
>>> x = state . solver . BVS ( "x" , 64 )
>>> x
< BV64 x_0_64 >
>>> y = state . solver . BVS ( "y" , 64 )
>>> y
< BV64 y_1_64 >
```
而符号变量之间的运算同样不会时具体的数值，而是一个 AST， ：
```python
>>> x + 0x10
< BV64 x_0_64 + 0x10 >
>>> ( x + 0x10 ) / 2
< BV64 ( x_0_64 + 0x10 ) / 0x2 >
>>> x - y
< BV64 x_0_64 - y_1_64 >
```
每个 AST 都有一个 `.op` 和一个 `.args` 属性：
```python
>>> tree = ( x + 1 ) / ( y + 2 )
>>> tree
< BV64 ( x_0_64 + 0x1 ) / ( y_1_64 + 0x2 ) >
>>> tree . op # op 是表示操作符的字符串
'__floordiv__'
>>> tree . args # 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 L , 64 )
```
知道了符号变量的表示，接下来看符号约束：
```python
>>> x == 1 # AST 比较会得到一个符号化的布尔值
< Bool x_0_64 == 0x1 >
>>> x + y > 100
< Bool ( x_0_64 + y_1_64 ) > 0x64 >
>>> state . solver . BVV ( 1 , 64 ) > 0 # 无符号数 1
< Bool True >
>>> state . solver . BVV ( - 1 , 64 ) > 0 # 无符号数 0xffffffffffffffff
< Bool True >
```
正因为布尔值是符号化的，所以在需要做 if 或者 while 判断的时候，不要直接使用比较作为条件，而应该使用 `.is_true` 和 `.is_false` 来进行判断：
```python
>>> yes = state . solver . BVV ( 1 , 64 ) > 0
>>> yes
< Bool True >
>>> state . solver . is_true ( yes )
True
>>> state . solver . is_false ( yes )
False
>>> maybe = x == y
>>> maybe
< Bool x_0_64 == y_1_64 >
>>> state . solver . is_true ( maybe )
False
>>> state . solver . is_false ( maybe )
False
```
为了进行符号求解，首先要将符号化布尔值作为符号变量有效值的断言加入到 state 中，作为限制条件，当然如果添加了无法满足的限制条件，将无法求解：
```python
>>> state . solver . add ( x > y ) # 添加限制条件
[ < Bool x_0_64 > y_1_64 > ]
>>> state . solver . add ( y > 2 )
[ < Bool y_1_64 > 0x2 > ]
>>> state . solver . add ( 10 > x )
[ < Bool x_0_64 < 0xa > ]
>>> state . satisfiable () # 可以求解
True
>>> state . solver . eval ( x + y ) # eval 求解得到任意一个符合条件的值
15 L
>> state . solver . eval_one ( x + y ) # 求解得到结果，如果有不止一个结果则抛出异常
>>> state . solver . eval_upto ( x + y , 5 ) # 给出最多 5 个结果
[ 16 L , 13 L , 8 L , 9 L , 17 L ]
>>> state . solver . eval_atleast ( x + y , 5 ) # 给出至少 5 个结果，否则抛出异常
[ 16 L , 13 L , 8 L , 9 L , 17 L ]
>>> state . solver . eval_exact ( x + y , 5 ) # 有正好 5 个结果，否则抛出异常
>>> state . solver . min ( x + y ) # 给出最小的结果
7 L
>>> state . solver . max ( x + y ) # 给出最大的结果
17 L
>>> state . solver . eval ( x + y , extra_constraints = [ x + y < 10 , x + y > 5 ]) # 额外添加临时限制条件
8 L
>>> state . solver . eval ( x + y , cast_to = str ) # 指定输出格式
' \x00\x00\x00\x00\x00\x00\x00\x08 '
>>> state . solver . add ( x - y > 10 ) # 添加不可满足的限制条件
[ < Bool ( x_0_64 - y_1_64 ) > 0xa > ]
>>> state . satisfiable () # 无法求解
False
```
angr 使用 z3 作为约束求解器，而 z3 支持 IEEE754 浮点数的理论，所以我们也可以使用浮点数。使用 `FPV` 和 `FPS` 即可创建浮点数值和浮点符号：
```python
>>> state = proj . factory . entry_state () # 刷新状态
>>> a = state . solver . FPV ( 3.2 , state . solver . fp . FSORT_DOUBLE ) # 浮点数值
>>> a
< FP64 FPV ( 3.2 , DOUBLE ) >
>>> b = state . solver . FPS ( 'b' , state . solver . fp . FSORT_DOUBLE ) # 浮点符号
>>> b
< FP64 FPS ( 'FP_b_2_64' , DOUBLE ) >
>>> a + b
< FP64 fpAdd ( 'RNE' , FPV ( 3.2 , DOUBLE ), FPS ( 'FP_b_2_64' , DOUBLE )) >
>>> a + 1.1
< FP64 FPV ( 4.300000000000001 , DOUBLE ) >
>>> a + 1.1 > 0
< Bool True >
>>> b + 1.1 > 0
< Bool fpGT ( fpAdd ( 'RNE' , FPS ( 'FP_b_2_64' , DOUBLE ), FPV ( 1.1 , DOUBLE )), FPV ( 0.0 , DOUBLE )) >
>>> state . solver . add ( b + 2 < 0 )
[ < Bool fpLT ( fpAdd ( 'RNE' , FPS ( 'FP_b_2_64' , DOUBLE ), FPV ( 2.0 , DOUBLE )), FPV ( 0.0 , DOUBLE )) > ]
>>> state . solver . add ( b + 2 > - 1 )
[ < Bool fpGT ( fpAdd ( 'RNE' , FPS ( 'FP_b_2_64' , DOUBLE ), FPV ( 2.0 , DOUBLE )), FPV ( - 1.0 , DOUBLE )) > ]
>>> state . solver . eval ( b )
- 2.4999999999999996
```
bitvectors 和浮点数的转换使用 `raw_to_bv` 和 `raw_to_fp` ：
```python
>>> a . raw_to_bv ()
< BV64 0x400999999999999a >
>>> b . raw_to_bv ()
< BV64 fpToIEEEBV ( FPS ( 'FP_b_2_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_3_64 , DOUBLE ) >
```
或者如果我们需要指定宽度的 bitvectors， `val_to_bv` 和 `val_to_fp` ：
```python
>>> 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 ) >
```
#### 程序状态
`state.step()` 用于模拟执行的一个 basic block 并返回一个 SimSuccessors 类型的对象，由于符号执行可能产生多个 state， `.successors` 属性是一个列表，包含了所有可能的 state。
程序状态 state 是一个 SimState 类型的对象，`angr.factory.AngrObjectFactory` 类提供了创建 state 对象的方法：
- `.blank_state()` ：返回一个几乎没有初始化的 state 对象，当访问未初始化的数据时，将返回一个没有约束条件的符号值。
- `.entry_state()` ：从主对象文件的入口点创建一个 state。
- `.full_init_state()` ：与 entry_state() 类似，但执行不是从入口点开始，而是从一个特殊的 SimProcedure 开始，在执行到入口点之前调用必要的初始化函数。
- `.call_state()` ：创建一个准备执行给定函数的 state。
下面对这些方法的参数做一些说明：
- 所有方法都可以传入参数 `addr` 来指定开始地址
- 可以通过 `args` 传入参数列表，`env` 传入环境变量。类型可以是字符串，也可以是 bitvectors
- 通过传入一个符号 bitvector 作为 `argc` ，可以将 `argc` 符号化
- 对于 `.call_state(addr, arg1, arg2, ...)` ， `addr` 是希望调用的函数地址，`argN` 是传递给函数的 N 个参数，如果希望分配一个内存空间并传递指针，则需要使用 `angr.PointerWrapper()` ；如果需要指定调用约定，可以传递一个 SimCC 对象作为 `cc` 参数
创建的 state 可以很方便地复制和合并：
```python
>>> s = proj . factory . blank_state ()
>>> s1 = s . copy () # 复制 state
>>> s2 = s . copy ()
>>> s1 . mem [ 0x1000 ] . uint32_t = 0x41414141
>>> s2 . mem [ 0x1000 ] . uint32_t = 0x42424242
>>> ( s_merged , m , anything_merged ) = s1 . merge ( s2 ) # 合并将返回一个元组
>>> s_merged # 表示合并后的 state
< SimState @ 0x405000 >
>>> m # 描述 state flag 的符号变量
[ < Bool state_merge_1_14_16 == 0x0 > , < Bool state_merge_1_14_16 == 0x1 > ]
>>> anything_merged # 描述是否全部合并的布尔值
True
>>> aaaa_or_bbbb = s_merged . mem [ 0x1000 ] . uint32_t # 此时的值需要根据 state flag 来判断
>>> aaaa_or_bbbb
< uint32_t < BV32 Reverse (( if ( state_merge_1_14_16 == 0x1 ) then 0x42424242 else ( if ( state_merge_1_14_16 == 0x0 ) then 0x41414141 else 0x0 ))) > at 0x1000 >
```
我们已经知道使用 `state.mem` 可以很方便的操作内存，但如果你想要对内存进行原始的操作时，可以使用 `state.memory` 的 `.load(addr, size)` 和 `.store(addr, val)` ：
```python
>>> s = proj . factory . blank_state ()
>>> s . memory . store ( 0x4000 , s . solver . BVV ( 0x0123456789abcdef , 128 )) # 默认大端序
>>> s . memory . load ( 0x4008 , 8 ) # 默认大端序
< BV64 0x123456789abcdef >
>>> s . memory . load ( 0x4008 , 8 , endness = angr . archinfo . Endness . LE ) # 小端序
< BV64 0xefcdab8967452301 >
>>> s . mem [ 0x4008 ] . uint64_t . resolved # 与 mem 对比
< BV64 0xefcdab8967452301 >
>>> s . memory . store ( 0x4000 , s . solver . BVV ( 0x0123456789abcdef , 128 ), endness = angr . archinfo . Endness . LE ) # 小端序
>>> s . memory . load ( 0x4000 , 8 ) # 默认大端序
< BV64 0xefcdab8967452301 >
>>> s . memory . load ( 0x4000 , 8 , endness = angr . archinfo . Endness . LE ) # 小端序
< BV64 0x123456789abcdef >
>>> s . mem [ 0x4000 ] . uint64_t . resolved # 与 mem 对比
< BV64 0x123456789abcdef >
```
可以看到默认情况下 store 和 load 都使用大端序的方式，但可以通过指定参数 `endness` 来使用小端序。
通过 `state.options` 可以对 angr 的行为做特定的优化。我们既可以在创建 state 时将 option 作为参数传递进去，也可以对已经存在的 state 进行修改。例如：
```python
>>> s = proj . factory . blank_state ( add_options = { angr . options . LAZY_SOLVES }) # 启用 options
>>> s = proj . factory . blank_state ( remove_options = { angr . options . LAZY_SOLVES }) # 禁用 options
>>> s . options . add ( angr . options . LAZY_SOLVES ) # 启用 option
>>> s . options . remove ( angr . options . LAZY_SOLVES ) # 禁用 option
```
SimState 对象的所有内容（包括`memory` 、`registers` 、`mem` 等）都是以插件的形式存储的，这样做的好处是将代码模块化，如果我们想要在 state 中存储其他的数据，那么直接实现一个插件就可以了。
- `state.globals` ：实现了一个标准的 Python dict 的接口，通过它可以在一个 state 上存储任意的数据。
- `state.history` ：存储了一个 state 在执行过程中的路径历史数据，它是一个链表，每个节点表示一个执行，通过像 `history.parent.parent` 这样的方式进行遍历。为了得到 history 中某个具体的值，可以使用迭代器 `history.NAME` ，这样的值保存在 `history.recent_NAME` 。如果想要快速得到这些值的一个列表，可以查看 `.hardcopy` 。
- `history.descriptions` ：对 state 每次执行的描述的列表。
- `history.bbl_addrs` ：
- `history.jumpkinds` ：
- `history.guards` ：
- `history.events` ：
- `history.actions` ：通常是空的，但如果启用了 `options.refs` ，则会记录程序执行时访问的所有内存、寄存器和临时变量。
- `state.callstack` ：用于记录函数调用堆栈，它是一个链表，可以直接遍历 `state.callstack` 获得每个调用的 frame。
- `callstack.func_addr` ：当前正在执行的函数的地址。
- `callstack.call_site_addr` ：调用当前函数的 basic block 的地址。
- `callstack.stack_ptr` ：从当前函数开头开始计算的堆栈指针的值。
- `callstack.ret_addr` ：当前函数的返回地址。
#### 模拟管理器
（ ） ， ，
我们用一个小程序来作例子，它有 3 种可能性，也就是 3 条路径：
```c
#include <stdio.h>
#include <stdlib.h>
int main () {
int num = 0 ;
scanf ( "%d" , & num );
if ( num > 50 ) {
if ( num <= 100 ) {
printf ( "50 < num <= 100 \n " );
} else {
printf ( "100 < num \n " );
exit ( 1 );
}
} else {
printf ( "num <= 50 \n " );
}
}
// gcc example.c
```
模拟管理器最基本的功能是将一个 stash 里所有的 states 向前推进一个 basic block， `.step()` 来实现，而 `.run()` 方法可以直接执行到程序结束：
```python
>>> proj = angr . Project ( 'a.out' , auto_load_libs = False )
>>> state = proj . factory . entry_state ()
>>> simgr = proj . factory . simgr ( state ) # 创建 SimulationManager
>>> simgr
< SimulationManager with 1 active >
>>> simgr . active # active stash
[ < SimState @ 0x400640 > ]
>>> while len ( simgr . active ) == 1 : # 一直执行到 active stash 中有不止一个 state
... simgr . step ()
...
< SimulationManager with 1 active >
...
< SimulationManager with 1 active >
< SimulationManager with 2 active >
>>> simgr . active # 有 2 个 active state
[ < SimState @ 0x40078f > , < SimState @ 0x400763 > ]
>>> simgr . step () # 同时推进 2 个 state
< SimulationManager with 3 active >
>>> simgr . active # 得到 3 个 state
[ < SimState @ 0x400600 > , < SimState @ 0x40076b > , < SimState @ 0x400779 > ]
>>> simgr . run () # 一直执行到程序结束
< SimulationManager with 3 deadended >
>>> simgr . deadended # deadended stash
[ < SimState @ 0x1000068 > , < SimState @ 0x1000020 > , < SimState @ 0x1000068 > ]
```
于是我们得到了 3 个 deadended 状态的 state。这一状态表示一个 state 一直执行到没有后继者了，那么就将它从 active stash 中移除，放到 deadended stash 中。
stash 默认的类型有下面几种，当然你也可以定义自己的 stash：
- `active` ：默认情况下存储可以执行的 state。
- `deadended` ：当 state 无法继续执行时会被放到这里，包括没有更多的有效指令，没有可满足的后继状态，或者指令指针无效等。
- `pruned` ：当启用 `LAZY_SOLVES` 时，除非绝对必要，否则是不会在执行中检查 state 的可满足性的。当某个 state 被发现是不可满足的，则 state 会被回溯上去，以确定最早是哪个 state 不可满足。然后这之后所有的 state 都会被放到 `pruned` stash 中。
- `unconstrained` ：如果在 SimulationManager 创建时启用了 `save_unconstrained` ，则那些没有约束条件的 state 会被放到 `unconstrained` stash 中。
- `unsat` ：如果在 SimulationManager 创建时启用了 `save_unsat` ，则那些被认为不可满足的 state 会被放到 `unsat` stash 中。
另外还有一个叫做 `errored` 的列表，它不是一个 stash。如果 state 在执行过程中发生错误，则该 state 会被包装在一个 ErrorRecord 对象中，该对象包含 state 和引发的错误，然后这个对象被插入到 `errored` 中。
可以使用 `.move()` ，将 `filter_func` 筛选出来的 state 从 `from_stash` 移动到 `to_stash` ：
```python
>>> simgr . move ( from_stash = 'deadended' , to_stash = 'more_then_50' , filter_func = lambda s : '100' in s . posix . dumps ( 1 ))
< SimulationManager with 1 deadended , 2 more_then_50 >
```
每个 stash 都是一个列表，可以用列表的操作来遍历它，同时 angr 也提供了一些高级的方法，例如在 stash 名称前面加上 `one_` ，表示该 stash 的第一个 state； `mp_` ，将得到一个 [mulpyplexed ](https://github.com/zardus/mulpyplexer ) 版本的 stash：
```python
>>> for s in simgr . deadended + simgr . more_then_50 :
... print hex ( s . addr )
...
0x1000068 L
0x1000020 L
0x1000068 L
>>> simgr . one_more_then_50
< SimState @ 0x1000020 >
>>> simgr . mp_more_then_50
MP ([ < SimState @ 0x1000020 > , < SimState @ 0x1000068 > ])
>>> simgr . mp_more_then_50 . posix . dumps ( 0 )
MP ([ '-2424202024@' , '+0000000060 \x00 ' ])
```
最后再介绍一下模拟管理器所使用的探索技术（ ） ， ， ， `simgr.use_technique(tech)` 来实现，其中 tech 是一个 ExplorationTechnique 子类的实例。angr 内置的探索技术在 `angr.exploration_techniques` 下：
- `Explorer` ：该技术实现了 `.explore()` 功能，允许在探索时查找或避免某些地址。
- `DFS` ：深度优先搜索，每次只探索一条路径，其它路径会放到 `deferred` stash 中。直到当前路径探索结束，再从 `deferred` 中取出最长的一条继续探索。
- `LoopLimiter` ：限制路径的循环次数，超出限制的路径将被放到 `discard` stash 中。
- `LengthLimiter` ：限制路径的最大长度
- `ManualMergepoint` ：将程序中的某个地址标记为合并点，将在一定时间范围内到达的所有 state 合并在一起。
- `Veritesting` ：是[这篇论文 ](https://users.ece.cmu.edu/~aavgerin/papers/veritesting-icse-2014.pdf )的实现，试图识别出有用的合并点来解决路径爆炸问题。在创建 SimulationManager 时通过 `veritesting=True` 来开启。
- `Tracer` ：记录在某个具体输入下的执行路径，结果是执行完最后一个 basic block 的 state， `traced` stash 中。
- `Oppologist` ：当遇到某个不支持的指令时，它将具体化该指令的所有输入并使用 unicorn engine 继续执行。
- `Threading` ：将线程级并行添加到探索过程中。
- `Spiller` ：当处于 active 的 state 过多时，将其中一些转存到磁盘上以保持较低的内存消耗。
#### VEX IR 翻译器
， （ PyVEX ](https://github.com/angr/pyvex ) 作为 libVEX 的 Python 包装。当然也对 libVEX 做了一些修改，使其更加适用于程序分析。
@ -246,7 +737,7 @@ angr 使用了 VEX 作为二进制分析的中间表示。VEX IR 是由 Valgrind
```python
>>> import pyvex , archinfo
>>> bb = pyvex . IRSB ( ' \xc3 ' , 0x400400 , archinfo . ArchAMD64 ()) # 将一个位于 0x400400 的 AMD64 基本块（\xc3， ）
>>> bb . pp () # 打印
>>> bb . pp () # 打印 IRSB（ ）
IRSB {
t0 : Ity_I64 t1 : Ity_I64 t2 : Ity_I64 t3 : Ity_I64
@ -289,11 +780,11 @@ t1
'Ijk_Ret'
```
#### 体系结构信息收集
到这里 angr 的核心概念就介绍得差不多了，更多更详细的内容还是推荐查看官方教程和 API 文档。
## CTF 实例
6.2.3、 6.2.8。
## 参考资料
firmianay