附件,参考1,参考2
符号执行原理
基本概念
即初始参数用变量代替,模拟程序执行过程,维护执行到各个位置时的状态(用各个变量之间的代数关系表示)。
- 符号状态(Symbolic State)
当前状态所有参数的集合,用 σ σ σ 表示。集合中的每个元素用表示初始参数的变量表示。 - 路径约束(Path Constraint)
到达当前路径需要表示初始参数满足的关系,通常用 PC 表示。
例如下面的程序:
#include <bits/stdc++.h>using namespace std;int main() {int x, y, z;cin >> x >> y;z = 2 * y;if (x == z) {if (x > y + 10) {cout << "Path-1";} else {cout << "Path-2";}} else {cout << "Path-3";}return 0;
}
对应的程序框图如下:

用 x s i m x_{sim} xsim, y s i m y_{sim} ysim 分别表示初始输入的参数 x ,y 。
如果执行到 Path-1 ,则:
- σ = { x = x s i m , y = y s i m , z = 2 ⋅ y s i m } σ=\{x=x_{sim},y=y_{sim},z=2\cdot y_{sim}\} σ={x=xsim,y=ysim,z=2⋅ysim}
- PC = ( x s i m = 2 ⋅ y s i m ) ∧ ( x s i m > y s i m + 10 ) \text{PC}=(x_{sim}=2\cdot y_{sim}) \wedge ( x_{sim}>y_{sim}+10) PC=(xsim=2⋅ysim)∧(xsim>ysim+10)
约束求解
即根据符号执行求得的执行到目标位置时的状态,反推出初始时假设的各个变量的值。
例如上面计算出执行到 Path-1 时的 σ σ σ 和 PC 。如果执行到 Path-1 则应当满足 PC 为真,进一步推出 x s i m = 22 , y s i m = 11 x_{sim} = 22,y_{sim}=11 xsim=22,ysim=11 为一组合法解。
为了进行约数求解,angr 内置了 z3 约束求解器。
动态符号执行
由于 angr 分析基于的是低级语言,会涉及内存、寄存器等结构,如果全部符号化会使得路径约束变得十分复杂且没有必要。因此 angr 采取动态符号执行(Dynamic Symbloic Execution)或者叫做混合执行(Concolic Execution)的方式,即将关键变量符号化,其他变量都赋一个合理的初始值。angr 在默认情况下,只有从标准输入流中读取的数据会被符号化,其他数据都是具有实际值的。
angr 入门
以下面的程序为例,介绍 angr 的基本用法
//gcc example-1.c -o example-1
#include <stdio.h>
#include <stdlib.h>
#include <string.h>void encrypt(char *flag) {for (int i = 0; i < 13; i++) {flag[i] ^= i;flag[i] += 32;}
}// flag{G00dJ0b}
int main() {char flag[100] = {};scanf("%s", flag);if (strlen(flag) != 13) {printf("Wrong length!\n");exit(0);}encrypt(flag);if (!strcmp(flag, "\x86\x8d\x83\x84\x9f\x62\x56\x57\x8c\x63\x5a\x89\x91")) {printf("Right!\n");} else {printf("Wrong!\n");}return 0;
}
加载二进制文件
首先,angr 需要加载二进制文件。
import angr
proj = angr.Project('example-1')
符号执行状态——SimStae
前面介绍的符号执行的时维护的状态在 angr 中对应为 SimStae 类。其中初始状态需要我们来创建。
state = proj.factory.entry_state()
angr 中许多类的都需要通过 factory 获得,factory 是工厂的意思,可以理解为 proj 的 factory 给用户生产了许多类的实例,这里生产的实例是 SimState ,entry_state 函数用来获取程序入口点的状态,也就是初始状态。
state 中维护这内存、寄存器以及文件结构等参数。在初始状态时,我们可以设置其中一些参数,可以是参数也可以是具体数值。
在angr中,无论是具体值还是符号量都有相同的类型——claripy.ast.bv.BV,也就是BitVector的意思,BV后面的数字表示这个比特向量的位数。
- 创建 32bit 数值 666
claripy.BVV(666, 32) - 创建 32bit 变量
sym_varclaripy.BVS('sym_var', 32)
在本题目中,可以设置 stdin 参数。
sym_flag = claripy.BVS('flag', 60 * 8)
state = proj.factory.entry_state(stdin=sym_flag)
符号执行引擎——Simulation Managers
前面提到的符号执行在 angr 中的具体实现为 Simulation Managers 类。
simgr = proj.factory.simgr(state)
angr 符号执行的过程类似于 bfs 的过程。在到达一个条件分枝时,一个状态会分裂出多个状态分别进入各个分枝中。simgr.active 为当前存在的所有状态,simgr.step() 相当于所有状态都向下执行一步。
直接求解
我们可以直接设置需要执行到的目标位置
simgr.explore(find=0x40133D)
由于开了 PIE ,地址随机,angr 默认基址为 0x400000 ,当然也可以指定基址:
proj = angr.Project('example-1', load_options={'main_opts' : {'base_addr' : 0x400000}
})
此时的状态被保存到了 found这 个数组中,可以通过 simgr.found[0] 获取当前的状态,其中 dumps() 的参数 0,1,2 分别表示 stdin,stdout,stderr 的内容,直接输出即可,不需要前面设置 stdin 参数为变量。(貌似这个得和前面 simgr.explore 配合使用)
found = simgr.found[0]
print(found.posix.dumps(0))
完整代码:
import angrproj = angr.Project('example-1')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=0x40133D)
found = simgr.found[0]
print(found.posix.dumps(0))
# b'flag{G00dJ0b}\x00\x00\x02Z\x0e\x02\xe4\x00\x19\x08\x89\x00\x00\x01\x00\x00\x1a\x00\x1a\x02\x00<\x02\x00)\x00\x19\x04\x00\x19\x89\x89\x89\x01\x01\x0e\x01*\x8a\x00\x00\x02\x00\x10\x00\x00J'
求解参数
如果是求解前面设的参数,则需要设置求解器
solver = simgr.found[0].solver
之后求解参数
print(solver.eval(sym_flag, cast_to=bytes))
当然,求解器可以添加条件限制
比如在这个地址处添加 eax = 0 的条件限制。

solver.add(simgr.found[0].regs.eax == 0)
完整代码:
import angr
import claripyproj = angr.Project('example-1')
sym_flag = claripy.BVS('flag', 60 * 8)
state = proj.factory.entry_state(stdin=sym_flag)
simgr = proj.factory.simgr(state)
simgr.explore(find=0x40133B)
solver = simgr.found[0].solver
solver.add(simgr.found[0].regs.eax == 0)
print(solver.eval(sym_flag, cast_to=bytes))
# b'flag{G00dJ0b}\x00\x02\x89\x01J\x01\x8a\x89\x08\x02\x00I\x89\x02\x00\x00*\x01\x00\x01\x01\x01\x00\x01\x02\x02@\x00\x00\x00\x89)\x19\x003\x00\x01J\x01\x01*\x02\x00\x00\x00\x01\x00'
手动模拟
前面 simgr.explore 的过程其实可以手动模拟
思路是每 step 后遍历所有状态,当找位于目标地址的状态后,求解参数即可。
完整代码:
import sys
import angr
import claripyproj = angr.Project('example-1')
sym_flag = claripy.BVS('flag', 60 * 8)
state = proj.factory.entry_state(stdin=sym_flag)
simgr = proj.factory.simgr(state)
while len(simgr.active):for active in simgr.active:if active.addr == 0x40133D:print(active.solver.eval(sym_flag, cast_to=bytes))sys.exit(0)simgr.step()
# b'flag{G00dJ0b}\x00*\x1a-\x08\x02\x02\x00\x00\x0c\x01\x00*\x02))\x00***\x00\x00\x01\x02I\x1b(\x08D\xc1\x01\x01J\x8d\x01\x01\x00\x19\x08\x00K\x01\x00\x00\x01\x00\x00'
angr_explore
_angr_find
主要讲解 explore 函数中 find 的用法,前面已经介绍过了。
直接定位到目标地址。

import angrproj = angr.Project('_angr_find')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=0x80492F0)
found = simgr.found[0]
print(found.posix.dumps(0))
# b'CYSRBXIA'
_angr_avoid
主函数复杂,ida反编译不出来,直接看判断函数

可以看到只有同时满足 should_succeed 为真和 s1 = s2 时才正确。
其中 should_succeed 初值为 1 且仅在 avoid_me 函数中被赋为 0 。

而 avoid_me 被多次调用

如果避免执行到 avoid_me 函数,则搜索空间将大大降低。
import angrproj = angr.Project('_angr_avoid')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8049300, avoid=0x80492BB)
found = simgr.found[0]
print(found.posix.dumps(0))
# b'QBQRZMMV'
_angr_find_condition

代码由许多相似结构组成,最终目标地址有多个。

explore 函数中的 find 和 avoid 参数可以自定义功能。这里可以通过判断执行到当前位置时 stdout 的内容确定是否为目标地址。
import angrdef is_successful(state):return b'Good Job.' in state.posix.dumps(1)def should_avoid(state):return b'Try again.' in state.posix.dumps(1)proj = angr.Project('_angr_find_condition')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=is_successful, avoid=should_avoid)
print(simgr.found[0].posix.dumps(0))
# b'CNCDLYYH'
当然也参数可以简化为 lambda 表达式
import angrproj = angr.Project('_angr_find_condition')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
# b'CNCDLYYH'
angr_symbolic
前面提到创建 SimStae 类的时候可以设置某些参数为变量或值,这些参数可以是,如寄存器、某块内存甚至是某个文件。
_angr_symbolic_registers
ida 反编译不是很准确,需要分析具体汇编

首先 get_user_input 函数将输入结果依次放入 eax ,ebx ,edx 三个寄存器中。

紧接着将寄存器中的值分别作为三个函数的参数。

angr 中除了可以创建函数入口状态 factory.entry_state 外还可以创建空状态 blank_state 。
指定 blank_state 的地址以及寄存器中的值即可求解。
import angr
import claripyproj = angr.Project('_angr_symbolic_registers')
state = proj.factory.blank_state(addr=0x0804958F)
password0 = claripy.BVS('password0', 32)
password1 = claripy.BVS('password1', 32)
password2 = claripy.BVS('password2', 32)
state.regs.eax = password0
state.regs.ebx = password1
state.regs.edx = password2
simgr = proj.factory.simgr(state)
simgr.explore(find=0x080495EF)
solver = simgr.found[0].solver
print(f'password0: {hex(solver.eval(password0))}')
print(f'password1: {hex(solver.eval(password1))}')
print(f'password2: {hex(solver.eval(password2))}')
# password0: 0x729d64c2
# password1: 0x372c322
# password2: 0x189ff536
当然,直接复用前面 _angr_find_condition 的代码也可以求解。
_angr_symbolic_stack
关键函数:

通过 blank_state 获取初始状态, ebp 的值是未约束的。在这题中,我们之后要向栈中 push 符号值,并且通过 ebp 索引这些符号值(比如 [ebp+var_C] ),所以我们得让 ebp 有一个正确的初值了。ebp 的值是什么不重要,我们只需要保证它和esp的偏移是正确的即可。
我们将起始地址设在 scanf 函数之后的 0x80493EF 。
state = proj.factory.blank_state(addr=0x80493EF)
从 mov ebp, esp 开始到起始地址前,看 esp 的变化:

可以看到,esp 与 ebp 的关系为 ebp = esp + 0x18 + 4 + 4 + 4 +4 = esp + 40 。
state.regs.ebp = state.regs.esp + 40
可以看到,complex_function0 和 complex_function1 参数分别存放在 [ebp+var_C] 和 [ebp+var_10] 中。

其中 var_10 = -0x10 ,var_C = -0xC 。

在栈上对于位置的值,之后就是正常求解。
state.regs.esp = state.regs.ebp - 0xC + 4
password0 = claripy.BVS('password0', 32)
password1 = claripy.BVS('password1', 32)
state.stack_push(password0)
state.stack_push(password1)
state.regs.esp = state.regs.ebp - 40
完整代码如下:
import angr
import claripyproj = angr.Project('_angr_symbolic_stack')
state = proj.factory.blank_state(addr=0x80493EF)
state.regs.ebp = state.regs.esp + 40
state.regs.esp = state.regs.ebp - 0xC + 4
password0 = claripy.BVS('password0', 32)
password1 = claripy.BVS('password1', 32)
state.stack_push(password0)
state.stack_push(password1)
state.regs.esp = state.regs.ebp - 40
simgr = proj.factory.simgr(state)
simgr.explore(find=0x804943C)
solver = simgr.found[0].solver
print(f'password0: {hex(solver.eval(password0))}')
print(f'password1: {hex(solver.eval(password1))}')
# password0: 0xef03928
# password1: 0x46731955
_angr_symbolic_memory

这次数据读入的位置是固定的内存地址,因此直接在对应地址处设置变量。
password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
password2 = claripy.BVS('password2', 64)
password3 = claripy.BVS('password3', 64)
state.mem[0xB53A820].uint64_t = password0
state.mem[0xB53A820 + 8].uint64_t = password1
state.mem[0xB53A820 + 16].uint64_t = password2
state.mem[0xB53A820 + 24].uint64_t = password3
如果我们要获取内存中的数据(具体值或者符号值),可以这样用
state.mem[0xA1BA1C0].uint64_t.resolved
完整代码如下:
import angr
import claripyproj = angr.Project('_angr_symbolic_memory')
state = proj.factory.blank_state(addr=0x8049315)
password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
password2 = claripy.BVS('password2', 64)
password3 = claripy.BVS('password3', 64)
state.mem[0xB53A820].uint64_t = password0
state.mem[0xB53A820 + 8].uint64_t = password1
state.mem[0xB53A820 + 16].uint64_t = password2
state.mem[0xB53A820 + 24].uint64_t = password3
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8049381)
solver = simgr.found[0].solver
print(f'password0: {solver.eval(password0, cast_to=bytes)}')
print(f'password1: {solver.eval(password1, cast_to=bytes)}')
print(f'password2: {solver.eval(password2, cast_to=bytes)}')
print(f'password3: {solver.eval(password3, cast_to=bytes)}')
# password0: b'MUPROSTX'
# password1: b'OWBBFEQD'
# password2: b'IHRUZBZU'
# password3: b'PZRKTOZX'
这里会发现直接输入求得的结果并不能通过检验,这是因为端序的问题,程序输入时输入函数自动进行端序的转换使其变为小端序存放在内存中,而内存设置的是端序转换后的结果。
实际输入应为:
XTSORPUM DQEFBBWO UZBZURHI XZOTKRZP
_angr_symbolic_dynamic_memory

这次采用的是动态分配内存,内存地址不确定。
但是我们可以设置内存指针的值,然后在指针指向的内存区域设置参数求解。
比如我们可以设置内存地址为bss起始位置。

password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
state.mem[0x804C040].uint64_t = password0
state.mem[0x804C040 + 8].uint64_t = password1
之后设置两个指针 buffer0 和 buffer1 指向对应内存。
state.mem[0xA3FA020].uint32_t = 0x804C040
state.mem[0xA3FA028].uint32_t = 0x804C040 + 8
之后就是常规的求解过程。
完整代码如下:
import angr
import claripyproj = angr.Project('_angr_symbolic_dynamic_memory')
state = proj.factory.blank_state(addr=0x804938C)
password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
state.mem[0x804C040].uint64_t = password0
state.mem[0x804C040 + 8].uint64_t = password1
state.mem[0xA3FA020].uint32_t = 0x804C040
state.mem[0xA3FA028].uint32_t = 0x804C040 + 8
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8049452)
solver = simgr.found[0].solver
print(f'password0: {solver.eval(password0, cast_to=bytes)}')
print(f'password1: {solver.eval(password1, cast_to=bytes)}')
# password0: b'KWVBCKPX'
# password1: b'GSBFNQGX'
_angr_symbolic_file
主函数逻辑如下:

先向 buffer 中读入数据,然后执行 ignore_me 函数后再从 XTQAFOST.txt 中读入数据到 buffer。
ignore_me 函数的关键部分如下:

可见之后再次读入到 buffer 中的数据还是输入数据。
因此我们可以直接对文件的内容进行符号化。
要对文件内容进行符号化,首先我们要创建一个模拟的文件 SimFile ,文件名为 XTQAFOST.txt ,内容为 8 字节的符号值,大小为 0x40 字节:
password0 = claripy.BVS('password0', 0x40)
sim_file = angr.SimFile(name='XTQAFOST.txt', content=password0, size=0x40)
后插入到 state 的文件系统(FileSystem)中,state 的文件系统可以通过 state.fs 获得:
state.fs.insert('XTQAFOST.txt', sim_file)
之后就是常规求解了。
完整代码如下:
import angr
import claripyproj = angr.Project('_angr_symbolic_file')
state = proj.factory.blank_state(addr=0x8049564)
password0 = claripy.BVS('password0', 0x40)
sim_file = angr.SimFile(name='XTQAFOST.txt', content=password0, size=0x40)
state.fs.insert('XTQAFOST.txt', sim_file)
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8049635)
solver = simgr.found[0].solver
print(f'password0: {solver.eval(password0, cast_to=bytes)}')
# password0: b'XLCQLBYI'
angr_constraints
angr在符号执行的过程中,会将路径约束保存在SimState内置的约束求解器内。但是存在一些特殊的情况,使得状态数迅速增长导致 angr 无法求解。这种现象称为路径爆炸。下面举一个利用 constraints 手动添加限制解决路径爆炸的例子:
主程序十分简单。

然而直接求解是求不出来的,问题出在 check_equals_XCKPBIWXXTQAFOST 函数上:

由于这里进行了 16 次 if 判断,每次判断时一个状态会分裂出两个状态,因此经过这个函数状态数膨胀了 2 16 2^{16} 216 倍,直接导致 angr 路径爆炸。
解决这个路径爆炸的方法十分简单。因为这个函数本质上是一个比较函数,因此可以在这个函数调用之前加一条限制就可以完美解决了。
simgr.explore(find=0x80493A4)
found = simgr.found[0]
found.add_constraints(found.memory.load(buffer_addr, 16) == b'XCKPBIWXXTQAFOST')
完整代码如下:
import angr
import claripyproj = angr.Project('_angr_constraints')
state = proj.factory.blank_state(addr=0x804935D)
password = claripy.BVS('password', 16 * 8)
buffer_addr = 0x804C040
state.memory.store(buffer_addr, password)
simgr = proj.factory.simgr(state)
simgr.explore(find=0x80493A4)
found = simgr.found[0]
found.add_constraints(found.memory.load(buffer_addr, 16) == b'XCKPBIWXXTQAFOST')
print(found.solver.eval(password, cast_to=bytes))
# b'IOXDQYNPQNLWCMRT'
angr_hooks
angr hooks 即将程序中的的函数用自己实现或 angr 自带的函数替代,这种方法可以解决路径爆炸问题。
_angr_hooks
可以看出,程序分两次输入和加密,因此前面直接添加条件限制的方式不太适合。

考虑将 check_equals_XCKPBIWXXTQAFOST hook。

@proj.hook(addr=0x80493CE, length=5)
def my_check_equals(state):buffer_addr = 0x804C044buffer = state.memory.load(buffer_addr, 16)state.regs.eax = claripy.If(buffer == b'XCKPBIWXXTQAFOST', claripy.BVV(1, 32), claripy.BVV(0, 32))
这一部分可以写作如下形式:
def my_check_equals(state):buffer_addr = 0x804C044buffer = state.memory.load(buffer_addr, 16)state.regs.eax = claripy.If(buffer == b'XYMKBKUHNIQYNQXE', claripy.BVV(1, 32), claripy.BVV(0, 32))proj.hook(addr=0x80493CE, hook=my_check_equals, length=5)
length = 5 指的是指令地址跳过 5 字节。这里 hook 是将地址替换,而 call 指令本身为 E8 E5 EE FF FF 占 5 字节,需要跳过。
经过 hook 后就可以正常求解了。
import angr
import claripyproj = angr.Project('_angr_hooks')# @proj.hook(addr=0x80493CE, length=5)
# def my_check_equals(state):
# buffer_addr = 0x804C044
# buffer = state.memory.load(buffer_addr, 16)
# state.regs.eax = claripy.If(buffer == b'XCKPBIWXXTQAFOST', claripy.BVV(1, 32), claripy.BVV(0, 32))def my_check_equals(state):buffer_addr = 0x804C044buffer = state.memory.load(buffer_addr, 16)state.regs.eax = claripy.If(buffer == b'XYMKBKUHNIQYNQXE', claripy.BVV(1, 32), claripy.BVV(0, 32))proj.hook(addr=0x80493CE, hook=my_check_equals, length=5)
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
# b'ZXIDRXEORJOTFFJNWYDFOSDBYRLSUABZ'
_angr_simprocedures
前面的 hook 只是替换调用函数时的函数地址,但是当一个函数被多次调用的时候就需要 hook 函数本身。
如下图所示,程序结果十分复杂。

并且造成路径爆炸的 check_equals_XCKPBIWXXTQAFOST 函数被多次调用。

考虑 hook check_equals_XCKPBIWXXTQAFOST 函数本身。angr 对函数本身进行 hook 的方法为 SimProcedures ,定义一个 SimProcedures 的代码如下:
class MyCheckEquals(angr.SimProcedure):def run(self, buffer_addr, length):buffer = self.state.memory.load(buffer_addr, length)return claripy.If(buffer == b'XCKPBIWXXTQAFOST', claripy.BVV(1, 32), claripy.BVV(0, 32))
SimProcedure 中的 run 函数由子类实现,其接收的参数与 C 语言中的参数保持一致,返回为对应原函数的返回值。
定义好了 SimProcedure 之后,我们需要调用 hook_symbol 函数对程序中名为 check_equals_XCKPBIWXXTQAFOST 的函数进行 hook :
proj.hook_symbol(symbol_name='check_equals_XCKPBIWXXTQAFOST', simproc=MyCheckEquals())
完整代码如下:
import angr
import claripyclass MyCheckEquals(angr.SimProcedure):def run(self, buffer_addr, length):buffer = self.state.memory.load(buffer_addr, length)return claripy.If(buffer == b'XCKPBIWXXTQAFOST', claripy.BVV(1, 32), claripy.BVV(0, 32))proj = angr.Project('_angr_simprocedures')
proj.hook_symbol(symbol_name='check_equals_XCKPBIWXXTQAFOST', simproc=MyCheckEquals())
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
# b'VDOWLVMQTSSFNZGK'
angr_veritesting
Veritesting 意为路径归并,出自2014年的一篇论文 Enhancing Symbolic Execution with Veritesting ,是一种解决路径爆炸的方法。
如下图,主程序中引起路径爆炸的不是单独的函数,且加密过程在循环中,前面防止路径爆炸的方法失效。

设置参数 veritesting=True 即可。
import angrproj = angr.Project('angr_veritesting')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state, veritesting=True)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
# b'AFKPUZEJOTYDINSXCHMRWBGLQVAFKPUZ'
这种写法与上面的写法是等价的:
simgr = proj.factory.simgr(state)
simgr.use_technique(angr.exploration_techniques.Veritesting())
另外根据官方的说法:
Note that it frequenly doesn’t play nice with other techniques due to the invasive way it implements static symbolic execution.
Versitesting 通常与其他 exploration techniques 不兼容。
angr_library
_angr_static_binary
如果程序采用静态编译,则 angr 直接求解会使得符号执行陷入库函数的代码中导致求解时间过长,这就需要前面介绍的 _angr_simprocedures 的函数 hook 技术,而库函数 angr 有提前写好的 SimProcedures ,直接用即可。
import angrproj = angr.Project('_angr_static_binary')
proj.hook_symbol('printf', angr.SIM_PROCEDURES['libc']['printf']())
proj.hook_symbol('__isoc99_scanf', angr.SIM_PROCEDURES['libc']['scanf']())
proj.hook_symbol('strcmp', angr.SIM_PROCEDURES['libc']['strcmp']())
proj.hook_symbol('puts', angr.SIM_PROCEDURES['libc']['puts']())
proj.hook_symbol('__libc_start_main', angr.SIM_PROCEDURES['glibc']['__libc_start_main']())
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
# b'XROIJFIY'
_angr_shared_library
利用 angr 对动态链接库中单个的函数进行符号执行。
关键函数为 validate 。

该函数位于动态链接库中

在对应的动态链接库中找到对应的函数

通过 call_state 创建调用函数的状态:
state = proj.factory.call_state(validate_addr, claripy.BVV(password_addr, 32), length)
这里要注意的是,函数 validate 的参数为 password 的指针,而不是字符串本身。
因此需要在内存中选择某区域存放 password 的变量。
password = claripy.BVS('password', 8 * 8)
password_addr = 0x4024
state.memory.store(password_addr, password)
完整代码如下:
import angr
import claripyproj = angr.Project('_angr_shared_library.so')
validate_addr = 0x40129C
password = claripy.BVS('password', 8 * 8)
password_addr = 0x4024
length = claripy.BVV(8, 32)
state = proj.factory.call_state(validate_addr, claripy.BVV(password_addr, 32), length)
state.memory.store(0x4024, password)
simgr = proj.factory.simgr(state)
simgr.explore(find=0x401348)
found = simgr.found[0]
found.solver.add(found.regs.eax != 0)
print(found.solver.eval(password, cast_to=bytes))
# XNGWTLKW
angr_overflow
_angr_arbitrary_read
简单的栈溢出漏洞,v4 可以溢出覆盖 s 为 Good Job. 地址。

直接求解不行,因为 puts 的输出内容的由 v4 溢出覆盖的地址确定,而 angr 事先不知道 Good Job. 的地址,导致无法求解。
import angrproj = angr.Project('15_angr_arbitrary_read')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
这里可以把条件改为判断 puts 的参数是否为 Good Job. 的地址。
可以先符号执行到这里

然后判断 eax 是否为 Good Job. 的地址。
import angrproj = angr.Project('_angr_arbitrary_read')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8049259)
found = simgr.found[0]
found.add_constraints(found.regs.eax == 0x58434B4F)
print(simgr.found[0].posix.dumps(0))
# b'0004074803 \xd9\xd9Y\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9OKCX'
当然,这个过程可以自动判断:
def check_puts(state):puts_parameter = state.memory.load(state.regs.esp + 4, 4, endness=proj.arch.memory_endness)if state.solver.symbolic(puts_parameter):good_job_string_address = 0x58434B4Fis_vulnerable_expression = puts_parameter == good_job_string_addresscopied_state = state.copy()copied_state.add_constraints(is_vulnerable_expression)if copied_state.satisfiable():state.add_constraints(is_vulnerable_expression)return Truereturn Falsedef is_successful(state):puts_address = 0x08049090if state.addr == puts_address:return check_puts(state)return Falsesimgr.explore(find=is_successful)
完整代码如下:
import angrdef check_puts(state):puts_parameter = state.memory.load(state.regs.esp + 4, 4, endness=proj.arch.memory_endness)if state.solver.symbolic(puts_parameter):good_job_string_address = 0x58434B4Fis_vulnerable_expression = puts_parameter == good_job_string_addresscopied_state = state.copy()copied_state.add_constraints(is_vulnerable_expression)if copied_state.satisfiable():state.add_constraints(is_vulnerable_expression)return Truereturn Falsedef is_successful(state):puts_address = 0x08049090if state.addr == puts_address:return check_puts(state)return Falseproj = angr.Project('_angr_arbitrary_read')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=is_successful)
print(simgr.found[0].posix.dumps(0))
# b'0004074803 \xd9\xd9\x99\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9OKCX'
_angr_arbitrary_write
这次是覆盖 *dest 指针指向 password_buffer 然后向其中写入 BIWXXTQA 。

和上道题思路一样,这次检查 strncpy 的参数。
import angr
import claripydef check_strncpy(state):dest = state.memory.load(state.regs.esp + 4, 4, endness=proj.arch.memory_endness)src = state.memory.load(state.regs.esp + 8, 4, endness=proj.arch.memory_endness)src_content = state.memory.load(src, 8)if state.solver.symbolic(src_content) and state.solver.symbolic(dest):if state.satisfiable(extra_constraints=[claripy.And(src_content == b'BIWXXTQA', dest == 0x58434B40)]):state.add_constraints(claripy.And(src_content == b'BIWXXTQA', dest == 0x58434B40))return Truereturn Falsedef is_successful(state):strncpy_address = 0x80490F0if state.addr == strncpy_address:return check_strncpy(state)return Falseproj = angr.Project('_angr_arbitrary_write')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=is_successful)
print(simgr.found[0].posix.dumps(0))
# b'0061440360 BIWXXTQA\xd9\xd9\xd9\xd9\xd9\xd8\xd9\xd9@KCX'
_angr_arbitrary_jump
栈溢出

目标是让程序执行到这里

当一个指令有很多分支的可能性时,称之为不受约束(unconstrained)的状态, 比如说当用户的输入决定下一条指令的位置。angr 在遇到不受约束的状态时会将其抛出,本题将要关闭这个默认行为,转而利用此状态去求解能够跳转到 print_good 函数的payload。
import angr
import claripyproj = angr.Project('_angr_arbitrary_jump')
payload = claripy.BVS('payload', 64 * 8)
state = proj.factory.entry_state(stdin=payload)
simgr = proj.factory.simgr(state,save_unconstrained=True,stashes={'active': [state],'unconstrained': [],'found': [],})
while (len(simgr.active) or len(simgr.unconstrained)) and not len(simgr.found):for unconstrained in simgr.unconstrained:eip = unconstrained.regs.eipprint_good_addr = 0x58434B58if unconstrained.satisfiable(extra_constraints=[eip == print_good_addr]):unconstrained.add_constraints(eip == print_good_addr)simgr.move('unconstrained', 'found')breaksimgr.drop(stash="unconstrained")simgr.step()
print(simgr.found[0].posix.dumps(0))
# b'\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xd2\xdaXKCX\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\x00\x00\x00\x00\x00'

















