Angr 学习笔记

Angr 学习笔记

安装

安装的话angr支持了Python 3.x可以不用去折腾2.x的版本了，对于Windows似乎可以直接：

1
pip install angr

就可以完成大部分需要库的安装，对于Linux可能会有一些复杂，这里给出一个链接给大家参考一下：

https://www.cnblogs.com/lxy8584099/p/13668749.html

本人是在Windows下安装的，也没遇到网上出现的缺失文件的现象。出现问题了我也不清楚呀 ：(

部分使用教程

导入 angr 包

1
import angr

似乎这一部没有出差错就是说明安装成功了。

新建一个 angr 工程

1
2
# 创建angr项目
p = angr.Project("<需要拿来解题的文件>")

上述过程相当于完成了angr的加载。

初始化 angr

Unicorn是 angr的依赖库，在Unicorn下可以执行任意一段二进制的代码，我们对此需要告诉其从哪里开始，因此我们需要对angr进行初始化

1
2
# 设置项目起点，entry_state代表程序的入口点，即main函数
init_state = p.factory.entry_state()

执行 angr

初始化后我们需要执行angr

1
2
# 设置模拟器
sm = p.factory.simulation_manager(init_state)

上述过程中我们设置了一个模拟器，接下来我们需要告诉程序应该到哪里去，我们需要设置目标地址：

1
sm.explore(find = "<目标地址>")

此时如果我们找到了通向对应的目标地址的时候，将其打印出来其符号向量：

1
2
3
4
5
6
7
# 如果到达目标地址，打印此时的符号向量
if simulation.found:
    solution_state = simulation.found[0]
    print(solution_state.posix.dumps(sys.stdin.fileno()))
# 否则抛出失败异常
else:
    raise Exception('Could not find solution')

00_angr_find

第一题拖进IDA分析可以看到是十分简单的，其关键部分便是中间的那个complex_function，我们尝试用angr来进行解题 ( 虽然爆破也可以直接执行 )。

我们找到对应目标 ( Good Job ) 的地址，将其导入进行求解

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
import angr

def main(argv):
    # 目标文件的路径
    path_to_binary = '../program/00_angr_find'
    # 创建angr项目
    project = angr.Project(path_to_binary)
    
    # 设置项目起点，entry_state代表程序的入口点，即main函数
    initial_state = project.factory.entry_state()
    # 设置模拟器
    simulation = project.factory.simgr(initial_state)
    
    # 设置目标地址
    print_good_addr = 0x0804867D
    simulation.explore(find=print_good_addr)
    
    # 如果到达目标地址，打印此时的符号向量
    if simulation.found:
        solution_state = simulation.found[0]
        print(solution_state.posix.dumps(sys.stdin.fileno()))
    # 否者抛出失败异常
    else:
        raise Exception('Could not find solution')
    
if __name__ == '__main__':
    main(sys.argv)

值得注意的是在输出语句中print(solution_state.posix.dumps(sys.stdin.fileno()))，其中的dumps在Python 3.x下运行成功，但是在文档中看到有些写的是dump，不清楚其是否为Python 2.x运行的，上述脚本运行不成功时可以试试看各改一下输出的dump

通过上述脚本我们可以直接得到目标地址的值在解密后得到的目标答案。

1
b'FMKGABFY'

本题中我们了解到了如何编写angr脚本，了解了如何创建项目，创建模拟器以及如何约束模拟器到对应的地址处和输出约束求解的结果。

1
2
3
4
5
angr.Project(file_path) #创建项目
project.factory.simgr(initial_state) #创建模拟器
simulation.explore(find=addr) #约束模拟器到达find指定的地址
solution_state = simulation.found[0]
print(solution_state.posix.dumps(sys.stdin.fileno())) #打印符号向量

01_angr_avoid

将程序拖进IDA，反编译主函数程序显示函数过大，无法反编译，在这个题目中我们主要学习angr的avoid的使用，对此我们利用avoid来去除我们不想要到达的地址。

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
import sys
import angr

def main(argv):
    # 目标文件的路径
    path_to_binary = '../program/00_angr_find'
    # 创建angr项目
    project = angr.Project(path_to_binary)
    
    # 设置项目起点，entry_state代表程序的入口点，即main函数
    initial_state = project.factory.entry_state()
    # 设置模拟器
    simulation = project.factory.simgr(initial_state)
    
    # 设置目标地址
    print_good_addr = 0x080485E0
    try_again_addr = 0x080485F2
    
    # simulation.explore(find=print_good_addr)
    
    # 在这里可以添加 avoid 来约束我们到达的目的地址 
    simulation.explore(find=print_good_addr, avoid=try_again_addr)
    # 如果到达目标地址，打印此时的符号向量
    if simulation.found:
        solution_state = simulation.found[0]
        print(solution_state.posix.dumps(sys.stdin.fileno()))
    # 否者抛出失败异常
    else:
        raise Exception('Could not find solution')
    
if __name__ == '__main__':
    main(sys.argv)

需要注意的是对应的good的地址不是这个字符串的地址，而是打印字符串时的汇编代码对应的地址。

通过上述例子，我们学会了如何加入规避的地址来进行进一步的约束求解

1
2
3
print_good_addr = XXXX	# 目的地址
try_again_addr = XXXX	# 规避地址
simulation.explore(find=print_good_addr, avoid=try_again_addr)

01_angr_condition

将程序拖入IDA可以看到主函数还是和上一题一样，函数过大而无法反编译，同时我们观察一下主函数里的数据可以看到有多个Good Job和多个Try again，此时的一个单一的约束并不能很好的起作用，此时用到了angr中的condition来对多个结果进行约束求解。

1
simulation.explore(find=print_good_addr, avoid=try_again_addr)

之前我们的约束条件都是上面的explore中加入find和avoid的函数地址，但是实际上find和avoid对应的参数可以是一个函数，我们将在这个函数里面进行一个条件的约束

1
2
3
4
5
6
7
def good_job(state):
      stdout_output = state.posix.dumps(sys.stdout.fileno())
      return 'Good Job' in str(stdout_output)

def try_again(state): 
      stdout_output = state.posix.dumps(sys.stdout.fileno())
      return 'Try again' in str(stdout_output)

stdout_output = state.posix.dumps(sys.stdout.fileno())用来获取标准输出的字符

我们利用获取的标准输出字符来进行创建函数，而进一步对我们的条件进行约束求解，那么我们传入的便不再是一个单一的地址，可以对输出的字符集合进行集体约束求解，得到我们想要的结果。

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 sys
import angr

# 到达目标地址，打印此时的符号向量
def good_job(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Good Job' in str(stdout_output)

# 否则抛出失败异常
def try_again(state): 
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Try again' in str(stdout_output)

def main(argv):
    path_to_binary = './02_angr_find_condition'
    # 创建angr项目
    project = angr.Project(path_to_binary)
    # 设置项目起点，entry_state代表程序的入口点，即main函数
    initial_state = project.factory.entry_state()
    # 设置模拟器
    simulation = project.factory.simgr(initial_state)
    # 设置目标地址
    simulation.explore(find=good_job, avoid=try_again) 
    if simulation.found:
        solution_state = simulation.found[0]
        print(solution_state.posix.dumps(sys.stdin.fileno()))
    else:
        raise Exception('Could not find solution')
    
if __name__ == '__main__':
    main(sys.argv)

上述例子，我们学会了对输出条件来进行集体约束求解，明白了simulation.explore对应的参数值可以是一个函数，在函数中我们调用标准的输出库，来对输出字符进行约束求解。

1
2
3
4
5
6
# 函数的返回类型为布尔类型 (bool)
def good_job(state):
	return b"XXX" in solution_state.posix.dumps(0) # 0 是输出 1 是输入
def try_again(state):
	return b"XXX" in solution_state.posix.dumps(0)
simulation.explore(find=good_job, avoid=try_again) # 参数值为函数

03_angr_symbolic_registers

打开题目一看，程序要求我们输入的是 3 个数据，通过三个复杂的函数进行运算，当三个数运算处理后的返回值均为 1 时，判断输入正确，反之判断错误。之前有一个学长去问过angr_CTF库的原作者问多个输入angr可以直接处理吗，原作者回答可以直接处理，但是为了学习目的我们不直接按照之前几个题目的方式来约束地址或者输出来进行运算。

我们还是给出之前的代码写法：

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
import sys
import angr

# 到达目标地址，打印此时的符号向量
def good_job(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Good Job' in str(stdout_output)

# 否则抛出失败异常
def try_again(state): 
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return 'Try again' in str(stdout_output)

def main(argv):
    path_to_binary = './03_angr_symbolic_registers'
    # 创建angr项目
    project = angr.Project(path_to_binary)
    # 设置项目起点，entry_state代表程序的入口点，即main函数
    initial_state = project.factory.entry_state()
    # 设置模拟器
    simulation = project.factory.simgr(initial_state)
    # 设置目标地址
    simulation.explore(find=good_job, avoid=try_again) 
    if simulation.found:
        solution_state = simulation.found[0]
        print(solution_state.posix.dumps(sys.stdin.fileno()))
    else:
        raise Exception('Could not find solution')
    
if __name__ == '__main__':
    main(sys.argv)
    # cfcdef7a 968d69bd c66a3c12

在题目名称中我们可以看到符号化寄存器的英文，那么什么是符号化寄存器？

设置状态的寄存器值，符号化寄存器值含义就是将寄存器内存储的值设为自变量，而后类别列方程加入约束条件内

似乎有点类似于z3设置多个未知数然后带入方程组进行约束求解。那么我们要怎么做呢？我们先观察一下程序的输入：

可以看出来我们的 3 个输入数据先后从ecx中转移到了eax、ebx、edx里，同时在后续复杂函数的处理部分中没有改变 3 个寄存器来进行其他处理，对此我们可以直接设置 3 个未知数来代替这三个寄存器，来参与下面函数的运算和执行。

要将寄存器符号化我们需要引入一个新的函数库：import claripy，由于我们不再是从主函数( main )直接执行我们的符号化向量，我们需要重新设置一个起始地址：

1
2
3
# 设置项目开始地址
start_addr = XXX
initial_state = project.factory.blank_state(addr=start_addr)

其中的project.factory.blank_state与之前的project.factory.entry_state不同了，blank_state相当于表示一个空的地址，需要我们把开始地址进行导入。

接下来便是将寄存器进行符号化，我们便利用到了之前引入的claripy库，下面给出示例：

1
2
3
4
5
6
7
# 将寄存器符号化
bit_length = XX  # 设置寄存器的长度 如 32 —> int 
register = claripy.BVS('<符号向量取名>', bit_length)
initial_state.regs.eax = register # 将 eax 寄存器符号化
# initial_state.regs.xxx = register # xxx 处换成其他寄存器名即可
# 设置模拟器
simulation = project.factory.simgr(initial_state)

那么我们想要输出对应找到后的寄存器值又该怎么处理呢？

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
if simulation.found:
   solution_state = simulation.found[0]
# 条件判断
   solution = solution_state.se.eval(register)
# 创建输出格式
   solution = '%x' % (solution)
   print(solution)
else:
   raise Exception('Could not find the solution')
-------------------------------------------------------------
# 如果有多个寄存器时
if simulation.found:
   solution_state = simulation.found[0]
# 条件判断
   solution1 = solution_state.se.eval(register1)
   solution2 = solution_state.se.eval(register2)
# 创建输出格式
   solution = '%x %x' % (solution1,solution2)
   print(solution)
else:
   raise Exception('Could not find the solution')

此时新的脚本可以如下编写：

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
import sys
import angr
import claripy

def main():
    binary_path = '../program/03_angr_symbolic_registers'
    project = angr.Project(binary_path)
	
    # 设置项目开始地址
    start_addr = 0x0804890E
    initial_state = project.factory.blank_state(addr=start_addr)
	
    
   # 将寄存器符号化
    bit_length = 32	# 此处的长度为 bit
    psd0 = claripy.BVS('psd0', bit_length)
    psd1 = claripy.BVS('psd1', bit_length)
    psd2 = claripy.BVS('psd2', bit_length)
	# 将符号化的寄存器对应到相应的寄存器
    initial_state.regs.eax = psd0
    initial_state.regs.ebx = psd1
    initial_state.regs.edx = psd2
	# 设置模拟
    simulation = project.factory.simgr(initial_state)

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

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

    simulation.explore(find=good_job, avoid=fail)
    
    if simulation.found:
        solution_state = simulation.found[0]
        solution0 = solution_state.se.eval(psd0)
        solution1 = solution_state.se.eval(psd1)
        solution2 = solution_state.se.eval(psd2)
		# 创建输出格式
        solution = '%x %x %x' % (solution0, solution1, solution2)
        print(solution)
    else:
        raise Exception('Could not find the solution')
            
if __name__ == '__main__':
    main()

上述过程中我们学习了符号化寄存器，修改对应的输出格式，同时如何更改执行的起始地址：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
# 设置项目开始地址
start_addr = XXX
initial_state = project.factory.blank_state(addr=start_addr)

# 将寄存器符号化
bit_length = XX  # 设置寄存器的长度 如 32 —> int 
register = claripy.BVS('<符号向量取名>', bit_length)
initial_state.regs.eax = register # 将 eax 寄存器符号化
# initial_state.regs.xxx = register # xxx 处换成其他寄存器名即可

# 更改输出格式
if simulation.found:
   solution_state = simulation.found[0]
# 条件判断
   solution = solution_state.se.eval(register)
# solution2 = solution_state.se.eval(register2)
# 创建输出格式
   solution = '%x' % (solution)
#  solution = '%x %x' % (solution,solution2)
   print(solution)
else:
   raise Exception('Could not find the solution')

04_angr_symbolic_stack

程序名字是符号化栈，对于这个题目我尝试了一下使用之前的02_angr_find_condition来进行约束输出求解，发现angr同样可以直接处理栈，岂不是直接一个输出条件的约束就可以吃遍逆向了？因为有些程序的分支结构十分大，angr会遍历所有可能的分支结构，简单的约束限制求解消耗的时间会十分巨大，所以我们需要进一步的学习来进行约束求解。

在程序里我们的输入是处于栈上的，在scanf过后执行了一个add esp, 10h的操作来清理scanf所产生的栈，因此我们真正的执行部分应该是在add esp, 10h之后，我们观察一下输入，可以看到v2最先被输入，然后便是v1，因此v2所在的栈空间是位于v1下方的 ( 栈向上增长 )。我们每次初始化栈时并不会有数据，而v1处于栈空间的中间，因此我们需要一个padding来帮我们覆写到对应v1所在的空间内。示意图如下：

v1距离栈顶还有0x8的空间，我们初始化栈时的padding将上面的0x8字节空间进行填充，之后的栈空间地址便是我们输入的v1地址。那么怎么进行初始化栈呢？栈开始时我们是将EBP和ESP两个栈指针的地址相等，然后入栈时栈顶指针ESP增加，我们在这个过程中是对栈进行了模拟操作，那么在angr中也有相应的模拟方式来实现模拟栈的初始化。

1
2
3
4
5
6
7
8
9
10
11
initial_state.regs.ebp = initial_state.regs.esp # 初始化栈，令ebp等于esp

password0 = claripy.BVS('password0', 32) # 初始化两个位向量
password1 = claripy.BVS('password1', 32)

padding_length_in_bytes = 0x8 # 填充栈数据 0x8 之后栈空间会在 v1 处
initial_state.regs.esp -= padding_length_in_bytes 

initial_state.stack_push(password0) # 将位向量压入栈中
initial_state.stack_push(password1)

那么我们便可以把这一连串代码加入到之前的第二题的代码之中，编写出如下脚本：

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
from mimetypes import init
import sys
import angr
import claripy


def main():
    binary_path = './04_angr_symbolic_stack'
    project = angr.Project(binary_path)
	# 设置开始地址
    start_addr = 0x08048697
    initial_state = project.factory.blank_state(addr=start_addr)

    initial_state.regs.ebp = initial_state.regs.esp # 初始化栈，令ebp等于esp

    password0 = claripy.BVS('password0', 32) # 初始化两个位向量
    password1 = claripy.BVS('password1', 32)

    padding_length_in_bytes = 0x8 # 填充栈
    initial_state.regs.esp -= padding_length_in_bytes # 从栈顶减去对应的 padding 使栈空间到 v1 处
	# 将位向量压入栈中
    initial_state.stack_push(password0) # v1
    initial_state.stack_push(password1) # v2

    simulation = project.factory.simgr(initial_state)

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

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

    simulation.explore(find=is_successful, avoid=should_abort)

    if simulation.found:
        solution_state = simulation.found[0]

        solution0 = solution_state.se.eval(password0)
        solution1 = solution_state.se.eval(password1)

        solution = '%u %u' % (solution0, solution1)
        print(solution)
    else:
        raise Exception('could not find the solution')

if __name__ == '__main__':
    main()

在这个题目中我们学会了如何符号化栈空间，我们通过填充部分padding使我们的输入数据处于栈顶 ( 绕过了输入 )，同时与符号化寄存器相结合，让angr进行模拟，来代替输入的输入。

1
2
3
4
5
6
7
8
9
10
initial_state.regs.ebp = initial_state.regs.esp # 初始化栈，令ebp等于esp

password0 = claripy.BVS('password0', 32) # 初始化向量
password1 = claripy.BVS('password1', 32)

padding_length_in_bytes = XXX # 填充栈数据 0x8 之后栈空间会在 v1 处
initial_state.regs.esp -= padding_length_in_bytes # 从栈顶减去 padding 的数据大小

initial_state.stack_push(password0) # 将位向量压入栈中
initial_state.stack_push(password1)

05_angr_symbolic_memory

看到题目便是我们要学习的符号化内存空间，观察一下输入的数据所在的位置，可以看到其处于在bss段上，属于一个内存区域内，我们所需要做的便是符号化内存空间。

与符号化栈空间有一点类似，我们需要设置 4 个符号向量来进行模拟输入，然后想办法将其放在内存空间里，angr提供有对应把符号项量放在内存中的函数，我们可以直接通过调用来对内存空间进行符号化。但在这之前我们需要找到bss段每个输入数据所在的地址值，将对应的地址传入到栈空间里。

1
2
# 对应参数值为符号化的地址，和符号化的参数名
initial_state.memory.store(password_addr, password)

其余部分和前面一个题的符号化栈空间是十分相像的，需要我们对输入进行符号化处理，然后将其地址和参数名传入到内存段即可。

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
import angr
import sys
import claripy
from Crypto.Util.number import long_to_bytes

def main():
    binary_path = '../program/05_angr_symbolic_memory'
    project = angr.Project(binary_path)

    start_addr = 0x08048601
    initial_state = project.factory.blank_state(addr=start_addr)

    password0 = claripy.BVS('password0', 64) # 64 = 8(8个字符) * 1(每个字符一字节) * 8(每个字节8比特)
    password1 = claripy.BVS('password1', 64)
    password2 = claripy.BVS('password2', 64)
    password3 = claripy.BVS('password3', 64)

    password0_addr = 0x09FD92A0
    password1_addr = 0x09FD92A8
    password2_addr = 0x09FD92B0
    password3_addr = 0x09FD92B8

    initial_state.memory.store(password0_addr, password0) # 将位向量存入内存
    initial_state.memory.store(password1_addr, password1)
    initial_state.memory.store(password2_addr, password2)
    initial_state.memory.store(password3_addr, password3)

    simulation = project.factory.simgr(initial_state)

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

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

    simulation.explore(find=is_successful, avoid=should_abort)

    if simulation.found:
        solution_state = simulation.found[0]

        solution0 = solution_state.se.eval(password0)
        solution1 = solution_state.se.eval(password1)
        solution2 = solution_state.se.eval(password2)
        solution3 = solution_state.se.eval(password3)
        solution = long_to_bytes(solution0)+b' '+long_to_bytes(solution1)+b' '+long_to_bytes(solution2)+b' '+long_to_bytes(solution3)
        print(solution.decode())
    else:
        raise Exception('Could not find solution')

if __name__ == '__main__':
    main()

不过需要注意的是符号化向量对应的大小应该是对应的bit数据大小，而不是看其字节长度。在这个过程中我们将内存进行了符号化处理，然后将我们的符号化向量传入到bss段中去。

1
2
3
password = claripy.BVS('password', <bit数据大小>) 
password_addr = XXX
initial_state.memory.store(password_addr, password) # 将位向量存入内存

06_angr_symbolic_dynamic_memory

在这个题目中与上一个题目不同的是题目动态分配了两个指针变量，将我们的输入保存在堆空间上，使得我们需要将堆上的空间进行符号化处理，也就是malloc分配的空间是动态的但是其返回的变量buufer位于bss段，是静态的，那么我们可以伪造指针，使其指向的是一片可写内存，进而符号化处理。

6.png

我们可以看到空间内的定义数据都是处于bss段上的，我们便对其想办法来符号化。

相当于我们模拟malloc分配地址空间，在bss段里找到一块空的空间来保存我们的输入数据。与此同时我们观察程序入口点可以看到程序在输入后有add esp, 16对scanf的栈空间进行整理，所以我们程序开始的地址为下面一行的0x08048699

8.png

接下来我们开始模拟malloc分配地址，并将其保存的输入符号化：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
# 符号化输入
password0 = claripy.BVS('password0', 64) # 64 = 8(8个字符) * 1(每个字符一字节) * 8(每个字节8比特)
password1 = claripy.BVS('password1', 64)

# 对应空白 bss 段内空间
fake0_addr = 0x09FD9160 # 伪造malloc得来的内存
fake1_addr = 0x09FD9180

# 指向伪造内存的指针
buffer0_addr = 0x09FD92AC # 输入的存放地址 buffer0
buffer1_addr = 0x09FD92B4 # buffer1

# 将指针指向伪造的内存
# 参数为输入数据存放地址,bss 段伪造的空间
initial_state.memory.store(buffer0_addr, fake0_addr, endness=project.arch.memory_endness) 
initial_state.memory.store(buffer1_addr, fake1_addr, endness=project.arch.memory_endness)

# 将伪造的内存符号化
initial_state.memory.store(fake0_addr, password0) # bss 段伪造的地址,符号化的输入
initial_state.memory.store(fake1_addr, password1)

我们整理一下脚本将符号化动态的内存空间加入到我们的第二题的代码组合便是我们的脚本：

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
from operator import is_
import sys
import angr
import claripy
from Crypto.Util.number import long_to_bytes

def main():
    binary_path = '../program/06_angr_symbolic_dynamic_memory'
    project = angr.Project(binary_path)

    start_addr = 0x08048699
    initial_state = project.factory.blank_state(addr=start_addr)

    password0 = claripy.BVS('password0', 64)
    password1 = claripy.BVS('password1', 64)
    fake0_addr = 0x09FD9160 # 伪造malloc得来的内存
    fake1_addr = 0x09FD9180

    buffer0_addr = 0x09FD92AC # 指向伪造内存的指针
    buffer1_addr = 0x09FD92B4
    initial_state.memory.store(buffer0_addr, fake0_addr, endness=project.arch.memory_endness) # 将指针指向伪造的内存
    initial_state.memory.store(buffer1_addr, fake1_addr, endness=project.arch.memory_endness)

    initial_state.memory.store(fake0_addr, password0) # 将伪造的内存符号化
    initial_state.memory.store(fake1_addr, password1)

    simulation = project.factory.simgr(initial_state)

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

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

    simulation.explore(find=is_successful, avoid=should_abort)

    if simulation.found:
        solution_state = simulation.found[0]

        solution0 = solution_state.se.eval(password0)
        solution1 = solution_state.se.eval(password1)

        solution = long_to_bytes(solution0) + b' ' + long_to_bytes(solution1)
        print(solution)
        print(solution.decode())
    else:
        raise Exception('Could not find solution')

if __name__ == '__main__':
    main()

通过这个题目，我们了解到如何将动态的内存分配的地址进行转换为符号化，我们需要在bss段上找到对应大小的空间来保存我们的输入，然后将符号化后的输入导入到伪装的bss段地址处，之后便可以利用之前符号化内存的方式实现解题，我们学到的关键函数为：

1
2
3
4
5
6
7
8
9
10
11
12
# 对应空白 bss 段内空间
fake_addr = XXX # 伪造malloc得来的内存

# 指向伪造内存的指针
buffer_addr = XXX # 输入的存放地址 buffer

# 将指针指向伪造的内存
# 参数为输入数据存放地址,bss 段伪造的空间
initial_state.memory.store(buffer_addr, fake_addr, endness=project.arch.memory_endness) 

# 将伪造的内存符号化
initial_state.memory.store(fake_addr, password) # bss 段伪造的地址,符号化的输入

参数：endness=project.arch.memory_endness
在默认情况下，angr使用大端格式往内存中写入整数，这个参数告诉angr使用小端格式写入，这是x86的格式

07_angr_symbolic_file

看到题目发现里面是一个文件操作，从文件里进行读取数据，而我们需要将文件进行符号化处理，而angr也提供了对应的封装模块来供我们进行调用处理。下面列出其符号化文件的方式：

1
2
3
4
5
6
7
8
9
10
11
12
# 开始执行地址
start_addr = XXX

filename = 'XXX' # 文件名称
symbolic_file_size_bytes = 64 # 文件大小(此处写的是字节),也可以直接写入 bit 之后main初始化向量时不需要 * 8

# 初始化位向量
password = claripy.BVS('password', symbolic_file_size_bytes * 8) # * 8 将byte进行转换到bits
password_file = angr.SimFile(filename, content=password, size=symbolic_file_size_bytes) # 符号化文件

# 再初始状态中添加一个虚拟的文件系统
initial_state = project.factory.blank_state(addr=start_addr, fs={filename: password_file})

那么我们就可以直接在第二题的条件约束上扩展，加入这一串对文件进行格式化的操作指令：

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
import sys
import angr
import claripy
from Crypto.Util.number import long_to_bytes

def main():
    binary_path = '../program/07_angr_symbolic_file'
    project = angr.Project(binary_path)

    start_addr = 0x080488EA

    filename = 'MRXJKZYR.txt' # 文件名称
    symbolic_file_size_bytes = 64 # 文件大小(字节)

    password = claripy.BVS('password', symbolic_file_size_bytes * 8) # 初始化位向量
    password_file = angr.SimFile(filename, content=password, size=symbolic_file_size_bytes) # 符号化文件

    initial_state = project.factory.blank_state(addr=start_addr, fs={filename: password_file}) # 再初始状态中添加一个虚拟的文件系统
    simulation = project.factory.simgr(initial_state)

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

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

    simulation.explore(find=is_successful, avoid=should_abort)

    if simulation.found:
        solution_state = simulation.found[0]

        solution = long_to_bytes(solution_state.solver.eval(password))
        print(solution.decode())
    else:
        raise Exception('Could not find solution')
    
if __name__ == '__main__':
    main()

在这节里面我们学会了如何对文件进行符号化，来创建我们的约束求解器，其关键的函数如下：

1
2
3
4
# 符号化文件
password_file = angr.SimFile(filename, content=password, size=symbolic_file_size_bytes)
# 在初始状态添加一个虚拟的文件系统
initial_state = project.factory.blank_state(addr=start_addr, fs={filename: password_file})

08_angr_constraints

把程序拖入进IDA进行分析可以得到如下伪代码，可以看出程序将我们对输入在经过加密后与字符串MRXJKZYRKMKENFZB进行比较值，我们可以轻松的看出目的的比较，但是angr是遍历各个分支来进行模拟的，因此时间开销十分大，我们需要将其进行减小模拟的过程分支来缩短模拟的时间。

那么需要怎么操作？我们可以将buffer进行符号化处理，然后让程序来替代我们加密，之后我们切换到angr中，由我们来对加密后的数据进行检验，看是否与目的字符串相等。

1
2
3
4
# 前半段与之前的方式一样，对输入的数据符号化，载入内存
# 之后进行模拟到检查函数之前
addr_to_check_constraint = 0x08048669
simulation.explore(find=addr_to_check_constraint)

此时我们需要转移到判断加密后的数据上：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
if simulation.found:
    solution_state = simulation.found[0]
	# 加密后的password的地址
    constrained_parameter_addr = 0x0804A050 # 即输入字符串保存的地址
    constrained_parameter_size_bytes = 16   # password的长度(字节)
    
     # 从内存中加载password  ( 输入 )
    constrained_parameter_bitvector = solution_state.memory.load(constrained_parameter_addr,constrained_parameter_size_bytes)
    
	# 对比的字符串
    constrained_parameter_desired_value = 'MRXJKZYRKMKENFZB'
    
	# 约束表达式
    constrained_expression = constrained_parameter_bitvector == constrained_parameter_desired_value                 
 	
    # 添加约束
    solution_state.add_constraints(constrained_expression)

    solution = long_to_bytes(solution_state.se.eval(password))
    print(solution.decode())
else:
    raise Exception('Could not find the sokution')

那么脚本如下：

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
import sys
import angr
import claripy
from Crypto.Util.number import long_to_bytes

def main():
    binary_path = '../program/08_angr_constraints'
    project = angr.Project(binary_path)

    start_addr = 0x08048625 # 在输入函数之后
    initial_state = project.factory.blank_state(addr=start_addr)

    password = claripy.BVS('password', 16*8)
    password_addr = 0x0804A050
    initial_state.memory.store(password_addr, password)

    simulation = project.factory.simgr(initial_state)

    addr_to_check_constraint = 0x08048669 # 在检查函数之前
    simulation.explore(find=addr_to_check_constraint)

    if simulation.found:
        solution_state = simulation.found[0]

        constrained_parameter_addr = 0x0804A050 # 加密后的password的地址
        constrained_parameter_size_bytes = 16   # password的长度(字节)
        constrained_parameter_bitvector = solution_state.memory.load(constrained_parameter_addr, constrained_parameter_size_bytes)  # 从内存中加载password

        constrained_parameter_desired_value = 'MRXJKZYRKMKENFZB'  # reference string

        constrained_expression = constrained_parameter_bitvector == constrained_parameter_desired_value                               # 约束表达式

        solution_state.add_constraints(constrained_expression)    # 添加约束

        solution = long_to_bytes(solution_state.se.eval(password))
        print(solution.decode())
    else:
        raise Exception('Could not find the sokution')

if __name__ == '__main__':
    main()

在这一个题目中我们学会了将angr的遍历范围进行约束，来提升求解速度。

1
2
3
4
5
# 从内存中加载password
constrained_parameter_bitvector = solution_state.memory.load(constrained_parameter_addr, constrained_parameter_size_bytes) # 参数为目标值的加载的地址，字节数大小
# 添加约束
constrained_expression = XXX # 条件表达式
solution_state.add_constraints(constrained_expression)

09_angr_hooks

拖入IDA分析，可以看到程序是由两个输入组成，当第一个输入错误时便会退出，其中第一次的输入经过加密后需要等于password，第二次的输入需要等于加密后的password

我们观察一下程序中需要hook的函数，可以看到程序执行的是进行比较字符串的操作，返回的是一个bool类型的数据，对此我们可以直接自己创建一个函数来进行直接比较并返回对应bool值，而不需要通过程序一个个的遍历判断，下面展示如何实现一个hook：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
# 绕过函数的地址
check_equals_caller_addr = 0x080486A9
# 通过 hook 跳过目标函数的长度
instruction_to_skip_length = 0x080486BB - 0x080486A9
# 创建一个 hook 函数
@project.hook(check_equals_caller_addr, instruction_to_skip_length) # 参数为绕过函数的地址,绕过函数长度
def skip_check_equals(state):
    user_input_buffer_addr = 0x0804A054	# 保存输入变量地址
    user_input_buffer_length = 16	# 第一个 scanf 的输入长度，此处为字节大小
    # 将输入载入内存
    user_input_string = state.memory.load(
        user_input_buffer_addr,
        user_input_buffer_length
    )
	# 目的字符串
    check_against_string = 'MRXJKZYRKMKENFZB'
	# 创建判断条件 -> 字符串的比较
    state.regs.eax = claripy.If(
        user_input_string == check_against_string,
        claripy.BVV(1, 32), # 程序的返回值是给寄存器 eax 保存
        claripy.BVV(0, 32) # eax 为 32 bit 的寄存器，所以大小设置为 32
    )  # claripy.BVV(返回数据,返回 bit 大小)      
# 开始模拟
simulation = project.factory.simgr(initial_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
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
import sys
import angr
import claripy


def main():
    binary_path = './09_angr_hooks'
    project = angr.Project(binary_path)

    initial_state = project.factory.entry_state()

    # 绕过函数的地址
    check_equals_caller_addr = 0x080486A9
    # 通过 hook 跳过目标函数的长度
    instruction_to_skip_length = 0x080486BB - 0x080486A9

    # 创建一个 hook 函数
    # 参数为绕过函数的地址,绕过函数长度
    @project.hook(check_equals_caller_addr, length = instruction_to_skip_length)
    def skip_check_equals(state):
        user_input_buffer_addr = 0x0804A054  # 保存输入变量地址
        user_input_buffer_length = 16  # 第一个 scanf 的输入长度，此处为字节大小
        # 将输入载入内存
        user_input_string = state.memory.load(
            user_input_buffer_addr,
            user_input_buffer_length
        )
        # 目的字符串
        check_against_string = 'MRXJKZYRKMKENFZB'
        # 创建判断条件 -> 字符串的比较
        # 同时设定返回值
        state.regs.eax = claripy.If(
            user_input_string == check_against_string,
            claripy.BVV(1, 32),  # 程序的返回值是给寄存器 eax 保存
            claripy.BVV(0, 32)  # eax 为 32 bit 的寄存器，所以大小设置为 32
        )  # claripy.BVV(返回数据,返回 bit 大小)
    def is_successful(state):
        stdout_output = state.posix.dumps(sys.stdout.fileno())
        return b'Good Job.' in stdout_output

    def should_abort(state):
        stdout_output = state.posix.dumps(sys.stdout.fileno())
        return b'Try again.' in stdout_output
    # 开始模拟
    simulation = project.factory.simgr(initial_state)
    simulation.explore(find=is_successful, avoid=should_abort)

    if simulation.found:
        solution_state = simulation.found[0]

        solution = solution_state.posix.dumps(sys.stdin.fileno())

        print(solution.decode())
    else:
        raise Exception('Could not find the solution')


if __name__ == '__main__':
    main()

通过这个例子我们学会了使用hook来代替程序中的函数，并执行我们自己构造的函数。其关键函数如下

1
2
3
4
5
6
7
8
9
10
# 创建一个 hook 函数
# 参数为绕过函数的地址,绕过函数长度
@project.hook(check_equals_caller_addr, length = instruction_to_skip_length)
# 创建判断条件 -> 字符串的比较
# 同时设定返回值
state.regs.eax = claripy.If(
    user_input_string == check_against_string, # 创建判断语句
    claripy.BVV(1, 32),  # 程序的返回值是给寄存器 eax 保存
    claripy.BVV(0, 32)  # eax 为 32 bit 的寄存器，所以大小设置为 32
)  # claripy.BVV(返回数据,返回 bit 大小)

10_angr_simprocedures

上一道题目我们是只利用一个hook进行模拟了一个函数，但是在这个题目里面我们可以找到许许多多的函数，如果一个个写会累死的 ( bushi )

所以在这个题目中我们需要想办法hook一片的函数，那么我们为什么不想一下我们把名字hook了，意味着每次调用这个相同名字的函数时执行的便是我们自己编写的过程。实现如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
# 创建一个类
   class mySimPro(angr.SimProcedure):
       def run(self, user_input_addr, user_input_length):
           # angr 输入的符号向量
           angr_bvs = self.state.memory.load(
               user_input_addr,
               user_input_length
           )
           # 目标字符串
           desired = 'MRXJKZYRKMKENFZB'
           return claripy.If(
               desired == angr_bvs, # 条件判断
               claripy.BVV(1,32), # 返回值设置
               claripy.BVV(0,32)
           )
   
   # hook 的函数名
   check_symbol = 'check_equals_MRXJKZYRKMKENFZB'
   # 创建 hook
   project.hook_symbol(check_symbol,mySimPro())    # 创建一个类来继承 angr.SimProcedure
   simulation = project.factory.simgr(initial_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
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
from pydoc import describe
import angr
import sys
import claripy


def main():
    binary_path = './09_angr_hooks'
    project = angr.Project(binary_path)
    initial_state = project.factory.entry_state()

    # 创建一个类
    class mySimPro(angr.SimProcedure):
        def run(self, user_input_addr, user_input_length):
            # angr 输入的符号向量
            angr_bvs = self.state.memory.load(
                user_input_addr,
                user_input_length
            )
            # 目标字符串
            desired = 'MRXJKZYRKMKENFZB'
            return claripy.If(
                desired == angr_bvs, # 条件判断
                claripy.BVV(1,32), # 返回值设置
                claripy.BVV(0,32)
            )
    
    # hook 的函数名
    check_symbol = 'check_equals_MRXJKZYRKMKENFZB'
    # 创建 hook
    project.hook_symbol(check_symbol,mySimPro())    # 创建一个类来继承 angr.SimProcedure
    simulation = project.factory.simgr(initial_state)

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

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

    simulation.explore(find=is_successful, avoid=should_abort)

    if simulation.found:
        solution_state = simulation.found[0]

        solution = solution_state.posix.dumps(sys.stdin.fileno())

        print(solution.decode())
    else:
        raise Exception('Could not find the solution')


if __name__ == '__main__':
    main()

在这道题目中我们学习了如何hook一个函数名，从而使程序在每次运行到这个函数名时执行的都是我们hook后的函数，对此我们利用继承的方式对其进行hook：

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
class ReplacementCheckEquals(angr.SimProcedure): # 继承angr的SimProcedure类
    def run(self, to_check, length):             # 模拟 angr 的输入
        user_input_buffer_addr = to_check
        user_input_buffer_length = length

        user_input_string = self.state.memory.load(
            user_input_buffer_addr,
            user_input_buffer_length
        )

        check_against_string = XXX # 检查函数，来判断输入的正确与否 

        return claripy.If(
            user_input_string == check_against_string,
            claripy.BVV(1, 32), # 返回值 返回值的 bit 位大小
            claripy.BVV(0, 32)
        )


# 没去符号名时
check_equals_symbol = 'check_equals_MRXJKZYRKMKENFZB' # 函数名
project.hook_symbol(check_equals_symbol, ReplacementCheckEquals())
-----------------------------------------------------------------------------------
# hook原来的check函数，也可以使用上面的代码，但是如果程序去符号的话，就只能这种方法
check_equals_addr = XXX
project.hook(check_equals_addr, ReplacementCheckEquals())  # 目标函数的地址,继承了angr.SimProcedure的类名

11_angr_sim_scanf

随着angr的更新迭代，似乎逐渐支持了scanf这一类的函数，可以不需要手动模拟scanf，angr可以直接自动化模拟，问了一下草莓师傅，似乎angr现在还能自动hook，关于这个我也没有去测试过，也不是太了解这些。

根据题目要求，需要我们模拟scanf来进行模拟输入，实现方式似乎类似于hook函数名，同样需要我们进行继承angr下的SimpProcedure，只是里面的一些函数发生了变化：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
class ReplacementScanf(angr.SimProcedure):
   def run(self, fmt, scanf0_addr, scanf1_addr):
        scanf0 = claripy.BVS('scanf0', 4*8) # 符号化输入
        scanf1 = claripy.BVS('scanf1', 4*8)

        self.state.memory.store(scanf0_addr, scanf0, endness=project.arch.memory_endness) # 将输入保存到内存空间
        self.state.memory.store(scanf1_addr, scanf1, endness=project.arch.memory_endness)

        self.state.globals['solution0'] = scanf0 # 将scanf0和scanf1保存到当前状态
        self.state.globals['solution1'] = scanf1
    
    scanf_symbol = '__isoc99_scanf'  # 类似于 hook 函数名的方式
    project.hook_symbol(scanf_symbol, ReplacementScanf())

    simulation = project.factory.simgr(initial_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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
import sys
import angr
import claripy

def main():
    binary_path = '../program/11_angr_sim_scanf'
    project = angr.Project(binary_path)

    initial_state = project.factory.entry_state()

    class ReplacementScanf(angr.SimProcedure):

        def run(self, fmt, scanf0_addr, scanf1_addr):
            scanf0 = claripy.BVS('scanf0', 4*8)
            scanf1 = claripy.BVS('scanf1', 4*8)

            self.state.memory.store(scanf0_addr, scanf0, endness=project.arch.memory_endness)
            self.state.memory.store(scanf1_addr, scanf1, endness=project.arch.memory_endness)

            self.state.globals['solution0'] = scanf0 # 将scanf0和scanf1保存到当前状态
            self.state.globals['solution1'] = scanf1

    scanf_symbol = '__isoc99_scanf' 
    project.hook_symbol(scanf_symbol, ReplacementScanf())

    simulation = project.factory.simgr(initial_state)

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

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

    simulation.explore(find=is_successful, avoid=should_abort)

    if simulation.found:
        solution_state = simulation.found[0]

        solution0 = solution_state.globals['solution0'] #从当前状态取出scanf0和scanf1
        solution1 = solution_state.globals['solution1']

        solution = '%u %u' % (solution_state.se.eval(solution0), solution_state.se.eval(solution1))
        print(solution)
    else:
        raise Exception('Could not find the solution')

if __name__ == '__main__':
    main()

我们在这个题中同样利用到了符号化函数名的方式来对一堆的scanf进行模拟，并将其保存在内存段里，具体函数如下：

1
2
self.state.globals['solution0'] = scanf0 # 将 scanf0 进行保存
solution0 = solution_state.globals['solution0'] # 从当前状态取出 scanf0

12_angr_veritesting

在这个题目中与01的avoid来约束目标输出字符串，但是这个题目中循环的次数较大，如果直接套用01的脚本可能会出现路径爆炸 ( angr模拟执行时遍历的路径是成指数级上涨，如果都需要需要执行那么便会引发错误 )，我们之前所做的hook函数，添加约束条件都是有效的防止路径爆炸的操作，我们接下来采用一个新的方式来解决路径爆炸的问题：

1
sm=p.factory.simulation_manager(istate,veritesting=True)

这个函数让我们直接忽视循环结构，直接进行求解，一般耗时会比较长。

加入这个防止路径爆炸的脚本为：

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 sys
import angr

def main():
    binary_path = '../program/12_angr_veritesting'
    project = angr.Project(binary_path)

    initial_state = project.factory.entry_state()
    simulation = project.factory.simgr(initial_state, veritesting=True) # 设置自动合并路径

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

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

    simulation.explore(find=is_successful, avoid=should_abort)

    if simulation.found:
        solution_state = simulation.found[0]

        solution = solution_state.posix.dumps(sys.stdin.fileno())
        print(solution)
    else:
        raise Exception('Could not find the solution')

if __name__ == '__main__':
    main()

13_angr_static_binary

这个示例的逻辑和01题是一样的,主要不同的地方是在于这个程序是静态链接编译的,所以程序中包含了一些libc的函数实现,但是这里可能会存在两个问题:

  1. 这些函数里面隐藏一些出题人的坑;

  2. 这些函数里面的实现可能会依赖其他的系统函数或者实现方式不相同.所以12 题主要是让我们通过Hook 的方式重定向函数中被调用的libc 的函数

首先,Linux 下启动main() 函数需要通过__libc_start_main 对程序进行初始化,然后再跳转到main() 函数;其次,在main() 函数里面调用了printf ,scanf ,puts ,所以我们需要通过Hook 来重定向它们.

幸运的是,我们不需要重新实现这些函数的实现,Angr 代码库里面已经帮我们实现了一部分libc 的函数库,所以我们只需要倒入它们即可.

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 angr
import sys


project = angr.Project(sys.argv[1])
initial_state = project.factory.entry_state()
simulation = project.factory.simgr(initial_state,veritesting = True) # 开启自动合并路径

project.hook(0x804ed40, angr.SIM_PROCEDURES['libc']['printf']()) # hook库函数
project.hook(0x804ed80, angr.SIM_PROCEDURES['libc']['scanf']())
project.hook(0x804f350, angr.SIM_PROCEDURES['libc']['puts']())
project.hook(0x8048d10, angr.SIM_PROCEDURES['glibc']['__libc_start_main']())

def is_successful(state):
  stdout_output = state.posix.dumps(sys.stdout.fileno())
  return 'Good Job.' in str(stdout_output)  # :boolean

def should_abort(state):
  stdout_output = state.posix.dumps(sys.stdout.fileno())
  return 'Try again.' in str(stdout_output)  # :boolean

simulation.explore(find = is_successful,avoid = should_abort)

if simulation.found :
  solution_state = simulation.found[0]
  print(solution_state.posix.dumps(sys.stdin.fileno()))

通过上述题目，我们了解到了如何将静态链接中的库函数进行hook，从而来获取libc 的函数库：

1
2
project.hook(<调用地址>, angr.SIM_PROCEDURES['<系统库名>']['<系统函数名>']()) # hook库函数
angr.SIM_PROCEDURES[ 系统库名 ] [ 系统函数名 ] ()  =>  获取Angr 内部实现的系统函数

14_angr_shared_library

在编译好的程序中我们可以看到有一个validate函数对我们的输入进行了比较，但是进入这个函数却发现没有相关的实现方式

这是因为validate在共享库里，即程序提供的so中，事实上so也算是一种可执行文件，但是没有经过符号链接，我们需要的便是通过angr加载共享库，然后伪造参数来对validate函数进行调用。

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
def main(argv):
  path_to_binary = sys.argv[1]  #  注意我们是要load so 库而不是执行程序

  base = 0x400000  #  base 基址是随意定的,可以随意修改
  project = angr.Project(path_to_binary, load_options={
    'main_opts' : {
      'custom_base_addr' : base
    }
  })

  buffer_pointer = claripy.BVV(0x3000000, 32)  #  创建一个buffer 指针值
  validate_function_address = base + 0x6D7
  initial_state = project.factory.call_state(validate_function_address, buffer_pointer,claripy.BVV(8, 32))  #  调用validate_function,因为函数声明validata_function(buffer_point,buffer_length) ,所以我们构造出调用validata_function(0x3000000,0x8) .

  password = claripy.BVS('password', 8 * 8)  #  创建一个求解对象,大小为8 字节
  initial_state.memory.store(buffer_pointer, password)  #  保存到0x30000000

  simulation = project.factory.simgr(initial_state)

  simulation.explore(find = base + 0x783)  #  执行到validate 函数的RETN 指令

  if simulation.found:
    solution_state = simulation.found[0]

    solution_state.add_constraints(solution_state.regs.eax != 0)  #  记得,我们要求validate 函数的返回值为1 的时候就是有解的,那么我们就需要在求解的时候添加上这么一个求解约束条件EAX 不能为False .
    solution = solution_state.se.eval(password)
    print(solution)

15_angr_arbitrary_read

单纯的从程序上看的话似乎程序一直是输入错误，但是我们到栈上看输入的变量，可以发现读入了20个字符，但是栈空间中到s的距离仅有16，所以意味着多出来的4字节会覆盖s保存的地址，因此我们可以直接用这4字节进行替换到输出正确的地址处。

所以脚本可以如下进行编写：

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
def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)

  initial_state = project.factory.entry_state()

  class ReplacementScanf(angr.SimProcedure):  #  实现Scanf Hook 函数

    def run(self, format_string, check_key_address,input_buffer_address):
      scanf0 = claripy.BVS('scanf0', 4 * 8)   # check_key
      scanf1 = claripy.BVS('scanf1', 20 * 8)  # input_buffer

      for char in scanf1.chop(bits=8):
        self.state.add_constraints(char >= '0', char <= 'z')  #  对input_buffer 的输入约束

      self.state.memory.store(check_key_address, scanf0, endness=project.arch.memory_endness)
      self.state.memory.store(input_buffer_address, scanf1,endness=project.arch.memory_endness)  #  保存求解变量到指定的内存中

      self.state.globals['solution0'] = scanf0  #  保存这两个变量到state 中,后续求解需要用到
      self.state.globals['solution1'] = scanf1

  scanf_symbol = '__isoc99_scanf'
  project.hook_symbol(scanf_symbol, ReplacementScanf())  #  Hook scanf 函数

  def check_puts(state):
    puts_parameter = state.memory.load(state.regs.esp + 4, 4, endness=project.arch.memory_endness)  #  获取puts() 函数的参数

    if state.se.symbolic(puts_parameter):  #  检查这个参数是否为符号化对象
      good_job_string_address = 0x4D525854B

      copied_state = state.copy()  #  复制执行状态上下文进行约束求解,不影响原理的执行上下文

      copied_state.add_constraints(puts_parameter == good_job_string_address)  #  puts 的参数地址是否可以被指定为0x4D525854B ,如果可以的话,那就证明这个值是可控的

      if copied_state.satisfiable():  #  判断添加了上面这个约束是否有解
        state.add_constraints(puts_parameter == good_job_string_address)  #  如果有解的话就保存到我们执行的那个状态对象
        return True 
      else:
        return False
    else:
      return False

  simulation = project.factory.simgr(initial_state)
    
  def is_successful(state):
    puts_address = 0x8048370  #  当程序执行到puts() 函数时,我们就认为路径探索到了这里,然后再去通过check_puts() 判断这里是否存在漏洞,告诉Angr这是不是我们需要找的那条执行路径
    
    if state.addr == puts_address:
      return check_puts(state)
    else:
      return False

  simulation.explore(find=is_successful)

  if simulation.found:
    solution_state = simulation.found[0]

    solution0 = solution_state.se.eval(solution_state.globals['solution0'])
    solution1 = solution_state.se.eval(solution_state.globals['solution1'],cast_to=bytes)  #  输出字符串序列化的内容

    print(solution0,solution1)

通过这个题目我们可以学习到添加对输入的约束，和复制状态的上下文，以及序列化内容转化为字符串：

1
2
3
4
5
state.copy()  # 复制状态上下文

state.satisfiable()  # 判断当前的所有约束是否有解

solution_state.se.eval(求解变量,cast_to=bytes)  # 序列化变量内容为字符串

16_angr_arbitrary_write

从程序看，其最终目的是将password_buffer里面的字符替换成KZYRKMKE，但是程序中彬没有指向password_buffer的变量，同时我们也发现与上一个题目一样函数存在溢出的漏洞，所以我们利用这个4字节溢出将目的password_buffer的值修改，达到输出正确的目的。

脚本如下：

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
def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)
  initial_state = project.factory.entry_state()

  class ReplacementScanf(angr.SimProcedure):

    def run(self, format_string, check_key ,input_buffer):
      scanf0 = claripy.BVS('scanf0', 4 * 8)
      scanf1 = claripy.BVS('scanf1', 20 * 8)

      for char in scanf1.chop(bits=8):
        self.state.add_constraints(char >= '0', char <= 'z')

      self.state.memory.store(check_key, scanf0, endness=project.arch.memory_endness)
      self.state.memory.store(input_buffer, scanf1, endness=project.arch.memory_endness)

      self.state.globals['solution0'] = scanf0
      self.state.globals['solution1'] = scanf1

  scanf_symbol = '__isoc99_scanf'
  project.hook_symbol(scanf_symbol, ReplacementScanf())

  def check_strncpy(state):
    strncpy_dest = state.memory.load(state.regs.esp + 4, 4, endness=project.arch.memory_endness)  #  获取strncpy() 的参数,strncpy_dest ..
    strncpy_src  = state.memory.load(state.regs.esp + 8, 4, endness=project.arch.memory_endness)
    strncpy_len  = state.memory.load(state.regs.esp + 12, 4, endness=project.arch.memory_endness)
    src_contents = state.memory.load(strncpy_src, strncpy_len)  #  因为参数中只保存了地址,我们需要根据这个地址去获取内容

    if state.se.symbolic(strncpy_dest) and state.se.symbolic(src_contents) :  #  判断dest 和src 的内容是不是符号化对象
      if state.satisfiable(extra_constraints=(src_contents[ -1 : -64 ] == 'KZYRKMKE' ,strncpy_dest == 0x4D52584C)):  #  尝试求解,其中strncpy_dest == 0x4D52584C 的意思是判断dest 是否可控为password 的地址;src_contents[ -1 : -64 ] == 'KZYRKMKE' 是判断input_buffer 的内容是否可控为'KZYRKMKE' ,因为这块内存是倒序,所以需要通过[ -1 : -64 ] 倒转(contentes 的内容是比特,获取8 字节的大小为:8*8 = 64),然后判断该值是否为字符串'KZYRKMKE'
        state.add_constraints(src_contents[ -1 : -64 ] == 'KZYRKMKE',strncpy_dest == 0x4D52584C)
        return True
      else:
        return False
    else:
      return False

  simulation = project.factory.simgr(initial_state)

  def is_successful(state):
    strncpy_address = 0x8048410

    if state.addr == strncpy_address:
      return check_strncpy(state)
    else:
      return False

  simulation.explore(find=is_successful)

  if simulation.found:
    solution_state = simulation.found[0]
    solution0 = solution_state.se.eval(solution_state.globals['solution0'])
    solution1 = solution_state.se.eval(solution_state.globals['solution1'],cast_to=bytes)

    print(solution0,solution1)

17_angr_arbitrary_iump

一打开程序一看就只有一个输入，和一个输入错误，我们查看其函数，发现在某个地址处可以发现有输出Good，我们可以判断出这个是将ret的返回地址进行覆盖然后跳转到对应的输入正确函数地址处。

脚本如下：

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
def main(argv):
  path_to_binary = argv[1]
  project = angr.Project(path_to_binary)
  initial_state = project.factory.entry_state()

  simulation = project.factory.simgr(
    initial_state,
    save_unconstrained=True,
    stashes={
      'active' : [initial_state],
      'unconstrained' : [],
      'found' : [],
      'not_needed' : []
    }
  )

  class ReplacementScanf(angr.SimProcedure):

    def run(self, format_string, input_buffer_address):
      input_buffer = claripy.BVS('input_buffer', 64 * 8)  #  设置一个较大的input_buffer

      for char in input_buffer.chop(bits=8):
        self.state.add_constraints(char >= '0', char <= 'z')

      self.state.memory.store(input_buffer_address, input_buffer, endness=project.arch.memory_endness)

      self.state.globals['solution'] = input_buffer

  scanf_symbol = '__isoc99_scanf'
  project.hook_symbol(scanf_symbol, ReplacementScanf())  #  对scanf() 做Hook

  while (simulation.active or simulation.unconstrained) and (not simulation.found):  #  
    for unconstrained_state in simulation.unconstrained:
      def should_move(s):
        return s is unconstrained_state
      
      simulation.move('unconstrained', 'found', filter_func=should_move)  #  保存

    simulation.step()  #  步进执行

  if simulation.found:
    solution_state = simulation.found[0]

    solution_state.add_constraints(solution_state.regs.eip == 0x4D525849)  #  判断EIP 地址是否可控

    solution = solution_state.se.eval(solution_state.globals['solution'],cast_to = bytes)  #  生成Payload
    print(solution)
Reverse
Angr 学习笔记
https://equinox-shame.github.io/2022/03/19/Angr 学习笔记/
作者
梓曰
发布于
2022年3月19日
许可协议