angr入门

什么Angr

Angr 是一个功能强大且灵活的二进制分析框架，广泛应用于逆向工程、安全研究和漏洞检测等领域。它结合了多种技术（例如：静态分析、动态分析、符号执行等）（具体可参考The Art of War: Offensive Techniques in Binary Analysis），支持多种平台和架构，使得用户可以高效地分析和操作二进制文件。

angr 入门文档及API可参考：

接下来直接上题，以Github上的angr_ctf项目进行angr的使用学习。

AngrCTF

基本用法

00_angr_find

IDA查看伪代码如下：

从输入流中读取8字节字符串，经过complex_function函数处理，最后与JACEJGCS作比较。

angr会自动处理 scanf 的简单格式的输入，也会自动添加并处理分支路径的约束条件，从而求得到达目标路径的输入。当然我们也可以手动注入符号替换scanf的输入（需在scanf之后注入）。

这题主要是让我们熟悉angr的基本用法：

  1. 创建Project。
  2. 创建初始state。
  3. 将待求解的变量符号化，存储对应内存空间中。
  4. 创建simgr求解器，指定求解成功的目标路径（以及应该避免的路径）。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
import sys

import angr
import claripy

# open binary file
proj = angr.Project('./00_angr_find')
# get the entry state
init_state = proj.factory.entry_state()

# try solve
simgr = proj.factory.simgr(init_state)
success_addr = 0x0804867D
simgr.explore(find=success_addr)

if simgr.found:
    solver_state = simgr.found[0]
    print(solver_state.posix.dumps(sys.stdin.fileno()).decode())
else:
    print("Could not find the solution")

01_angr_avoid

函数体太大，索性直接看汇编代码，在main函数中，首先要求输入8字节字符。

然后进入complex_function函数进行处理

之后就是一堆相似的汇编代码。其中会调用avoid_me函数以及maybe_good函数。

显然，我们不能让程序进入到avoid_me函数中。因此在使用 angr 求解过程中，应对进入avoid_me函数的状态不再进行后续执行，简而言之就是截枝，以防止路径爆炸，具体操作是通过simgr.explore()的avoid参数指定。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
import sys, angr

proj = angr.Project("./01_angr_avoid")
init_state = proj.factory.entry_state()
simgr = proj.factory.simgr(init_state)
success_addr = 0x080485E0
avoid_addr = 0x080485A8

simgr.explore(find=success_addr, avoid=avoid_addr)

if simgr.found:
    solve_state = simgr.found[0]
    print(solve_state.posix.dumps(sys.stdin.fileno()).decode())
else:
    print("Could not find the solution")

02_angr_find_condition

有很多输出Try again.和Good Job.的地方（对应的地址不同），因此将simgr.explore()的find和avoid参数指定为地址就不管用了。不过参数 find 与 avoid 除了可以是目标地址外，还可以支持自定义函数，该函数的参数为模拟状态，返回值为布尔类型。

这样一来，我们就可以编写自定义函数来判断一个状态是否是我们应当要寻找的状态。该自定义函数的功能应该如下：

  • 如果当前state进入到输出Try again.的地方，此时它的标准输出流中就会存在Try again.字符串，通过判断这一特征，可对满足条件的state进行截支（即avoid）。
  • 如果当前state进入到输出Good Job.的地方，此时它的标准输出流中就会存在Good Job.字符串，通过判断这一特征，可以知道当前state是否是我们的目标state（即find）。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
import angr, sys

def is_find_state(state):
    return b'Good Job.' in state.posix.dumps(sys.stdout.fileno())

def is_avoid_state(state):
    return b'Try again.' in state.posix.dumps(sys.stdout.fileno())

proj = angr.Project('./02_angr_find_condition')
init_state = proj.factory.entry_state()
simgr = proj.factory.simgr(init_state)
simgr.explore(find=is_find_state, avoid=is_avoid_state)

if simgr.found:
    solve_state = simgr.found[0]
    print(solve_state.posix.dumps(sys.stdin.fileno()).decode())
else:
    print("no found")

符号化

03_angr_symbolic_registers

IDA反编译出一地鸡毛，直接看汇编代码吧。get_user_input函数读取三个数存放在eax, ebx, edx寄存器中。

然后将这三个数又分别存放在ebp+var_14, ebp+var_10, ebp+var_C 对应地址空间中，之后对这三个数分别调用complex_function_x函数进行处理，如果这三个函数的返回结果都为0，则打印Good Job.。

这里其实可以有很多做法：

  • 设置初始state为stdin之后，符号化堆栈中ebp+var_14, ebp+var_10, ebp+var_C 的地址空间（这种做法见下一题）。
  • 设置初始state为stdin之后，符号化eax, ebx, edx寄存器。
  • 设置初始state为程序入口处，不符号化，使用上一题的脚本也可求解。

根据题目意思，就符号化寄存器吧，需要注意的是，由于我们符号化的是get_user_input函数执行之后的寄存器，因此需要通过blank_state()设置初始状态为在此之后，否则执行不成功。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
import angr
import claripy

proj = angr.Project('./03_angr_symbolic_registers')

# 创建待求解的bvs
bvs_v1 = claripy.BVS('v1', 32) #4bytes
bvs_v2 = claripy.BVS('v2', 32) #4bytes
bvs_v3 = claripy.BVS('v3', 32) #4bytes

# 跳过get_user_input函数，设置angr初始求解状态为调用get_user_input函数之后
start_state = 0x08048980
init_state = proj.factory.blank_state(addr=start_state)

# 将eax,ebx,edx的值设置为对应的bvs，即替换get_user_input函数的返回值（三个输入的数字）
init_state.regs.eax = bvs_v1
init_state.regs.ebx = bvs_v2
init_state.regs.edx = bvs_v3

find_addr = 0x080489E9
simgr = proj.factory.simgr(init_state)
simgr.explore(find=find_addr)

if simgr.found:
    solve_state = simgr.found[0]
    v1 = solve_state.solver.eval(bvs_v1)
    v2 = solve_state.solver.eval(bvs_v2)
    v3 = solve_state.solver.eval(bvs_v3)
    print(f'v1 = {hex(v1)}, v2 = {hex(v2)}, v3 = {hex(v3)}')
else:
    print("no found")

04_angr_symbolic_stack

题目内容很简单，就是输入两个数v1、v2，进行complex_function()函数操作，最后与固定值比较，相等则输出Good Job，否则输出Try again。

思路也很简单，就是符号化v1、v2，但注意到v1、v2是在栈上的，且没有像题03那样借助寄存器传送输入值到栈上，因此我们只能符号化栈上的变量。

具体做法为：

  1. 使用blank_state()创建 scanf 之后的空白状态作为初始状态。（如果使用entry_state()创建以程序入口为初始状态，求解会失败，个人认为可能是执行了 scanf 函数，覆盖了我们设置的符号变量）
  2. 设置esp的值为ebp的值，恢复栈帧初始状态。然后设置 ebp 和 esp 的相对位置，最后使用 state.stack_push(val) 来手动地将符号变量推到栈上。
  3. 设置find路径，进行求解。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
import angr
import claripy

proj = angr.Project('./04_angr_symbolic_stack')

start_addr = 0x08048697
init_state = proj.factory.blank_state(addr=start_addr)

bvs_v1 = claripy.BVS('v1', 32)# 4bytes
bvs_v2 = claripy.BVS('v2', 32)# 4bytes

# 将esp指针恢复到和ebp指针一致，恢复栈帧初始状态
init_state.regs.ebp = init_state.regs.esp
# 设置esp和ebp的初始相对位置，由于第一个变量值在esp-0xC的地址中，因此初始相对位置0x8（注意此程序在32bit系统下执行）
init_state.regs.esp -= 0x8
# 符号变量入栈
init_state.stack_push(bvs_v1)# -0x4, esp-0xC
init_state.stack_push(bvs_v2)# -0x8, esp-0x10

find_addr = 0x080486E4
simgr = proj.factory.simgr(init_state)
simgr.explore(find=find_addr)

if simgr.found:
    solve_state = simgr.found[0]
    v1 = solve_state.solver.eval(bvs_v1)
    v2 = solve_state.solver.eval(bvs_v2)
    print(f'v1 = {v1}, v2 = {v2}')
else:
    print("no found")

05_angr_symbolic_memory

IDA反汇编如下。在user_input变量是一个全局变量，地址固定，然后这些空间接收4个8字节的输入字符串（这些变量在空间上连续）

想法很简单，就是符号化接收输入的变量，但它们是全局变量（位于bss段）。为此 angr 提供了如下接口供我们操作内存：

  • state.memory.load(addr, size_in_bytes) ：获取该地址上指定大小的位向量。
  • state.memory.store(addr, bitvector) ：将一个位向量存储到指定地址。

需要注意的是如果要储存的数值，则需要通过 endness 参数指定大小端序，字符串则不需要。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
import angr
import claripy

proj = angr.Project('./05_angr_symbolic_memory')

start_addr = 0x08048601
init_state = proj.factory.blank_state(addr=start_addr)

user_input_size = 8 * 8 # 8bytes 
bvs_user_input_0 = claripy.BVS('user_input_0', user_input_size)
bvs_user_input_1 = claripy.BVS('user_input_1', user_input_size)
bvs_user_input_2 = claripy.BVS('user_input_2', user_input_size)
bvs_user_input_3 = claripy.BVS('user_input_3', user_input_size)

user_input_addr = 0x0A1BA1C0
init_state.memory.store(user_input_addr, bvs_user_input_0)
init_state.memory.store(user_input_addr + 0x08, bvs_user_input_1)
init_state.memory.store(user_input_addr + 0x10, bvs_user_input_2)
init_state.memory.store(user_input_addr + 0x18, bvs_user_input_3)


simgr = proj.factory.simgr(init_state)
find_addr = 0x0804866D
simgr.explore(find=find_addr)

if simgr.found:
    solve_state = simgr.found[0]
    u0 = solve_state.solver.eval(bvs_user_input_0, cast_to=bytes)
    u1 = solve_state.solver.eval(bvs_user_input_1, cast_to=bytes)
    u2 = solve_state.solver.eval(bvs_user_input_2, cast_to=bytes)
    u3 = solve_state.solver.eval(bvs_user_input_3, cast_to=bytes)
    print(f'user_input = {u0}, {u1}, {u2}, {u3}')
else:
    print("no found")

06_angr_symbolic_dynamic_memory

动态分配内存，这导致buffer0和buffer1指向的内存地址不固定，但是buffer0和buffer1是全局变量，地址是固定的。

由于动态分配内存的缘故，我们无法确定所要符号化的内存地址。但是我们可以这么做：

  1. 让buffer0和buffer1指向我们所设定的内存地址（称之为假地址），这片内存等同于动态分配的内存。
  2. 将待求解变量符号化，存储到假地址所在内存空间中，之后按照正常流程求解。

由于符号执行并不会真正运行程序，它只是模拟程序的运行状态，因此伪造任何地址都不会导致程序出现问题。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
import angr
import claripy

proj = angr.Project('./06_angr_symbolic_dynamic_memory')

# scanf之后的状态为初始状态
start_addr = 0x08048699
init_state = proj.factory.blank_state(addr=start_addr)

# 让buffer指向假地址，对应malloc开辟的空间，需注意大小端
buffer0_addr = 0x0ABCC8A4
buffer1_addr = 0x0ABCC8AC
fake_buffer0_addr = 0x0ABCC860
fake_buffer1_addr = 0x0ABCC874
init_state.memory.store(buffer0_addr, fake_buffer0_addr, endness=proj.arch.memory_endness)
init_state.memory.store(buffer1_addr, fake_buffer1_addr, endness=proj.arch.memory_endness)

# 创建bvs并存放到假地址空间中
buffer_size = 8 * 8 # 8bytes
bvs_buffer0 = claripy.BVS('buffer0', buffer_size)
bvs_buffer1 = claripy.BVS('buffer1', buffer_size)
init_state.memory.store(fake_buffer0_addr, bvs_buffer0)
init_state.memory.store(fake_buffer1_addr, bvs_buffer1)

# 模拟执行
simgr = proj.factory.simgr(init_state)
find_addr = 0x08048759
simgr.explore(find=find_addr)

if simgr.found:
    solve_state = simgr.found[0]
    b0 = solve_state.solver.eval(bvs_buffer0, cast_to=bytes)
    b1 = solve_state.solver.eval(bvs_buffer1, cast_to=bytes)
    print(f'buffer = {b0}, {b1}')
else:
    print("no found")

07_angr_symbolic_file

这个题目的特殊操作在于：涉及到文件读写操作，ignore_me函数将buffer中的数据写入文件中（写了两次，第二次是覆写），fread将文件中的数据又读回buffer中。这题可以利用 angr 的仿真文件系统。

Emulated Filesystem

在 angr 中与文件系统之间的操作是通过SimFile对象完成的。SimFile是对存储的抽象模型，一个 SimFile对象可以表示一系列的字节、符号等。以下是它的一些用法：

1
2
3
4
5
6
7
8
9
10
11
# 创建模拟文件
sim_file = angr.SimFile(filename, content = "flag{F4k3_f1@9!}\n", size=size_bytes)
sim_file = angr.storage.SimFile(filename, content=bvs_password, size=size_bytes)
# 读
data, size, new_pos = sim_file.read(pos, size)
# 写
new_pos = sim_file.write(pos, data)
# 模拟文件与程序中的真实文件进行关联
state.fs.insert(realname, simfile)
# 删除关联
state.fs.delete(realname)

exp

我们的具体操作是创建一个模拟文件，存储待求解的符号化变量，然后与程序中真实的文件进行关联，最后正常求解。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
import angr
import claripy

proj = angr.Project('./07_angr_symbolic_file')

# ingore_me之后，创建模拟文件和待求解的bvs（放入模拟文件中），模拟文件关联state
start_addr = 0x080488D6
init_state = proj.factory.blank_state(addr=start_addr)

# 创建待求解bvs
password_size = 64 * 8 # 64bytes
bvs_password = claripy.BVS('password', password_size)

# 符号化文件
sim_file = angr.SimFile('1.txt', bvs_password, size=password_size//8)# size in bytes there
# sim_file = angr.storage.SimFile('1.txt', content=bvs_password, size=64)

# 与state关联
init_state.fs.insert('OJKSQYDP.txt', sim_file)

# 模拟执行
simgr = proj.factory.simgr(init_state)
find_addr = 0x080489B0
simgr.explore(find=find_addr)

if simgr.found:
    solve_state = simgr.found[0]
    password = solve_state.solver.eval(bvs_password, cast_to=bytes)
    print(f'password = {password}')
else:
    print("no found")

约束条件

08_angr_constraints

比较特殊的地方在于它的check_equals_xxxx()函数，里面使用 for 循环逐字节比较。对于模拟来说，每次循环中的比较有两种可能的结果：相等和不相等，字符串16字节，因此模拟执行的路径最多有$2^{16}=65536$条，这就会导致路径爆炸的问题。

因此我们需要通过state.solver.add()或者state.add_constraints()手动添加约束条件，以替换check_equals_xxxx()函数功能，从而避免逐字节比较造成的路径爆炸问题。

具体操作为：

  1. 选择 scanf 之后的状态作为 angr 执行的初始状态。
  2. 符号化待求解的 buffer，模拟执行到check_equals_xxxx()函数处。
  3. 对求解出的state添加约束条件，以等价替换check_equals_xxxx()函数所执行的功能，然后约束求解出具体值。

当然这里也可以通过 angr 的 hook 操作来改写check_equals_xxxx()函数（见题09）。

Constraints

位向量之间可以进行比较运算 ，其结果为 Bool 类型的对象：

1
2
3
4
5
6
7
8
9
10
>>> bvv = claripy.BVV(0xdeadbeef, 32)
>>> bvv2 = claripy.BVV(0xdeadbeef, 32)
>>> bvv == bvv2
<Bool True>
>>> bvs = claripy.BVS('bvs', 32)
>>> bvs == bvv + bvv2
<Bool bvs_0_32 == 0xbd5b7dde>
>>> bvs2 = claripy.BVS('bvs2', 32)
>>> bvs2 > bvs * bvv + bvv2
<Bool bvs2_1_32 > bvs_0_32 * 0xdeadbeef + 0xdeadbeef>

对于带有符号值的比较而言， Bool 类型的对象直接表示了对应的式子，因此可以作为约束条件被添加到一个状态当中，我们可以通过 state.solver.add() 为对应状态添加约束：

1
2
3
>>> state.solver.add(bvs == bvv + bvv2)
>>> state.solver.add(bvs2 > bvs * bvv + bvv2)
>>> state.solver.eval(bvs2) # get the concrete value under constraints

除了 Bool 类以外，Claripy 还提供了一些以位向量作为结果的运算操作，以下是一个例子（完整的还是去读文档吧）：

1
2
>>> claripy.If(bvs == bvs2, bvs, bvs2)
<BV32 if bvs_0_32 == bvs2_1_32 then bvs_0_32 else bvs2_1_32>

exp

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
import angr
import claripy

proj = angr.Project('./08_angr_constraints')

# 在scanf之后创建空白state
start_addr = 0x08048625
init_state = proj.factory.blank_state(addr=start_addr)

buffer_addr = 0x0804A050
buffer_size = 16 * 8
bvs_buffer = claripy.BVS('buffer', buffer_size)
init_state.memory.store(buffer_addr, bvs_buffer)

# angr模拟执行, 执行到check_equals_xxx之前
check_addr = 0x08048669
simgr = proj.factory.simgr(init_state)
simgr.explore(find=check_addr)

# 约束条件
compare_str = b'AUPDNNPROEZRJWKB'
if simgr.found:
    for i in simgr.found:
        check_state = i
        password = check_state.memory.load(buffer_addr, buffer_size//8)
        check_state.add_constraints(compare_str == password)
        # 或
        # check_state.solver.add(compare_str == password)

        print(f'password = {check_state.solver.eval(bvs_buffer,cast_to=bytes)}')

函数操作

09_angr_hooks

第一个输入进行complex_function函数操作后，调用check_equals_xxxx()函数进行字符串比较，该函数内部是逐字节比较，与题08类似，需注意其函数返回值通过寄存器eax传递。第二个输入与进行complex_function函数后的password进行比较。只有这两个比较都相等时才输出Good Job。

初次想到的想法是将输入分成两部分进行模拟执行，因为这两次输入没有关联性。第一次模拟执行求解第一次的输入，代码与题08的解题代码相似，模拟范围是第10~13行。第二次模拟执行求解第二次的输入，模拟范围是第14~17行。

以上做法稍微复杂，比较简单的做法如题目所示，使用hook操作替换check_equals_xxxx()函数，以防止路径爆炸问题。

Function hook

在 angr 中，我们可以使用：

1
project.hook(addr = call_insn_addr, hook = my_function, length = n)`

来 hook 掉对应的 call 指令，其函数的参数说明如下：

  • call_insn_addr：被 hook 的 call 指令的地址
  • my_function ：我们的自定义 python 函数
  • length： call 指令的长度

这种hook有局限性，它本质上是替换call函数的跳转地址，倘若所要替换的某一函数在程序中有多个call，那么使用该方法则需要挨个hook 这些调用该函数的call指令。因此angr提供了project.hook_symbol()函数，能够根据函数名通过符号表hook对应函数（符号表可以得到函数的地址）。

我们的自定义函数应当为接收 state 作为参数的函数，angr 还提供了 decorator 语法糖，因此以下两种写法都可以：

1
2
3
4
5
6
7
8
9
10
11
# method 1
@project.hook(0x1234, length=5)
def my_hook_func(state):
    # do something, this is an example
    state.regs.eax = 0xdeadbeef

# method 2
def my_hook_func2(state):
    # do something, this is an example
    state.regs.eax = 0xdeadbeef
proj.hook(addr = 0x5678, hook = my_hook_func2, length = 5)

exp

因此本题我们可以通过hook操作替换check_equals_xxxx()函数，自定义函数中则需要加载buffer，并使用 claripy.If() 创建一个buffer与password的比较，并将值给到 eax 寄存器作为返回值。其余操作类似。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
import angr, claripy, sys

buffer_addr = 0x0804A054
buffer_bytes = 16
hook_call_addr = 0x080486B3
call_size = 0x080486B8 - hook_call_addr
find_addr = 0x08048768
compare_str = b'XYMKBKUHNIQYNQXE'

def hook_check_equal(state):
    buffer_str1 = state.memory.load(buffer_addr, buffer_bytes)
    # 不能用ifelse语句，而应该是claripy.If(expression, ret_if_true, ret_if_false),里面的返回值类型得是BVV
    state.regs.eax = claripy.If(
        buffer_str1 == compare_str,
        claripy.BVV(1, 32),
        claripy.BVV(0, 32)
    )

proj = angr.Project('./09_angr_hooks')

init_state = proj.factory.entry_state()

# hook check_equal函数
proj.hook(addr=hook_call_addr, hook=hook_check_equal, length=call_size)

# angr模拟执行, 执行到输出Good Job
simgr = proj.factory.simgr(init_state)
simgr.explore(find=find_addr)

if simgr.found:
    solve_state = simgr.found[0]
    password = solve_state.posix.dumps(sys.stdin.fileno()).decode()
    print(f'password = {password}')
else:
    print('no found')

10_angr_simprocedures

main函数的CFG很大，但是IDA反汇编仅出了一点伪代码，看来得看汇编代码。整个程序首先是将”ORSDDWXHZURJRBDH”存入password中，然后要求我们输入16字节的字符串，之后就是很多跳转，几乎每个分支都调用了check_equals_xx函数，这些分支最后中都会进入同一地方，进行”Try again”和”Good Job”的判断。

我们的做法显然还是要使用hook来替换这些check_equals_xx函数，但是它们对应的call指令很多，使用project.hook()挨个替换每个call指令的跳转地址那就非常复杂了。但是，angr提供了project.hook_symbol()函数，可以直接通过函数名hook这些函数。

Simulated Procedure

在 angr 中 angr.SimProcedure 类用来表示在一个状态上的一个运行过程——即函数实际上是一个 SimPrecedure。

我们可以通过创建一个继承自 angr.SimProcedure 的类并重写 run() 方法的方式来表示一个自定义函数，其中 run() 方法的参数为被hook函数的参数。自定义函数主要用于对文件中的原有函数进行替换，例如 angr 会用内置的一些 SimProcedure 来替换掉一些库函数（见题13），以加快模拟执行的速度。。

若我们已经有该二进制文件的符号表，我们可以直接使用 project.hook_symbol(symbol_str, sim_procedure_instance) 来自动 hook 掉文件中所有的对应符号，示例如下：

1
2
3
4
5
6
7
8
9
10
import angr
import claripy

class MyProcedure(angr.SimProcedure):
    def run(self, arg1, arg2):
        # do something, this's an example
        return self.state.memory.load(arg1, arg2)

proj = angr.Project('./test')
proj.hook_symbol('func_to_hook', MyProcedure())

当然，在 SimProcedure 的 run() 过程中我们也可以使用SimProcedure类的一些成员函数：

  • ret(expr): 函数返回。
  • jump(addr): 跳转到指定地址。
  • exit(code): 终止程序。
  • call(addr, args, continue_at): 调用文件中的函数。
  • inline_call(procedure, *args): 内联地调用另一个 SimProcedure。

exp

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
import sys
import angr
import claripy

proj = angr.Project('./10_angr_simprocedures')
init_state = proj.factory.entry_state()

compared_str = 'ORSDDWXHZURJRBDH'
# 自定义用于等价替换 check_equal_xxx 函数的SimProcedure
class MyProcedure(angr.SimProcedure):
    def run(self, buffer_addr, length):
        buffer = self.state.memory.load(buffer_addr, length)
        return claripy.If(buffer == compared_str, claripy.BVV(1, 32), claripy.BVV(0, 32))

#  hook by symbol
proj.hook_symbol('check_equals_ORSDDWXHZURJRBDH', MyProcedure())

# 模拟执行
simgr = proj.factory.simgr(init_state)
simgr.explore(find=0x0804A981, avoid=0x0804A96F)

if simgr.found:
    solve_state = simgr.found[0]
    password = solve_state.posix.dumps(sys.stdin.fileno()).decode()
    print(f'password = {password}')
else:
    print('no found')

11_angr_sim_scanf

IDA反编译超时，直接看汇编代码。main函数一开头有很多伪分支（如果仔细看的话），这些伪分支后面都存在scanf函数，要求我们输入两个无符号整数，这两个字符串要等于另外两个值。

这题使用题02的脚本也可以快速求解出来，但我们根据题目的意思，实现一个SimProcedure 来模拟scanf的执行过程并hook掉scanf函数。脚本如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
import sys
import angr
import claripy

class MyProcedure(angr.SimProcedure):
    def run(self, str_format, buffer0_addr, buffer1_addr):
        bvs_buffer0 = claripy.BVS('buffer0', 4 * 8)
        bvs_buffer1 = claripy.BVS('buffer1', 4 * 8)

        self.state.memory.store(buffer0_addr, bvs_buffer0, endness=proj.arch.memory_endness)
        self.state.memory.store(buffer1_addr, bvs_buffer1, endness=proj.arch.memory_endness)

        # 仅仅只是方便后面提取buffer0、buffer1的值
        # self.state.globals['buffer'] = (bvs_buffer0, bvs_buffer1)

proj = angr.Project('./11_angr_sim_scanf')
init_state = proj.factory.entry_state()

#  hook by symbol
proj.hook_symbol('__isoc99_scanf', MyProcedure())

# 模拟执行
simgr = proj.factory.simgr(init_state)
simgr.explore(find=0x0804FC9E, avoid=0x0804FC8C)

if simgr.found:
    solve_state = simgr.found[0]

    # 需要确定大小端，否则输出有误！！！
    buffer0 = solve_state.solver.eval(solve_state.memory.load(0x0805D898, 4, endness=proj.arch.memory_endness))# bytes in there
    buffer1 = solve_state.solver.eval(solve_state.memory.load(0x0806185C, 4, endness=proj.arch.memory_endness))

    # buffer = solve_state.globals['buffer']
    # buffer0 = solve_state.solver.eval(buffer[0]) # 这里不用endness是因为run中存储时制定了该符号变量的存储时的大小端模式
    # buffer1 = solve_state.solver.eval(buffer[1])

    print(f'password = {buffer0}, {buffer1}')
else:
    print('no found')

路径合并

12_angr_veritesting

拖入IDA中分析，发现又是逐字节比较字符串，但不同的地方在于，这个比较功能不在单独的一个函数中，所以不方便使用hook，然而angr 提供 Veritesting的技术来合并路径，以缓解路径爆炸问题。

Veritesting

动态符号执行（DSE）基于路径的方式来生成公式，每条路径生成一个公式，公式易于求解，但生成公式的开销较大。

静态符号执行（SSE）基于语句的方式来生成公式，公式覆盖多条路径，开销较小，公式较为简洁，但求解难度较大。

Veritesting结合了静态符合执行与动态符号执行的优势，缓解了路径爆炸问题。其基本思想是将符号执行应用于程序的某些关键部分，而静态分析用于处理其他部分，从而减轻路径爆炸问题，同时减少误报率。

Veritesting原理参考论文：[Enhancing Symbolic Execution with Veritesting.pdf](https://users.ece.cmu.edu/~dbrumley/pdf/Avgerinos et al._2014_Enhancing Symbolic Execution with Veritesting.pdf)

exp

具体操作是在创建simgr时指定veritesting=True，这样 angr 便会在运行过程中自动进行路径合并，从而缓解路径爆炸的问题。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
import sys
import angr

proj = angr.Project('./12_angr_veritesting')
init_state = proj.factory.entry_state()

# 开启路径合并，减少路径爆炸
simgr = proj.factory.simgr(init_state, veritesting=True)
simgr.explore(find=0x08048684, avoid=0x08048696)

if simgr.found:
    solve_state = simgr.found[0]
    password = solve_state.posix.dumps(sys.stdin.fileno()).decode()
    print(f'password = {password}')
else:
    print('no found')

库操作

13_angr_static_binary

拖入IDA中分析，感觉和题00一样，但是模拟执行的时间很长🧐，这是为什么？后来看了官方题解才知道这个程序是静态编译生成的，以往的程序是动态编译生成的。

那这有什么区别呢？我们需要先了解一下动态编译和静态编译的区别。

动态编译和静态编译

动态编译是将应用程序需要的模块都编译成动态链接库，启动程序（初始化）时，这些模块不会被加载，运行时用到哪个模块就调用哪个。

静态编译就是在编译时，把所有模块都编译进可执行文件里，因而文件体积也就更大，当启动这个可执行文件时，所有模块都会被加载进来。

angr加速静态编译的程序的模拟执行

事实已经呈现：静态编译的程序进行模拟执行的时间会变得很长。那angr如何处理这一问题呢？

angr内部实现了一些用于替换标准库函数的simprocedure，这些函数的工作速度更快。通常情况下，angr 会自动地用工作速度快得多的 simprocedure 代替标准库函数，但是这题中库函数都已经因为静态编译成了静态函数了，angr 没法自动替换。要解决这题，需要手动 hook 所有使用标准库的C函数。获取 angr 内置库函数的方式是 angr.SIM_PROCEDURES[lib_name][function_name] ，以下是一些常用的库函数SimProcedures：

1
2
3
4
5
6
7
8
9
10
11
12
angr.SIM_PROCEDURES['libc']['malloc']
angr.SIM_PROCEDURES['libc']['fopen']
angr.SIM_PROCEDURES['libc']['fclose']
angr.SIM_PROCEDURES['libc']['fwrite']
angr.SIM_PROCEDURES['libc']['getchar']
angr.SIM_PROCEDURES['libc']['strncmp']
angr.SIM_PROCEDURES['libc']['strcmp']
angr.SIM_PROCEDURES['libc']['scanf']
angr.SIM_PROCEDURES['libc']['printf']
angr.SIM_PROCEDURES['libc']['puts']
angr.SIM_PROCEDURES['libc']['exit']
angr.SIM_PROCEDURES['glibc']['__libc_start_main']

使用例子如下：

1
2
3
proj.hook(0x0804ED40, angr.SIM_PROCEDURES['libc']['printf']())
# 或
proj.hook_symbol("printf", angr.SIM_PROCEDURES['libc']['printf']())

exp

由于 main 函数并不是程序开始执行时运行的第一个函数，而是 _start 函数，里面会调用__libc_start_main()函数进行初始化，包括设置程序的环境、处理命令行参数、注册析构函数等，最后调用用户定义的 main 函数。

这个初始化的过程对于 angr 非常耗时，因此我们需要从 main 函数处创建blank_state，或者 hook 掉 __libc_start_main() ，从而使用 entry_state 也是可以的。

除此之外，我们还需要 hook 掉 printf、scanf、strcmp、puts 这些库函数。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
import sys, angr

proj = angr.Project('./13_angr_static_binary')
#init_state = proj.factory.entry_state()
init_state = proj.factory.blank_state(addr=0x080488FE)# main入口

# hook ，不同于之前，地址不是调用处的，而是这些函数地址！
proj.hook(0x0804ED40, angr.SIM_PROCEDURES['libc']['printf']())
proj.hook(0x0804ED80, angr.SIM_PROCEDURES['libc']['scanf']())
proj.hook(0x0805B450, angr.SIM_PROCEDURES['libc']['strcmp']())
proj.hook(0x0804F350, angr.SIM_PROCEDURES['libc']['puts']())
# proj.hook(0x08048D10, angr.SIM_PROCEDURES['glibc']['__libc_start_main']()) # 可以不用，因为定义的初始状态为main入口
# 或
# 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']())

simgr = proj.factory.simgr(init_state)
simgr.explore(find=0x080489E1, avoid=0x080489CF)

if simgr.found:
    solve_state = simgr.found[0]
    password = solve_state.posix.dumps(sys.stdin.fileno()).decode()
    print(f'password = {password}')
else:
    print('no found')

14_angr_shared_library

使用到的关键函数validate是一个外部导入函数（extrn标识），它的具体定义在同目录下的so文件中。

需要注意的是，动态链接库是不能单独运行的，我们需要模拟validate函数调用，通过以下代码可以创建一个函数调用的初始状态。

1
project.factory.call_state(function_addr, paramter_1, paramter_1)

此外我们还需要指定动态链接库的基址，并且后续引用库中的变量或函数等时，它们的地址都是基址 + 偏移量。

请注意，在linux下执行本题程序时，需要将动态库放在 /lib 和 /usr/lib 这两个目录下的库文件，或者把动态库的所在路径用export指令加入到 ~/.bash_profile 中的LD_LIBRARY_PATH变量中。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
import angr
import claripy

# 基址
base = 0x400000
proj = angr.Project('./lib14_angr_shared_library.so',
                    load_options={
                            'main_opts': {
                              'base_addr': base
                              }
                            }
                    )

# 创建调用validate函数所需的两个参数
password_pointer = claripy.BVV(0x121244, 4 * 8)
password_length = claripy.BVV(8, 4 * 8)

# 创建一个函数调用的初始状态
validate_function_addr = base + 0x000006D7
init_state = proj.factory.call_state(validate_function_addr, password_pointer, password_length)

# 将待求解的bvs放入对应的参数中
password_bvs = claripy.BVS('password', 8 * 8)
init_state.memory.store(password_pointer, password_bvs)

# 设置最终状态为strcmp(s1, s2) == 0之后
simgr = proj.factory.simgr(init_state)
simgr.explore(find=base + 0x0000077D)

if simgr.found:
    check_state = simgr.found[0]
    check_state.add_constraints(check_state.regs.eax == 1)
    password = check_state.solver.eval(password_bvs, cast_to=bytes)
    print(f'password = {password}')
else:
    print('no found')

漏洞利用

15_angr_arbitrary_read

要求我们输入一个数字以及20字节的字符串，如果key=2358019，就输出s指向的字符串（其实就是“Try again”），否则仍然输出“Try again”！？

看了下提示，这道题是想让我们输出”Good Job”字符串。注意到v4只有16字节大小，而它要接收20字节，所以会覆盖s指针。因此我们可以通过这个漏洞，将s指向”Good Job”字符串所在地址。

为了求解怎样的输入能触发这一漏洞，我们需要 hook 掉 scanf 函数，将输入符号化。同时还需要一个验证函数来检测输入是否触发漏洞，选择的检测点就是puts函数的PLT地址，因为无论输出“Try again”还是”Good Job”都会调用这个函数。具体的检测操作是：取出puts函数的传入参数，判断这个puts函数是否是通过puts(s)调用的（可通过判断参数是否符号化），然后再判断该参数的值是否是puts函数的PLT地址。更为详细的解析见代码中。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
import angr
import claripy

proj = angr.Project('./15_angr_arbitrary_read')

# hook scanf函数，重写内部实现
class ReplacementScanf(angr.SimProcedure):
    def run(self, format, key_addr, string_addr):
        # scanf的两个参数
        key_bvs = claripy.BVS('key', 4 * 8)
        string_bvs = claripy.BVS('string', 20 * 8)

        # 限制字符串的字符为可打印字符，方便我们执行程序时的手动输入
        for alp in string_bvs.chop(bits=8):
            self.state.add_constraints(alp >= '0', alp <= 'z')

        self.state.memory.store(key_addr, key_bvs, endness=proj.arch.memory_endness)
        self.state.memory.store(string_addr, string_bvs)

        # 设置成全局
        self.state.globals['key'] = key_bvs
        self.state.globals['string'] = string_bvs

proj.hook_symbol('__isoc99_scanf', ReplacementScanf())

# 当puts函数被调用，检查其传入的参数是否是我们的bvs
def check_puts(state):
    # 根据当前堆栈可知，esp+4指向传入的参数，esp指向返回地址
    puts_param = state.memory.load(state.regs.esp + 4, 4, endness=proj.arch.memory_endness)
    # 如果是put函数的传参是符号化的，说明是put(s)
    if state.solver.symbolic(puts_param):
        good_job_string_address = 0x4F534957
        # 是否是good job字符串的首地址，是则说明任意写成功
        is_vulnerable_expression = puts_param == good_job_string_address
        # 如果满足额外约束条件，则添加，这样一来就不需要state.copy()一份来判断
        if state.satisfiable(extra_constraints=(is_vulnerable_expression,)):
            # 添加约束条件供state.solver.eval求解具体值
            state.add_constraints(is_vulnerable_expression)
            return True
        else:
            return False
    else:
        return False

# explore find成功的依据
def is_successful(state):
    puts_addr = 0x08048370
    if state.addr == puts_addr:
        return check_puts(state)
    else:
        return False

init_state = proj.factory.entry_state()
simgr = proj.factory.simgr(init_state)
simgr.explore(find=is_successful)

if simgr.found:
    solution_state = simgr.found[0]
    key = solution_state.solver.eval(solution_state.globals['key'])
    s = solution_state.solver.eval(solution_state.globals['string'], cast_to=bytes).decode()
    print(f'key = {key}, string = {s}')
else:
    print('no found')

16_angr_arbitrary_write

跟题15相似。思路很简单，我们需要通过s覆盖dest指针，使其指向password_buffer，同时确保s的前8字节为“DVTBOGZL”。

对于angr代码实现，具体为：hook掉scanf函数，使输入符号化，然后检测点是strncpy函数，如果其两个指针参数是符号化的，则说明通过strncpy(dest, s, 0x10u)调用的，这是成功的第一步。最后检查地址参数dest是否指向password_buffer，以及参数s的前8字节是否是“DVTBOGZL”。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
import angr
import claripy

proj = angr.Project('./16_angr_arbitrary_write')

class ReplacementScanf(angr.SimProcedure):
    def run(self, format, key_addr, s_addr):
        # 创建scanf的两个参数bvs
        key_bvs = claripy.BVS('key', 4 * 8)
        s_bvs = claripy.BVS('s', 20 * 8)
        # 约束字符串为可打印字符，方便程序运行时输入
        for alp in s_bvs.chop(bits=8):
            self.state.add_constraints(alp >= '0', alp <= 'z')

        # bvs保存到内存中,数字需注意大小端
        self.state.memory.store(key_addr, key_bvs, endness=proj.arch.memory_endness)
        self.state.memory.store(s_addr, s_bvs)

        # 全局化，方便读取
        self.state.globals['key'] = key_bvs
        self.state.globals['s'] = s_bvs

proj.hook_symbol('__isoc99_scanf', ReplacementScanf())

def check_strncpy(state):

    dest_param = state.memory.load(state.regs.esp + 4, 4, endness=proj.arch.memory_endness)# bytes in there
    s_param = state.memory.load(state.regs.esp + 8, 4, endness=proj.arch.memory_endness)

    front_str = state.memory.load(s_param, 8)# bytes in there
    if state.solver.symbolic(dest_param) and state.solver.symbolic(front_str):
        password_buffer_addr = 0x4655544C
        should_str = b'DVTBOGZL'
        constraint1 = dest_param == password_buffer_addr
        constraint2 = front_str == should_str

        if state.satisfiable(extra_constraints=(constraint1, constraint2)):
            state.add_constraints(constraint1, constraint2)
            return True
        else:
            return False
    else:
        return False



def is_successful(state):
    strncpy_addr = 0x08048410
    if state.addr == strncpy_addr:
        return check_strncpy(state)
    else:
        return False

init_state = proj.factory.entry_state()
simgr = proj.factory.simgr(init_state)
simgr.explore(find=is_successful)

if simgr.found:
    solution_state = simgr.found[0]
    key = solution_state.solver.eval(solution_state.globals['key'])
    s = solution_state.solver.eval(solution_state.globals['s'], cast_to=bytes)
    print(f'key = {key}, s = {s}')
else:
    print('no found')

17_angr_arbitrary_jump

read_input函数中有一个不限字节的字符串输入，这是解题的关键。然后我通过搜索”Good Job“字符串，找到了如下图所示函数。

这么一看，就明白了。它想让我们通过不限长度的输入来覆盖调用read_input后的返回地址，使其指向print_good函数，从而能够输出“Good Job”字符串。画个堆栈图再让我们更明白点。

此时堆栈调用图中，[ebp + 4]是返回地址，ebp - 30是 v1 的首地址，因此我们需要输入38字节的字符串才能够覆盖返回地址，从而利用栈溢出来控制程序进行跳转。

然而对于 angr 而言这样的状态是不受约束的状态（unconstrained state），会被自动丢弃，因此我们还需要想办法让 angr 保留这样的状态。

statsh

在 angr 当中，不同的状态被组织到 simulation manager 的不同的 stash 当中，我们可以按照自己的需求进行步进、过滤、合并、移动等。

stash 类型

在 angr 当中一共有以下几种 stash：

  • simgr.active：活跃的状态列表。在未指定替代的情况下会被模拟器默认执行。
  • simgr.deadended：死亡的状态列表。当一个状态无法再被继续执行时（例如没有有效指令、无效的指令指针、不满足其所有的后继（successors））便会被归入该列表。
  • simgr.pruned：被剪枝的状态列表。在指定了 LAZY_SOLVES 时，状态仅在必要时检查可满足性，当一个状态在指定了 LAZY_SOLVES 时被发现是不可满足的（unsat），状态层（state hierarchy）将会被遍历以确认在其历史中最初变为不满足的时间，该点及其所有后代都会被剪枝（pruned）并放入该列表。
  • simgr.unconstrained：不受约束的状态列表。当创建 SimulationManager 时指定了 save_unconstrained=True，则被认为不受约束的（unconstrained，即指令指针被用户数据或其他来源的符号化数据控制）状态会被归入该列表。
  • simgr.unsat：不可满足的状态列表。当创建 SimulationManager 时指定了 save_unsat=True，则被认为无法被满足的（unsatisfiable，即存在约束冲突的状态，例如在同一时刻要求输入既是"AAAA" 又是 "BBBB"）状态会被归入该列表。

还有一种不是 stash 的状态列表——errored，若在执行中产生了错误，则状态与其产生的错误会被包裹在一个 ErrorRecord 实例中（可通过 record.state 与 record.error 访问），该 record 会被插入到 errored 中，我们可以通过 record.debug() 启动一个调试窗口。

stash 操作

我们可以使用 stash.move() 来在 stash 之间转移放置状态，用法如下：

1
>>> simgr.move(from_stash = 'unconstrained', to_stash = 'active')

在转移当中我们还可以通过指定 filter_func 参数来进行过滤：

1
2
3
4
>>> def filter_func(state):
...     return b'arttnba3' in state.posix.dumps(1)
...
>>> simgr.move(from_stash = 'unconstrained', to_stash = 'active', filter_func = filter_func)

stash 本质上就是个 list，因此在初始化时我们可以通过字典的方式指定每个 stash 的初始内容：

1
2
3
4
5
>>> simgr = proj.factory.simgr(init_state,
...     stashes = {
...             'active':[init_state],
...             'found':[],
...     })

exp

由于本题我们需要通过栈溢出来控制 eip，属于 unconstrained 状态，因此我们不能像之前一样使用simulation.explore方法，这样就无法模拟执行我们想要的 unconstrained 状态。我们需要使用 simgr.step() 来进行单步执行，每次都手动将处于unconstrained 状态转移到found stash中，当然也可以添加过滤函数来过滤指定的unconstrained 状态。最后约束eip为print_good的地址进行求解。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
import angr
import claripy

proj = angr.Project('./17_angr_arbitrary_jump')

# hook scanf
class ReplacementScanf(angr.SimProcedure):
    def run(self, format, v1_addr):
        # v1自身长度 + 4字节（覆盖地址）
        v1_bvs = claripy.BVS('v1', 38 * 8)
        # 限制v1的输入字符
        for alp in v1_bvs.chop(bits=8):
            self.state.add_constraints(alp >= '0', alp <= 'z')
        # bvs入内存
        self.state.memory.store(v1_addr, v1_bvs)
        # 设全局
        self.state.globals['v1'] = v1_bvs

proj.hook_symbol('__isoc99_scanf', ReplacementScanf())

init_state = proj.factory.entry_state()
simgr = proj.factory.simgr(
        init_state,
        save_unconstrained=True,# 保存不受约束的state
        stashes={
          'active': [init_state],# 初始求解时只有一个初始状态，且处于active
          'unconstrained': [],
          'found': [],
          'not_needed': []
        }
    )

# 检测unconstrained_state的eip是否是print_good函数地址，满足则加入found stash中
def filter_unconstrained(state):
    print_good_function_addr = 0x4D4C4749
    return state.satisfiable(extra_constraints=(state.regs.eip == print_good_function_addr,))

# 单步执行 step by step
while not simgr.found:
    if simgr.active or simgr.unconstrained:
        # Look for unconstrained states and move them to the 'found' stash.
        simgr.move(from_stash='unconstrained', to_stash='found', filter_func=filter_unconstrained)
        # simgr.move(from_stash='unconstrained', to_stash='found')
        simgr.step()
    else:
        break


if simgr.found:
    solution_state = simgr.found[0]
    print_good_function_addr = 0x4D4C4749
    # 添加约束条件供solver求解
    solution_state.add_constraints(solution_state.regs.eip == print_good_function_addr)
    v = solution_state.solver.eval(solution_state.globals['v1'], cast_to=bytes)
    print(f'v1 = {v}')
else:
    print('no found')

参考：

https://docs.angr.io/en/latest/core-concepts/states.html

https://github.com/jakespringer/angr_ctf

https://arttnba3.cn/2022/11/24/ANGR-0X00-ANGR_CTF/

https://ctf-wiki.org/reverse/tools/simulate-execution/angr

https://github.com/ZERO-A-ONE/AngrCTF_FITM/blob/master/

ubuntu 执行ELF 32-bit文件，提示找不到，明明就在当前路径执行的_mx6u运行elf无法找到文件或路径-CSDN博客

Reverse
#angr
angr入门
http://example.com/2024/06/11/工具入门/angr入门/
作者
gla2xy
发布于
2024年6月11日
许可协议