参考：angr
AngrCTF_FITM/笔记/03/Angr_CTF从入门到精通（三）.md at master · ZERO-A-ONE/AngrCTF_FITM

angr_explore

00_angr_find

IDA分析结果：

逻辑简单，输入，complex_function进行加密，加密结果等于JACEJGCS就成功

angr：

import angr
import sys
def Go():path_to_binary = "00_angr_find"project = angr.Project(path_to_binary, auto_load_libs = False)# 模拟程序运行状态，获取程序上下文init_state = project.factory.entry_state()# 模拟程序向下执行simulation = project.factory.simgr(init_state)print_good_address = 0x8048675# 设置出口simulation.explore(find=print_good_address)if simulation.found:# 找到的正确路径solution_state = simulation.found[0]# 打印找到的输入solution = solution_state.posix.dumps(sys.stdin.fileno())print("[+] Success! Solution is: {}".format(solution.decode("utf-8")))else:raise Exception("Could not find the solution")if __name__ == "__main__":Go()

代码过程：

• 创建 project
• 设置 state
• 新建符号量 : BVS (bitvector symbolic ) 或 BVV (bitvector value)
• 把符号量设置到内存或者其他地方
• 设置 Simulation Managers ， 进行路径探索的对象
• 运行，探索满足路径需要的值
• 约束求解，获取执行结果

输出：

[+] Success! Solution is: JXWVXRKX

01_angr_avoid

主函数太大无法编译，但是可以分析，目标是到达 maybe_good，不能到达 avoid_me:

angr代码：

import angr
import sysdef angr_process():project = angr.Project("01_angr_avoid")# 获取程序快照（上下文）init_state = project.factory.entry_state()# 获取一个模拟状态，让程序下一步执行simgr = project.factory.simgr(init_state)avoid_me = 0x80485a8maybe_good = 0x80485b5# explore 返回一个SM，所有找到路径simgr.explore(find = maybe_good, avoid = avoid_me)if simgr.found:# 选择第一个成功的路径solution_state = simgr.found[0]print(solution_state)solution_dump = solution_state.posix.dumps(sys.stdin.fileno())print("[+] Success! Solution is:{}".format(solution_dump.decode("utf-8")))if __name__ == "__main__":angr_process()

02_angr_find_condition

angr代码：

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('02_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))

这里通过is_successful函数判断当前状态的输出流中是否包含b’Good Job.'，如果包含则表示到达目的地址，ok，此时可以打印对应的输入了。should_avoid函数同理。

除了传入一个函数以外，我们也可以使用lambda表达式来简化代码：

import angrproj = angr.Project('dist/02_angr_find_condition')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
# simgr.explore(find=is_successful, avoid=should_avoid)
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))

angr_symbolic

angr在默认情况下只会符号化从标准输入流中读取的数据，而实际情况往往需要我们符号化其他数据，如寄存器、某块内存甚至是某个文件。这一节我们来学习如何手动符号化并且利用angr内置的约束求解器对符号值进行约束求解。

03_angr_symbolic_registers

这里用 get_user_input 获取用户输入，也可以用之前的方法解出：

import angrproj = angr.Project('03_angr_symbolic_registers')
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))

但为了体现本节的主题，即手动符号化与约束求解，我们尝试换一种方法来解决这道题。

要准确进行符号化，我们得从汇编着手分析：

可以看到 get_user_input 函数获取到用户输入后，将输入的内容保存在三个寄存器里，然后通过寄存器赋值给其他变量。所以这里考虑符号化寄存器。
让程序能够达到 Good Job 位置。

angr代码：

import angr
import claripyproj = angr.Project('03_angr_symbolic_registers')
state = proj.factory.blank_state(addr=0x8048980)
# 符号化寄存器
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=0x80489E6)
#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))}')if simgr.found:for solve in simgr.found:solution_state = solvesolution0 = format(solution_state.solver.eval(password0), 'x')solution1 = format(solution_state.solver.eval(password1), 'x')solution2 = format(solution_state.solver.eval(password2), 'x')solution = solution0 + " " + solution1 + " " + solution2print("[+] Success! Solution is: {}".format(solution))

注意这里的初始state是通过blank_state函数而不是entry_state函数获得的。
因为在0x8048980之前的指令对我们的求解其实是没有任何作用的，包括get_user_input函数，因为接下来我们就要将get_user_input函数的结果符号化了，而不是让angr自动帮我们符号化通过scanf读取的数据。

可能有同学还会有疑问：如果直接从0x8048980这个地址开始符号执行，那初始的状态是什么样的呢？根据x86汇编常识，像eax，ebx，ecx这样的寄存器是上下文无关的，也就是说一个函数内不会引用在函数外部设置的eax，ebx或者ecx的值，而是在函数内部对寄存器重新初始化并使用。
所以我们用blank_state获取的状态，即时初始的一些寄存器处于未初始化状态也是丝毫没有影响的，因为它们马上就会被初始化。至于esp，angr会给他们一个默认的初值，使接下来的函数调用不会爆炸：

state.regs.esp
<BV32 0x7fff0000>

ebp的初始值仍然是未初始化的，但对我们后续的符号执行没有影响，不管它就行：

state.regs.ebp
<BV32 reg_1c_3_32{UNINITIALIZED}>

04_angr_symbolic_stack

了解了对寄存器的符号化之后，我们再看看如何对栈空间内的数据进行符号化。

这次也要从scanf之后开始执行：

state = proj.factory.blank_state(addr=0x8048694)

之前我们说过通过blank_state获取初始状态，ebp的值是未约束的。在这题中，我们之后要向栈中push符号值，并且通过ebp索引这些符号值（比如[ebp+var_C]），所以我们得让ebp有一个正确的初值了。之所以说是正确的初值，是因为我们跳过了函数开头对栈的调整，因此我们还需要手动调整ebp的值：
ebp的值是什么不重要，我们只需要保证它和esp的偏移是正确的即可，对前面的汇编指令进行分析我们可以得出此时ebp的偏移量为：0x18+4+4+4+4=40:

state.regs.ebp = state.regs.esp + 40

然后对esp的值执行调整，使我们接下来push进去的符号值恰好在[ebp+var_10]和[ebp+var_C]这两个位置，记得push完之后要把esp调回来：

state.regs.esp = state.regs.ebp - 0x8
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

angr代码：

import angr
import claripyproj = angr.Project('../dist/04_angr_symbolic_stack')
state = proj.factory.blank_state(addr=0x8048694)
state.regs.ebp = state.regs.esp + 40
state.regs.esp = state.regs.ebp - 0x8
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=0x80486E1)
solver = simgr.found[0].solver
print(f'password0: {hex(solver.eval(password0))}')
print(f'password1: {hex(solver.eval(password1))}')

这个思路是完整的，但是可以简化，明显发现有两行代码冗余了：

state.regs.ebp = state.regs.esp + 40
state.regs.esp = state.regs.ebp - 0x8
==>
state.regs.esp = state.regs.esp + 32
...
state.regs.esp = state.regs.ebp - 40

再简化一点呢，其实咱不用自己去开栈，然后平栈，只要保障局部变量相对于ebp位置是对的就可以了。
angr代码：

import angr
import sys
import claripy
def Go():path_to_binary = "./04_angr_symbolic_stack" project = angr.Project(path_to_binary, auto_load_libs=False)start_address = 0x8048697initial_state = project.factory.blank_state(addr=start_address)# 让ebp = esp，存在疑问，这个状态下，ebp是未初始化的，esp是有值的initial_state.regs.ebp = initial_state.regs.esppasswd_size_in_bits = 32passwd0 = claripy.BVS('passwd0', passwd_size_in_bits)passwd1 = claripy.BVS('passwd1', passwd_size_in_bits)# 把栈提高8个字节，因为main访问两个输入值是通过ebp+c 和 ebp+0x10padding_length_in_bytes = 0x8initial_state.regs.esp -= padding_length_in_bytes# 符号化栈initial_state.stack_push(passwd0)initial_state.stack_push(passwd1)simgr = project.factory.simgr(initial_state)def is_successful(state):stdout_output = state.posix.dumps(1)if b'Good Job.\n' in stdout_output:return Trueelse: return Falsedef should_abort(state):stdout_output = state.posix.dumps(1)if b'Try again.\n' in  stdout_output:return Trueelse: return Falsesimgr.explore(find=is_successful, avoid=should_abort)if simgr.found:for i in simgr.found:solution_state = isolution0 = (solution_state.solver.eval(passwd0))solution1 = (solution_state.solver.eval(passwd1))print("[+] Success! Solution is: {0} {1}".format(solution0, solution1))#print(solution0, solution1)else:raise Exception('Could not find the solution')
Go()

咱用 0x8048697 开始执行，调用scanf的栈就不用管了，保证handle_user函数中参数与ebp之间的偏移正确就好了，handle_user函数里有两个参数[ebp+var_10]和[ebp+var_C]，所以把esp先抬高 0x8 ，后面这将符号化的值压入栈，符号化的值就在[ebp+var_10]和[ebp+var_C]位置了，后面就可以直接使用了。

eval

• solver.eval(expression) 将会解出一个可行解
• solver.eval_one(expression)将会给出一个表达式的可行解，若有多个可行解，则抛出异常。
• solver.eval_upto(expression, n)将会给出最多n个可行解，如果不足n个就给出所有的可行解。
• solver.eval_exact(expression, n)将会给出n个可行解，如果解的个数不等于n个，将会抛出异常。
• solver.min(expression)将会给出最小可行解
• solver.max(expression)将会给出最大可行解

另外还有还有cast_to可以接收一个参数来指定把结果映射到哪种数据类型。目前这个参数只能是str，它将会以字符串形式展示返回的结果
参考：AngrCTF_FITM/笔记/02/Angr_CTF从入门到精通（二）.md at master · ZERO-A-ONE/AngrCTF_FITM

05_angr_symbolic_memory

输入保存在一个全局变量user_input里：

user_input是一个32字节长度的字符串。

angr代码：

import angr
import claripyproj = angr.Project('05_angr_symbolic_memory')
state = proj.factory.blank_state(addr=0x80485FE)
password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
password2 = claripy.BVS('password2', 64)
password3 = claripy.BVS('password3', 64)
state.mem[0xA1BA1C0].uint64_t = password0
state.mem[0xA1BA1C0 + 8].uint64_t = password1
state.mem[0xA1BA1C0 + 16].uint64_t = password2
state.mem[0xA1BA1C0 + 24].uint64_t = password3
simgr = proj.factory.simgr(state)
simgr.explore(find=0x804866A)
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)}')

操作连续内存也可以用state.memory 的 .load(addr, size) / .store(addr, val) 接口读写内存, size 以 bytes 为单位。

passwd0_address = 0xA1BA1C0
#passwd1_address = 0xA1BA1C8
#passwd2_address = 0xA1BA1D0
#passwd3_address = 0xA1BA1D8
initial_state.memory.store(passwd0_address, password0)
initial_state.memory.store(passwd0_address + 0x8,  password1)
initial_state.memory.store(passwd0_address + 0x10, password2)
initial_state.memory.store(passwd0_address + 0x18, password3)

06_angr_symbolic_dynamic_memory

输入buffer0和buffer1是malloc出来的指针，其中存放的地址不是确定的。
但我们仍然可以在内存中选定一块区域作为输入的地址，比如说在.bss段选定一块未使用的16字节区域，然后对输入进行符号化：

password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
state.mem[0xABCC700].uint64_t = password0
state.mem[0xABCC700 + 8].uint64_t = password1

然后将buffer0和buffer1的地址设成我们刚刚选定的地址：

state.mem[0xABCC8A4].uint32_t = 0xABCC700
state.mem[0xABCC8AC].uint32_t = 0xABCC700 + 8

angr代码：

import angr
import claripyproj = angr.Project('06_angr_symbolic_dynamic_memory')
state = proj.factory.blank_state(addr=0x8048696)
password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
state.mem[0xABCC700].uint64_t = password0
state.mem[0xABCC700 + 8].uint64_t = password1
state.mem[0xABCC8A4].uint32_t = 0xABCC700
state.mem[0xABCC8AC].uint32_t = 0xABCC700 + 8
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8048759)
solver = simgr.found[0].solver
print(f'password0: {solver.eval(password0, cast_to=bytes)}')
print(f'password1: {solver.eval(password1, cast_to=bytes)}')

07_angr_symbolic_file

这题是先把输入写进文件，再从文件中读取输入。
在这题中我们要忽略scanf，直接对文件的内容进行符号化。要对文件内容进行符号化，首先我们要创建一个模拟的文件SimFile，文件名为’OJKSQYDP.txt’，内容为8字节的符号值，大小为0x40字节：

password0 = claripy.BVS('password0', 64)
sim_file = angr.SimFile(name='OJKSQYDP.txt', content=password0, size=0x40)

然后插入到state的文件系统（FileSystem）中，state的文件系统可以通过state.fs获得：

state.fs.insert('OJKSQYDP.txt', sim_file)

angr代码：

import angr
import claripyproj = angr.Project('../dist/07_angr_symbolic_file')
state = proj.factory.blank_state(addr=0x80488D3)
password0 = claripy.BVS('password0', 64)
sim_file = angr.SimFile(name='OJKSQYDP.txt', content=password0, size=0x40)
state.fs.insert('OJKSQYDP.txt', sim_file)
simgr = proj.factory.simgr(state)
simgr.explore(find=0x80489AD)
solver = simgr.found[0].solver
print(f'password0: {solver.eval(password0, cast_to=bytes)}')

angr_constraints

angr在符号执行的过程中，会将路径约束保存在SimState内置的约束求解器内。这一节我们学习如何手动添加约束并进行约束求解，以及应对路径爆炸的一种方法。

08_angr_constraints

代码将输入的buffer通过complex_function加密，在通过check检查密文是不是满足要求。

这题直接调用explore是跑不出来的，因为在check_equals函数中不是比对失败就立刻退出循环，而是一直循环到最后。总共有16轮循环，每次循环会产生比对成功和比对失败两个状态，所以符号执行总共会产生216个状态，导致路径爆炸：

simgr.explore(find=lambda state : b'Good Job.' in state.posix.dumps(1)) # 不行

可以对buffer内存添加约束求解，当buffer值等于"AUPDNNPROEZRJWKB"求解。

angr代码：

import angr
import claripyproj = angr.Project('../dist/08_angr_constraints')
state = proj.factory.blank_state(addr=0x8048622)
password = claripy.BVS('password', 16 * 8)
buffer_addr = 0x804A050
state.memory.store(buffer_addr, password)
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8048669)
found = simgr.found[0]
found.add_constraints(found.memory.load(buffer_addr, 16) == b'AUPDNNPROEZRJWKB')
print(found.solver.eval(password, cast_to=bytes))

路径爆炸

路径爆炸的概念与数学中的指数爆炸概念类似，即某些情况下符号执行的路径/状态以指数级增长。

从08_angr_constraints中我们发现，即使是非常简单的比较函数，也可能让angr产生指数级的路径（216条路径），耗费大量时间甚至根本跑不出来，这就是符号执行的重大缺陷之一——路径爆炸。这既是我们在用符号执行解决实际问题时需要注意的问题，也是一种可以用来抗符号执行的思路。

应对路径爆炸的方法有很多，甚至还有专门的论文来讲述缓解路径爆炸的方法，在上一题中我们学到了最简单的一种：避开会产生路径爆炸的函数，用手动添加约束替代，这是最简单，也是非常好用的一种方法。总的来说，读者们在使用符号执行引擎时，要识别那些会导致路径爆炸的代码，并巧妙绕过。

angr_hooks

09_angr_hooks

这一题的程序流程与上题类似，也是有一个会引起路径爆炸的比较函数。与上题不同的是，这题的比较函数不在整个加密流程的最后，所以我们不能再采用上题手动添加约束并求解的方法。
既然check_equals函数本身的流程非常简单，那么我们就可以用hook技术将check_equals函数替换为一个等效的并且不会导致路径爆炸的函数，然后再进行符号执行。

@proj.hook(addr=0x80486B3, length=5)  # check_equals_XYMKBKUHNIQYNQXE
def my_check_equals(state):buffer_addr = 0x804A054buffer = state.memory.load(buffer_addr, 16)state.regs.eax = claripy.If(buffer == b'XYMKBKUHNIQYNQXE', claripy.BVV(1, 32), claripy.BVV(0, 32))

这里的hook是对call指令进行了hook，而不是函数本身，length指的是跳过的字节数，call指令占5个字节，所以length=5：

angr代码：

import angr
import claripyproj = angr.Project('09_angr_hooks')@proj.hook(addr=0x80486B3, length=5)  # check_equals_XYMKBKUHNIQYNQXE
def my_check_equals(state):buffer_addr = 0x804A054buffer = state.memory.load(buffer_addr, 16)state.regs.eax = claripy.If(buffer == b'XYMKBKUHNIQYNQXE', claripy.BVV(1, 32), claripy.BVV(0, 32))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))

10_angr_simprocedures

反编译结果：

这么看没问题，看看图结构发现有很多调用check函数的，HOOK call指令是行不通了。

所以要HOOK函数本身。
接下来我们就要引入一种对函数本身进行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'ORSDDWXHZURJRBDH', claripy.BVV(1, 32), claripy.BVV(0, 32))

SimProcedure按字面意思来理解就是“模拟程序”，在这里我们用一个SimProcedure的子类MyCheckEquals模拟了check_equals_ORSDDWXHZURJRBDH函数的功能，SimProcedure中的run函数由子类实现，其接收的参数与C语言中的参数保持一致，返回为对应原函数的返回值。

定义好了SimProcedure之后，我们需要调用hook_symbol函数对程序中名为check_equals_ORSDDWXHZURJRBDH的函数进行hook：

proj.hook_symbol(symbol_name='check_equals_ORSDDWXHZURJRBDH', simproc=MyCheckEquals())

hook之后angr在符号执行的过程中将不会调用原先的check_equals_ORSDDWXHZURJRBDH函数，而且MyCheckEquals类中的run函数。然后我们就可以用老方法解决这道题了。

angr代码：

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'ORSDDWXHZURJRBDH', claripy.BVV(1, 32), claripy.BVV(0, 32))proj = angr.Project('10_angr_simprocedures')
proj.hook_symbol(symbol_name='check_equals_ORSDDWXHZURJRBDH', 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))

11_angr_sim_scanf

关于这一题，angr_ctf给的说法是angr不支持多个参数的scanf：

This time, the solution involves simply replacing scanf with our own version, since Angr does not support requesting multiple parameters with scanf.

然而实际上是可以的，可能以前的版本不行，毕竟angr版本迭代还是很快的：

import angrproj = angr.Project('../dist/11_angr_sim_scanf')
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))

angr在angr/procedures中定义了很多模拟系统函数的SimProcedures。这些SimProcedures我们都可以通过angr.SIM_PROCEDURES来获得，用法如下：

proj.hook_symbol("__isoc99_scanf", angr.SIM_PROCEDURES['libc']['scanf']())

根据猜测，angr会根据导入表自动识别动态链接的库函数并用自己实现的SimProcedures进行替换的，所以这一步hook完全是多此一举。

angr代码：

import angrproj = angr.Project('11_angr_sim_scanf')
proj.hook_symbol("__isoc99_scanf", angr.SIM_PROCEDURES['libc']['scanf']())  # 多此一举
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))

方法2：自己hook scanf函数

import angr
import claripydef angr_process():project = angr.Project("11_angr_sim_scanf", auto_load_libs = False)init_state = project.factory.entry_state()class ReplacementScanf(angr.SimProcedure):def run(self, format_string, param0, param1):scanf0 = claripy.BVS("scanf0", 32)scanf1 = claripy.BVS("scanf1", 32)scanf0_address = param0scanf1_address = param1self.state.memory.store(scanf0_address, scanf0, endness = project.arch.memory_endness)self.state.memory.store(scanf1_address, scanf1, endness = project.arch.memory_endness)self.state.globals["solutions"] = (scanf0, scanf1)scanf_symbol = "__isoc99_scanf"project.hook_symbol(scanf_symbol, ReplacementScanf())simgr = project.factory.simgr(init_state)def is_successful(state):stdout_output = state.posix.dumps(1)if b'Good Job.\n' in stdout_output:return Trueelse: return Falsedef should_abort(state):stdout_output = state.posix.dumps(1)if b'Try again.\n' in  stdout_output:return Trueelse: return Falsesimgr.explore(find=is_successful, avoid=should_abort)if simgr.found:for i in simgr.found:solution_state = istored_solutions = solution_state.globals['solutions']scanf0_solution = solution_state.solver.eval(stored_solutions[0])scanf1_solution = solution_state.solver.eval(stored_solutions[1])print("[+] Success! Solution is: {0} {1}".format(scanf0_solution,scanf1_solution))else:raise Exception('Could not find the solution')angr_process()

globals

这里的关键我们都知道Python的变量生存周期，在这里scanf0和scanf1是函数ReplacementScanf的局部变量，为了让函数外部也能获得我们输入的符号位向量，从而调用求解器获得答案，需要将这两个符号位向量变为全局变量，这里我们需要调用带有全局状态的globals插件中“保存”对我们的符号值的引用。globals插件允许使用列表，元组或多个键的字典来存储多个位向量

self.state.globals['solutions'] = (scanf0, scanf1)

angr_veritesting

前面两节我们分别学习了应对路径爆炸的两种方法——手动约束和hook，这一节我们来学习有效缓解路径爆炸的第三种方法——Veritesting。

Veritesting意为路径归并，出自2014年的一篇论文Enhancing Symbolic Execution with Veritesting，读者对归并的原理感兴趣的话可以阅读一下。

12_angr_veritesting

angr中实现了上述论文中提到的Veritesting技术，我们只需要在构建simgr的时候添加一个veritesting=True参数即可，代码如下：

simgr = proj.factory.simgr(state, veritesting=True)

这次使用veritesting缓解路径爆炸：

import angrproj = angr.Project('../dist/12_angr_veritesting')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state, veritesting=True)
# simgr = proj.factory.simgr(state)
# simgr.use_technique(angr.exploration_techniques.Veritesting())
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))

另外根据官方的说法：

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

13_angr_static_binary

通常，Angr会自动地用工作速度快得多的simprocedure代替标准库函数，但是这题中库函数都已经因为静态编译成了静态函数了，angr没法自动替换。要解决这题，需要手动Hook所有使用标准库的C函数，angr已经在simprocedure中为我们提供了这些静态函数, 这里列举一些常用的函数

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代码：

import angrproj = angr.Project('../dist/13_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))

这题解题真正需要用的函数也就printf，scnaf，puts，即完成了angr需要的输出、输入、路径选择的功能，我们手动找到这几个函数的地址

这里比较容易忽略的一个函数就是__libc_start_main

让我们回忆一下在linux下一个c程序是如何启动的：

1. execve 开始执行
2. execve 内部会把bin程序加载后，就把.interp指定的 动态加载器加载
3. 动态加载器把需要加载的so都加载起来，特别的把 libc.so.6 加载
4. 调用到libc.so.6里的__libc_start_main函数，真正开始执行程序
5. libc_start_main做了一些事后，调用到main()函数

所以程序是一定需要用到__libc_start_main，分析后得到地址：0x8048D10，于是得到代码：

project.hook(0x804ed40, angr.SIM_PROCEDURES['libc']['printf']())
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']())

14_angr_shared_library

接下来我们通过这题来了解如何对动态链接库中单个的函数进行符号执行，main函数的代码如下：

其中validate函数是动态链接库lib14_angr_shared_library.so的函数：

我们可以直接通过call_state创建一个函数调用的初始状态：

state = proj.factory.call_state(validate_addr, password, length)

angr代码：

import angr
import claripyproj = angr.Project('lib14_angr_shared_library.so', load_options={'main_opts' : {'base_addr' : 0x400000}
})
# 这是validate的参数char* s1,地址设为0x3000000
buffer_pointer = claripy.BVV(0x3000000, 32)
# 这是validate的参数length
length = claripy.BVV(8, 32)
# 这是validate函数地址
validate_addr = 0x4006D7
# 参数char* s1 存放的字符串内容地址
password = claripy.BVS('password', 8 * 8)state = proj.factory.call_state(validate_addr, buffer_pointer, length)
state.memory.store(buffer_pointer, password)simgr = proj.factory.simgr(state)
simgr.explore(find=0x400783)
found = simgr.found[0]
found.solver.add(found.regs.eax == 1)
print(found.solver.eval(password, cast_to=bytes))

动态链接库都是地址无关的可执行文件（position-independent executable，PIE），若不手动指定PIE的基质，angr会将符号执行的基址指定为默认的0x400000，并输出：

WARNING | 2021-10-07 00:15:28,674 | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.

当然也可以自行指定基址，方法如下：

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

re-binary 选项

如果你想要对一个特定的二进制对象设置一些选项，CLE也能满足你的需求在加载二进制文件时可以设置特定的参数，使用 main_opts 和 lib_opts 参数进行设置。

• backend - 指定 backend
• base_addr - 指定基址
• entry_point - 指定入口点
• arch - 指定架构

示例如下：

>>> angr.Project('examples/fauxware/fauxware', main_opts={'backend': 'blob', 'arch': 'i386'}, lib_opts={'libc.so.6': {'backend': 'elf'}})
<Project examples/fauxware/fauxware>

参数main_opts和lib_opts接收一个以python字典形式存储的选项组。main_opts接收一个形如{选项名1：选项值1，选项名2：选项值2……}的字典，而lib_opts接收一个库名到形如{选项名1:选项值1，选项名2:选项值2……}的字典的映射。

lib_opts是二级字典，原因是一个二进制文件可能加载多个库，而main_opts指定的是主程序加载参数，而主程序一般只有一个，因此是一级字典。

这些选项的内容因不同的后台而异，下面是一些通用的选项：

• backend —— 使用哪个后台，可以是一个对象，也可以是一个名字(字符串)
• custom_base_addr —— 使用的基地址
• custom_entry_point —— 使用的入口点
• custom_arch —— 使用的处理器体系结构的名字

angr_overflow

这是angr_ctf系列的最后一节，在这一节我们通过三个栈溢出的例子来学习angr在漏洞挖掘方向的简单应用。

15_angr_arbitrary_read

该题是通过puts输出的，所以我们可以将判断输出中是否包含"Good Job."的条件改为，puts的参数是否为"Good Job."的地址，即0x484F4A47。检测puts参数的代码如下，很好理解：

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):# 如果puts的参数符号化了，说明v4的输入溢出到puts的参数了good_job_string_address = 0x484F4A47# 现在添加约束，要求溢出的数据跟goodjob字符串地址相同is_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 False

angr代码：

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 = 0x484F4A47is_vulnerable_expression = puts_parameter == good_job_string_addresscopied_state = state.copy()copied_state.add_constraints(is_vulnerable_expression)# 添加约束if copied_state.satisfiable():# satisfiable:是否满足state约束条件state.add_constraints(is_vulnerable_expression)return Truereturn Falsedef is_successful(state):puts_address = 0x08048370if state.addr == puts_address:#此时要去执行puts，但未进入puts，所以esp+4就是puts的参数return check_puts(state)return Falseproj = angr.Project('15_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))

16_angr_arbitrary_write

在这题中我们可以通过scanf将dest覆盖成任意地址，然后通过第二个strncpy向dest中保存的地址写入任何数据，因此我们可以向任何地址写入任何数据，这是一个任意写漏洞。首先我们将dest覆盖成password_buffer的地址，然后再通过第二个strncpy往dest中写入"PASSWORD"，最后输出"Good Job.“：

还是按照上题的思路，这回我们要check的是strncpy函数，约束条件为dest指向的地址为password_buffer，并且src为"NDYNWEUJ”。
angr代码：

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):# 输入的内容符号化，并且溢出到目的地址is_vulnerable_expression = claripy.And(src_content == b'NDYNWEUJ', dest == 0x57584344)# 约束要求输入字符串为'NDYNWEUJ'，并且将dest改为了password_buffer的地址copied_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):strncpy_address = 0x08048410if state.addr == strncpy_address:return check_strncpy(state)return Falseproj = angr.Project('16_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))

17_angr_arbitrary_jump

非常经典的ROP，可以覆盖返回值实现任意跳转



当一条指令有太多可能的分支时，就会出现无约束状态。当指令指针完全是符号指针时，就会发生这种情况，这意味着用户输入可以控制计算机执行的代码的地址

mov user_input, eax
jmp eax

例如此题存在的栈溢出漏洞就可以让我们的程序进入无约束状态。一般情况下，当Angr遇到不受约束的状态时，它会将其抛出。在我们的例子中，我们希望利用无约束状态来跳转到我们选择的位置。我们将在稍后了解如何禁用Angr的默认行为。

求解步骤：

• 初始化proj，让 angr 记录不受约束的状态
• 开始step直到发现 eip 为符号的状态
• 约束 eip 与 print_good 函数地址相同
• 约束求解

angr代码：

import angr
import claripy
import sysdef Go():path_to_binary = "./17_angr_arbitrary_jump" project = angr.Project(path_to_binary)initial_state = project.factory.entry_state() class ReplacementScanf(angr.SimProcedure):def run(self, format_string, input_buffer_address):input_buffer = claripy.BVS('input_buffer', 64 * 8)  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_bufferscanf_symbol = '__isoc99_scanf'project.hook_symbol(scanf_symbol, ReplacementScanf())simulation = project.factory.simgr(initial_state, save_unconstrained=True,stashes={'active' : [initial_state],'unconstrained' : [],'found' : [],'not_needed' : []})def check_vulnerable(state):return state.solver.symbolic(state.regs.eip)def has_found_solution():return simulation.founddef has_unconstrained_to_check():return simulation.unconstraineddef has_active():return simulation.activewhile (has_active() or has_unconstrained_to_check()) and (not has_found_solution()):for unconstrained_state in simulation.unconstrained:def should_move(s):return s is unconstrained_statesimulation.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 == 0x4d4c4749)solution = solution_state.solver.eval(solution_state.globals['solution'], cast_to=bytes)print(solution[::-1])else:raise Exception('Could not find the solution')if __name__ == '__main__':Go()

17真不太懂