符号执行学习

参考

jakespringer/angr_ctf
ZERO-A-ONE/AngrCTF_FITM: Angr CTF From introduction to mastery

概念

一个具有动态符号执行和静态分析的二进制分析工具，帮助我们自动化地分析和探索二进制文件中的执行路径。

原理：
    符号：符号是代表一组可能值的抽象。例如，一个符号 x 可能代表任意整数。
    路径约束：在执行过程中，程序的控制流会根据条件分支创建不同的执行路径。符号执行会收集这些条件分支的约束，形成路径约束。

执行过程：
    初始化：符号执行开始时，程序输入（如函数参数、全局变量等）被赋予符号值。
    执行：程序按照正常流程执行，但所有操作都是对符号值进行的。
    路径探索：在遇到条件分支时，符号执行会探索所有可能的路径。对于每个分支，它都会假设条件为真和假，并分别记录下相应的路径约束。
    约束求解：符号执行完成后，分析人员可以对这些路径约束进行求解，以找到满足特定路径的具体输入值。

使用 Angr 的步骤可以分为：

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

# 1、创建 project（二进制文件对象）
	# factory 属性，它提供了一些便捷的接口来创建符号执行的初始状态、模拟管理器等
	project = angr.Project(path_to_binary)

# 2、设置 state（记录某一时刻程序执行的状态包括内存、寄存器、堆栈等，类似快照）
	initial_state = project.factory.entry_state()  # 程序入口点
	initial_state = project.factory.blank_state(addr=0x400560)  # 从指定地址开始执行

# 3、设置符号量BVS
	# 命令行参数，project.factory.entry_state(args=["./filename", argv1])
	argv1 = claripy.BVS("argv1", 100 * 8)
	# 寄存器
	passwd_size_in_bits = 32  # 根据寄存器位数
	passwd0 = claripy.BVS('passwd0', passwd_size_in_bits)

# 4、把符号量设置到内存或者其他地方
	# 设置到寄存器
	initial_state.regs.eax = passwd0

# 4、设置 Simulation Managers （用于管理符号执行过程，帮助我们控制和探索程序的多个执行路径。）
	# 方法（explore、filter、step、drop等）
	# 属性（found、active、deadended等）
	simulation = project.factory.simgr(initial_state)

# 5、探索满足路径需要的值
	# 参数值可以是 单个或多个地址也可以是条件函数
	simulation.explore(find=find_condition, avoid=avoid_condition)

# 6、获取执行结果
	# 补充：标准输入、标准输出和标准错误 分别用（0、1、2表示）
	# 一般
	if simulation.found:
        solution_state = simulation.found[0]  # 获取通过 explore 找到符合条件的状态
        solution = solution_state.posix.dumps(0)  # 或 sys.stdin.fileno() 替换 0
	# 求解符号向量
	if simulation.found:
        solution_state = simulation.found[0]  # 获取通过 explore 找到符合条件的状态
        passwodr1 = solution_state.solver.eval(argv1) # 解析符号向量

例题（网鼎 vm）

起始找寻位置,我们可以选main, 也可以选特定验证函数, 但是需要注意的是, 数据的找寻
需要到达的路径为: success, flag这种成功的路径
避免走的路径便为失败路径
所以我们需要在ida找着三条路.
起初我选了vm_operate这个函数作为起始找寻位置,但是没有成功, 后面我选了main函数
需要到达的路径便为输出flag处
避免走的路径则是exit这种

import angr  # 导入angr库，angr是一个用于符号执行的强大框架

p = angr.Project('./signal.exe')  # 创建一个angr项目，加载指定的可执行文件'signal.exe'

state = p.factory.entry_state()  # 创建一个初始状态，即程序的入口点状态

simgr = p.factory.simgr(state)  # 创建一个SimulationManager对象，用于管理模拟执行的状态

# 使用SimulationManager的explore方法探索程序执行路径
# find参数指定了要寻找的目标地址，这里是0x004017A5
# avoid参数指定了要避免到达的地址，这里是0x004016E6
simgr.explore(find=0x004017A5, avoid=0x004016E6)

# simgr.found包含了所有到达find地址的状态列表
# 从列表中取出第一个找到的状态，并获取该状态的文件描述符0（通常是标准输入）的输出内容
flag = simgr.found[0].posix.dumps(0)[:15]  # 取前15个字符，可能是因为flag的长度是15

print(flag)  # 打印找到的flag