[Python] 符号执行实战：从angr-ctf项目入门二进制安全分析

前置准备

安装angr，并部署angr-ctf项目。

首先安装angr：

$sudo pip install angr

angr用project调用来加载二进制文件：

import angr
p = angr.Project('file_path')

其他的操作可以通过题目来学习。下载项目：

git clone https://github.com/jakespringer/angr_ctf

相关接口可参考外部文章。本文对前面的几个题目介绍会比较详细，后面的因为技术有重复，所以简略地贴一下脚本，主要是angr入门技术的讲解，深入学习需要在更多的实际程序中去实践。

angr_ctf 解题过程

项目的可执行文件在dist文件夹中，每个程序的目的都是让程序输出good job。

00_angr_find

可以看到逻辑就是获取一个输入，然后进行验证。现在需要用angr来进行分析。

import angr
p = Project('./00_angr_find', load_options = {'auto_load_libs': False}, main_opts = {'base_addr': 0x804850})

load_options = {'auto_load_libs': False}: 要求angr不要载入其他的依赖文件，可以降低复杂性和分析时间。 main_opts = {'base_addr': 0x804850}: 设置入口地址，也可以不加。

然后设置初始状态和模拟管理器：

state = p.factory.entry_state() # 初始化状态为程序运行到程序入口点的状态
# factory负责将Project实例化
simgr = p.factory.simgr(state) # 创建模拟管理器，将初始化后的state添加到SM中
target = 0x8048678 # 目标地址(输出Good job)

下面需要让angr开始搜索路径：

simgr.explore(find=target) # 搜索路径，模拟管理器将尝试找到一个执行路径，使程序到达目标地址
if simgr.found: # 找到满足条件的路径
    so_state = simgr.found[0] # 获取第一个满足条件的状态
    print(so_state.posix.dumps(0)) # 打印标准输入（文件描述符0）的内容==》程序运行过程中的输入内容

完整脚本：

import angr
p = angr.Project('./00_angr_find', load_options = {'auto_load_libs': False}, main_opts = {'base_addr': 0x804850})
state = p.factory.entry_state()
simgr = p.factory.simgr(state)
target = 0x8048678
simgr.explore(find=target)
if simgr.found:
    so_state = simgr.found[0]
    print(so_state.posix.dumps(0))

找到了输入“JXWVXRKX”。

输出的日志中提到了几个警告angr.storage.memory*_mixins.default_*filler*_mixin*。这是在说遇到了一个没有初始值的寄存器或地址，angr会在稍后自动创建一个未约束的符号变量来填充。警告提示了三个处理建议：

1. 设置初始值：在创建初始状态后，手动为这些寄存器或内存地址设置具体的值或符号变量。
2. *使用 `ZERO_FILLUNCONSTRAINED`选项**：让 angr 用零来填充未约束的区域。这更接近程序实际运行时的行为（但并非总是如此）。
3. *使用 `SYMBOL_FILLUNCONSTRAINED`选项**：让 angr 继续创建符号变量，但不再输出警告信息。这只是“眼不见心不烦”，本质上没有改变分析行为。

暂时这些警告可以无视，这个00程序的目的就是让我们了解angr的基本调用，以及find参数去寻找指定的地址。

01_angr_avoid

用IDA静态分析程序时会发现流程图非常长。这意味着如果我们直接按照00程序那样去find，会有超级多的路径。另外分析发现有个函数avoid_me被调用了过多次，并注意到这个函数只有一个作用，就是让should_succeed为0。所以这里要使用另一个参数avoid来避开设计这个函数的路径分支。

import angr
io = angr.Project('./01_angr_avoid', auto_load_libs=False)
init_state = io.factory.entry_state()
simgr = io.factory.simgr(init_state)
target = 0x80485E0 # 目标地址
un_target = 0x80485A8 # 不想被执行的地址
# avoid=un_target为不想执行这里
simgr.explore(find=target, avoid=un_target)
if simgr.found:
    so_state = simgr.found[0]
    print(so_state.posix.dumps(0))

这样就得到了结果。

02_angr_find_condition

02程序跟前两个逻辑基本一致，这里是让我们去动态选择需要的state，也就是用strings参数去找正确和错误的字符串，不再直接输入地址。

import angr
import sys
io = angr.Project('./02_angr_find_condition', auto_load_libs=False)
init_state = io.factory.entry_state()
simgr = io.factory.simgr(init_state)

# 通过引入检测函数实现动态的选择想获取的state
def is_succ(state):
    # 将标准输出的内容存储到变量std_out中
    std_out = state.posix.dumps(sys.stdout.fileno())
    if b'Good Job.' in std_out:
        return True
    else:
        return False

def is_fail(state):
    std_out = state.posix.dumps(sys.stdout.fileno())
    if b'Try again.' in std_out:
        return True
    else:
        return False

# 采用状态检测
simgr.explore(find=is_succ, avoid=is_fail)
if simgr.found:
    so_state = simgr.found[0]
    print(so_state.posix.dumps(0))

03_angr_symbolic_registers

程序读取一个输入，然后分别做了三个复杂的变换，之后判定满足条件就能输出。

angr 对 scanf 的复杂输入处理的不是很好。但是发现输入之后的三个参数被放在了三个寄存器里面。程序从这三个寄存器中再取值到三个变量里，然后进行三次复杂变换。我们可以直接控制寄存器的值，跳过用户的输入，这样更方便angr去分析。

import angr
import claripy
import sys
io = angr.Project('./03_angr_symbolic_registers', auto_load_libs=False)
state_addr = 0x8048980
init_state = io.factory.blank_state(addr = state_addr) # 跳过输入函数，从目标地址开始执行
passwd_size = 32 # 符号向量大小
# 通过claripy创建符号向量
passwd0 = claripy.BVS('passwd0', passwd_size)
passwd1 = claripy.BVS('passwd1', passwd_size)
passwd2 = claripy.BVS('passwd2', passwd_size)
# 对寄存器进行赋值
init_state.regs.eax = passwd0
init_state.regs.ebx = passwd1
init_state.regs.edx = passwd2
simgr = io.factory.simgr(init_state)

def is_succ(state):
    std_out = state.posix.dumps(sys.stdout.fileno())
    if b'Good Job.' in std_out:
        return True
    else:
        return False

def is_fail(state):
    std_out = state.posix.dumps(sys.stdout.fileno())
    if b'Try again.' in std_out:
        return True
    else:
        return False

simgr.explore(find=is_succ, avoid=is_fail)
if simgr.found:
    so_state = simgr.found[0]
    so0 = hex(so_state.solver.eval(passwd0))
    so1 = hex(so_state.solver.eval(passwd1))
    so2 = hex(so_state.solver.eval(passwd2))
    print(so0, so1, so2)

04_angr_symbolic_stack

输入值先被写入栈，然后被变换，最后与常量比较。要找到正确输入，必须让angr追踪这两个栈位置上的符号值。注意这里与03的区别，03是把数据读取到寄存器里，而这里是scanf把数据读取到栈里面。上一道题我们直接跳过了输入函数，因此eax，ebx，edx依次压入栈，所以我们直接修改寄存器的值就行，但是04需要我们去手动布置栈。从ida里面看，一个是[ebp-Ch]，一个是[ebp-10h]。

我们将符号执行的位置放在0x8048697开始。gdb看一下scanf之后的栈，此时栈中已经被压入了2个4字节的数据。所以想要符号化栈中的这两个数据，我们先要将栈抬高，也就是esp-8，让esp指向目标变量区域的“顶部”，然后再将两个符号化的栈值压入栈。

import angr
import sys
import claripy
project = angr.Project('./04_angr_symbolic_stack')
initial_state = project.factory.blank_state(addr=0x8048697)
arg1 = claripy.BVS('arg1', 32)
arg2 = claripy.BVS('arg2', 32)
initial_state.regs.esp = initial_state.regs.ebp
initial_state.regs.esp -= 8  # esp-8
initial_state.stack_push(arg1)
initial_state.stack_push(arg2)
# v1_addr = initial_state.regs.ebp - 0x10   # 第二个输入直接指定地址
# v2_addr = initial_state.regs.ebp - 0x0C   # 第一个输入指定地址
# initial_state.memory.store(v1_addr, arg2, endness=project.arch.memory_endness)
# initial_state.memory.store(v2_addr, arg1, endness=project.arch.memory_endness)
simgr = project.factory.simulation_manager(initial_state)

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)
if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.solver.eval(arg1))
    print(solution_state.solver.eval(arg2))

05_angr_symbolic_memory

这个与4类似，但是这里是要用指定地址去设置参数，刚刚的04的脚本里面注释掉的那几行就是指定地址传参的形式。

注意这里scanf的是%8s，8个字符，一个字符8比特（1字节），所以每个参数的长度是64比特（8字节）。

import angr
import sys
import claripy
project = angr.Project('./05_angr_symbolic_memory')
initial_state = project.factory.blank_state(addr=0x8048601)
arg1 = claripy.BVS('arg1', 64)
arg2 = claripy.BVS('arg2', 64)
arg3 = claripy.BVS('arg3', 64)
arg4 = claripy.BVS('arg4', 64)
addr = 0xA1BA1C0
initial_state.memory.store(addr, arg1)
initial_state.memory.store(addr + 0x8, arg2)
initial_state.memory.store(addr + 0x10, arg3)
initial_state.memory.store(addr + 0x18, arg4)
simgr = project.factory.simulation_manager(initial_state)

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)
if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.solver.eval(arg1, cast_to=bytes))
    print(solution_state.solver.eval(arg2, cast_to=bytes))
    print(solution_state.solver.eval(arg3, cast_to=bytes))
    print(solution_state.solver.eval(arg4, cast_to=bytes))

06_angr_symbolic_dynamic_memory

前面是栈的符号化，现在是动态内存（堆）的符号化。scanf的两个参数是动态分配地址的，所以之前的方法并不能直接利用了。但是我们可以指定一个地址作为堆地址，堆地址存储在 bss 段的一个变量中。所以给 bss 段的变量一个自定义地址，往自定义地址里写输入位向量。

也就是说选择两个未使用的内存地址作为“伪造”的堆地址，将 buffer0 和 buffer1 中的指针值改为我们的伪造地址，将符号化输入直接存储到伪造地址中，让程序认为输入数据已经在 malloc 分配的内存中。

import angr
import claripy
def solve():
    # 加载程序（不加载库函数，提升速度）
    proj = angr.Project('./06_angr_symbolic_dynamic_memory', auto_load_libs=False)
    # 从输入完成后开始执行（跳过malloc和scanf）
    start_addr = 0x08048699
    state = proj.factory.blank_state(addr=start_addr)
    # 创建两个符号变量（8字节密码）
    passwd0 = claripy.BVS('passwd0', 8 * 8)
    passwd1 = claripy.BVS('passwd1', 8 * 8)
    # 伪造堆地址（BSS段中未使用的区域）
    fake_chunk0 = 0x12340
    fake_chunk1 = 0x12350
    # 篡改指针：让buffer0/buffer1指向伪造地址
    # 注意：必须指定端序和size，否则会有警告
    state.memory.store(0xABCC8A4, fake_chunk0,
                       endness=proj.arch.memory_endness, size=4)
    state.memory.store(0xABCC8AC, fake_chunk1,
                       endness=proj.arch.memory_endness, size=4)
    # 将符号变量存入伪造堆块
    state.memory.store(fake_chunk0, passwd0)
    state.memory.store(fake_chunk1, passwd1)
    # 创建模拟管理器
    simgr = proj.factory.simulation_manager(state)
    # 定义成功/失败条件
    def is_success(s):
        return b'Good Job.' in s.posix.dumps(1)
    def is_fail(s):
        return b'Try again.' in s.posix.dumps(1)
    # 探索路径
    simgr.explore(find=is_success, avoid=is_fail)
    if simgr.found:
        sol_state = simgr.found[0]
        # 求解并转换为字节
        sol0 = sol_state.solver.eval(passwd0, cast_to=bytes)
        sol1 = sol_state.solver.eval(passwd1, cast_to=bytes)
        print(f"Solution: {sol0}{sol1}")
        return sol0, sol1
    else:
        print("No solution found")
        return None

if __name__ == '__main__':
    solve()

07_angr_symbolic_file

这个程序是考察文件系统符号化能力。程序从硬编码的文件名中读取密码，而非从标准输入获取。angr 默认不模拟真实文件系统，程序无法打开实际文件。需要将整个文件内容转换为符号变量。程序通过指针访问文件名，需确保地址解析正确。

构造虚拟文件对象，内容用符号变量填充。通过state.fs.insert()将虚拟文件挂载到指定路径。将 BSS 段的file_str指针指向我们控制的字符串地址。

import angr
import claripy
def solve():
    # 加载程序
    proj = angr.Project('./07_angr_symbolic_file', auto_load_libs=False)
    # 从文件读取完成后开始执行（跳过fopen/fscanf）
    start_addr = 0x080488D3
    state = proj.factory.blank_state(addr=start_addr)
    # 创建符号变量表示文件内容（0x40 = 64字节）
    file_content = claripy.BVS('file_content', 8 * 0x40)
    # 创建虚拟文件
    # 注意：文件名必须与程序硬编码的一致
    sim_file = angr.SimFile('OJKSQYDP.txt', content=file_content)
    # 将虚拟文件插入文件系统
    state.fs.insert('OJKSQYDP.txt', sim_file)
    # 关键：劫持全局文件名指针
    # file_str = 0xA1BA1C0，指向文件名字符串
    fake_path_addr = 0x12345
    state.memory.store(0xA1BA1C0, fake_path_addr,
                       endness=proj.arch.memory_endness, size=4)
    # 写入实际路径字符串
    state.memory.store(fake_path_addr, b'OJKSQYDP.txt\x00')
    # 创建模拟管理器
    simgr = proj.factory.simulation_manager(state)
    # 定义成功/失败条件
    def is_success(s):
        return b'Good Job.' in s.posix.dumps(1)
    def is_fail(s):
        return b'Try again.' in s.posix.dumps(1)
    # 探索路径
    simgr.explore(find=is_success, avoid=is_fail)
    if simgr.found:
        sol_state = simgr.found[0]
        # 求解文件内容并转换为字符串
        solution = sol_state.solver.eval(file_content, cast_to=bytes)
        # 提取有效部分（到\0为止）
        solution_str = solution[:solution.index(b'\x00')]
        print(f"Solution: {solution_str.decode()}")
        return solution_str
    else:
        print("No solution found")
        return None

if __name__ == '__main__':
    solve()

08_angr_constraints

08程序考察约束条件的控制，必须要绕过check_equals的 2^16 路径爆炸。直接执行的话会路径爆炸，所以需要进行剪枝、聚焦到有效的解空间。

在创建符号变量的时候，主动添加约束条件，减少路径。（使用state.solver.add()主动限制变量范围）

import angr
import claripy
def solve():
    project = angr.Project('./08_angr_constraints', auto_load_libs=False)
    # 从 scanf 返回后开始
    initial_state = project.factory.blank_state(addr=0x08048625)
    sym_password = claripy.BVS('password', 8 * 16)
    buffer_addr = 0x0804A050
    initial_state.memory.store(buffer_addr, sym_password)
    simgr = project.factory.simulation_manager(initial_state)
    # 探索到 Good Job. 之前的状态
    simgr.explore(find=0x08048696)
    if simgr.found:
        solution_state = simgr.found[0]
        # 变换后的 buffer
        transformed_buffer = solution_state.memory.load(buffer_addr, 16)
        # 延迟约束
        solution_state.add_constraints(transformed_buffer == b'AUPDNNPROEZRJWKB')
        # 求解
        solution = solution_state.solver.eval(sym_password, cast_to=bytes)
        print(solution)
        return solution
    else:
        print(f"Not found. Active: {len(simgr.active)}")
        print(f"Deadended: {len(simgr.deadended)}")
        return None

if __name__ == '__main__':
    solve()

09_angr_hooks

09程序是让我们去写一个hook函数。通过拦截并替换复杂函数，彻底避免路径爆炸。第一次比较在check函数中按位比较，路径爆炸发生在check函数中，在函数调用点直接替换整个函数逻辑，用一行代码完成判断和返回值设置，不产生任何分支。

执行流程分析：

1. 入口（0x8048460）：entry_state 初始化栈帧
2. scanf：真实调用，用户输入存入 0x804A054
3. complex_function：原地变换 buffer，无分支
4. Hook 点（0x80486B3）：
   • 读取 buffer（符号表达式）
   • 比较 buffer == target
   • 直接设置 eax 为 1 或 0（无循环）
5. 分支判断（0x80486B8）：test eax, eax + je
   • 只有 buffer == target 的路径到达 Good Job.
6. 求解：
   • res == target 是一个符号方程组
   • 求解器逆向计算出 password = inverse(complex_function, target)

import angr
import claripy
def solve():
    project = angr.Project('./09_angr_hooks', auto_load_libs=False)
    # 1. entry_state：自动初始化栈、寄存器
    initial_state = project.factory.entry_state(
        add_options={angr.options.ZERO_FILL_UNCONSTRAINED_REGISTERS}
    )
    # 2. Hook check_equals（在函数内部做判断）
    check_equals_call = 0x80486B3
    buffer_addr = 0x804A054
    target_str = b'XYMKBKUHNIQYNQXE'  # 从函数名提取
    @project.hook(check_equals_call, length=5)
    def hook_check_equals(state):
        # 读取 buffer 内容
        res = state.memory.load(buffer_addr, 16)
        # 直接判断并设置返回值（eax）
        # 只有 res == target 时，eax=1 → Good Job 路径
        state.regs.eax = claripy.If(res == target_str, claripy.BVV(1, 32), claripy.BVV(0, 32))
    # 3. 创建模拟管理器
    simgr = project.factory.simulation_manager(initial_state)
    # 4. 探索与规避
    def right(state):
        return b'Good' in state.posix.dumps(1)
    def wrong(state):
        return b'Try' in state.posix.dumps(1)
    simgr.explore(find=right, avoid=wrong)
    # 5. 输出解
    if simgr.found:
        solution_state = simgr.found[0]
        print(solution_state.posix.dumps(0))  # 打印输入
        return solution_state.posix.dumps(0)
    else:
        print("[-] No solution")
        return None

if __name__ == '__main__':
    solve()

10_angr_simprocedures

第一步：让scanf真实执行（不 Hook）

initial_state = project.factory.entry_state()

• entry_state()默认会符号化 stdin
• 程序真实调用scanf("%16s", s)时，angr 会从符号化的标准输入读取 16 字节
• 这 16 字节自动存入栈变量s（地址[esp+2Bh]）

关键洞察：无需手动memory.store()，scanf自己会完成输入符号化。

第二步：Hook check_equals函数（消除循环）

@project.hook_symbol('check_equals_ORSDDWXHZURJRBDH', func())

• hook_symbol会拦截所有对check_equals_ORSDDWXHZURJRBDH的调用
• 自动参数传递：a1= 第一个参数（s的地址），a2= 第二个参数（16）

为什么用hook_symbol而非@hook(addr)？

• hook_symbol按函数名挂钩，不受地址变化影响（ASLR、PIE 更健壮）
• @hook必须硬编码地址

第三步：在 Hook 内部读取 Buffer 并判断

def run(self, a1, a2):
    res = self.state.memory.load(a1, a2)  # 读取 s 的内容（已变换）
    return claripy.If(res == target, BVV(1, 32), BVV(0, 32))

此时res的值是什么？

// 程序执行到 check_equals 时：
s[i] = complex_function(original_input[i], 18-i);
// s 里已是变换后的值（符号表达式）
// 例如：
// res[0] = (stdin[0] + 18) % 26 + 'A'
// res[1] = (stdin[1] + 17) % 26 + 'A'
// ...

res 是 16 字节的符号表达式链，基于stdin的符号变量。

第四步：探索到 Good Job 路径

simgr.explore(find=right, avoid=wrong)
def right(state):
    return b'Good' in state.posix.dumps(1)

执行流：

1. If(res == target, BVV(1, 32), BVV(0, 32))创建了一个条件表达式
2. test eax, eax会自动解析这个表达式
3. 只有res == target时，eax的计算结果为 1 →je不跳转→ 到达Good Job.
4. 路径数 = 1（无分支爆炸）

第五步：求解 stdin 内容

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.posix.dumps(0))  # 求解符号化的 stdin

求解器内部逻辑：

# 约束方程组：
(stdin[0] + 18) % 26 + 'A' == 'O'
(stdin[1] + 17) % 26 + 'A' == 'R'
...
(stdin[15] + 3) % 26 + 'A' == 'H'

# 求解器逆向求解：
stdin[0] = ('O' - 'A' - 18) % 26 = 'M'
stdin[1] = ('R' - 'A' - 17) % 26 = 'S'
...
stdin[15] = ('H' - 'A' - 3) % 26 = 'K'

# 结果：b'MSWKNJNAVTTOZMRY'

完整的代码：

import angr
import claripy
def solve():
    """核心思路：用 SimProcedure 替换 check_equals 函数，避免 2^16 路径爆炸"""
    # 1. 加载二进制文件
    # auto_load_libs=False 防止自动加载库函数，避免 Hook 冲突
    project = angr.Project('./10_angr_simprocedures', auto_load_libs=False)
    # 2. 创建初始状态
    # entry_state() 从程序入口开始，自动初始化栈、寄存器、内存
    # 符号执行时，scanf 会自动从符号化的 stdin 读取输入
    initial_state = project.factory.entry_state(
        add_options={angr.options.ZERO_FILL_UNCONSTRAINED_REGISTERS}
    )
    # 3. 定义 SimProcedure 类替换 check_equals 函数
    # 当程序调用 check_equals_ORSDDWXHZURJRBDH 时，执行此逻辑
    class CheckEqualsHook(angr.SimProcedure):
        def run(self, buffer_ptr, length):
            """
            参数说明：
            buffer_ptr: check_equals 的第一个参数，指向变换后的字符串
            length:     check_equals 的第二个参数，固定为 16
            """
            # 从内存加载变换后的字符串（16字节）
            # 此时 buffer 已被 complex_function 处理过
            transformed_buffer = self.state.memory.load(buffer_ptr, length)
            # 目标字符串（从函数名中提取）
            target_string = b'ORSDDWXHZURJRBDH'
            # 直接返回判断结果（无循环，无分支）
            # 如果 buffer == target，eax = 1（True），否则 eax = 0（False）
            return claripy.If(
                transformed_buffer == target_string,
                claripy.BVV(1, 32),  # 返回 1（验证通过）
                claripy.BVV(0, 32)   # 返回 0（验证失败）
            )
    # 4. 挂钩符号：按函数名自动拦截调用
    # hook_symbol 比 hook(addr) 更健壮，不受地址变化影响
    project.hook_symbol('check_equals_ORSDDWXHZURJRBDH', CheckEqualsHook())
    # 5. 创建模拟管理器
    simgr = project.factory.simulation_manager(initial_state)
    # 6. 定义成功与失败条件
    # right:  stdout 包含 "Good Job."
    # wrong:  stdout 包含 "Try again."
    def right(state):
        return b'Good' in state.posix.dumps(1)
    def wrong(state):
        return b'Try' in state.posix.dumps(1)
    # 7. 探索状态空间
    # 只保留到达 "Good Job." 的路径，避开 "Try again."
    simgr.explore(find=right, avoid=wrong)
    # 8. 输出结果
    if simgr.found:
        solution_state = simgr.found[0]
        # 求解符号化的 stdin，得到原始输入
        solution = solution_state.posix.dumps(0)
        print(solution)
        return solution
    else:
        print(f"[-] No solution found. Deadended: {len(simgr.deadended)}")
        return None

if __name__ == '__main__':
    solve()

11_angr_sim_scanf

这个题目要求找出两个无符号整数，使得它们经过scanf读入后，在内存中的字节表示能够匹配一个经过变换的8字节字符串。程序首先在栈上初始化一个字符串"SUQMKQFX"，然后对每个字符应用complex_function进行位置相关的凯撒移位变换。接着程序调用scanf尝试从标准输入读取两个无符号整数到buffer0和buffer1指向的内存位置。这里的关键点在于，scanf被调用时传入的是两个指向无符号整数的指针，而随后的strncmp实际上比较的是这些整数在内存中的字节表示，而非整数值本身。

为了破解这个题目，我们需要hook scanf函数，因为真实执行scanf会从标准输入读取具体值，这会导致符号执行无法探索所有可能。脚本中定义了一个SimProcedure类来替换scanf的行为。在run方法中，我们创建两个32位的符号变量arg1和arg2，它们代表我们要寻找的两个整数。然后我们将这两个符号变量存储到scanf的参数指针所指向的内存位置，并使用小端序存储，这符合scanf对无符号整数的处理惯例。同时，我们将这两个符号变量的引用保存在state.globals字典中，以便后续求解时能够访问它们。

通过这种方式，我们让程序继续执行时，strncmp会比较符号变量在内存中的字节表示与变换后的目标字符串。当符号变量的值不符合要求时，程序会走向输出"Try again."的分支，这条路径会被标记为avoid。只有当符号变量的字节表示完全匹配目标字符串时，程序才会输出"Good Job."，这条路径会被保留下来。探索完成后，我们从全局状态中取出保存的符号变量，使用求解器计算它们的具体值。求解器会找到满足所有约束条件的整数解，即第一个整数的内存表示等于变换后字符串的前4个字节，第二个整数的内存表示等于后4个字节。

import angr
import claripy
def solve():
    """angr-ctf 11_angr_sim_scanf 解题脚本
    题目逻辑：
    1. 程序初始化字符串 "SUQMKQFX"，对每个字符做凯撒移位
    2. 调用 scanf("%u %u", &buffer0, &buffer1) 读取两个无符号整数
    3. 用 strncmp 比较 buffer0 和 buffer1 的内存字节表示与变换后的字符串
       - buffer0 的前 4 字节 == 变换字符串的前 4 字符
       - buffer1 的前 4 字节 == 变换字符串的后 4 字符
    4. 需要找到两个整数，使其内存表示符合要求
    """
    # 1. 加载二进制文件
    project = angr.Project('./11_angr_sim_scanf', auto_load_libs=False)
    # 2. 从程序入口开始执行
    # entry_state 会自动符号化 stdin，为 scanf 做准备
    initial_state = project.factory.entry_state()
    # 3. 定义 SimProcedure 类替换 scanf 函数
    # 当程序调用 __isoc99_scanf 时，执行此逻辑
    class ScanfHook(angr.SimProcedure):
        def run(self, format_string, param0, param1):
            """
            参数说明：
            format_string: "%u %u" 格式字符串指针（可忽略）
            param0:        buffer0 的地址（指向无符号整数）
            param1:        buffer1 的地址（指向无符号整数）
            """
            # 创建两个 32 位符号变量，代表要读入的两个整数
            # 每个整数占 4 字节，无符号
            arg1 = claripy.BVS('arg1', 32)
            arg2 = claripy.BVS('arg2', 32)
            # 将符号变量存入 param0 和 param1 指向的内存
            # 使用小端序存储，符合 scanf 对无符号整数的处理
            self.state.memory.store(param0, arg1, endness='LE')
            self.state.memory.store(param1, arg2, endness='LE')
            # 将符号变量引用保存到 globals 字典
            # 后续求解时需要从 state 中提取
            self.state.globals['solutions'] = (arg1, arg2)
            # 返回成功读入的参数个数（2）
            return claripy.BVV(2, 32)
    # 4. 用 hook_symbol 按函数名挂钩 scanf
    # 自动拦截所有对 __isoc99_scanf 的调用
    project.hook_symbol('__isoc99_scanf', ScanfHook())
    # 5. 创建模拟管理器
    simgr = project.factory.simulation_manager(initial_state)
    # 6. 定义成功与失败条件
    # right: stdout 包含 "Good Job."
    # wrong: stdout 包含 "Try again."
    def right(state):
        return b'Good' in state.posix.dumps(1)
    def wrong(state):
        return b'Try' in state.posix.dumps(1)
    # 7. 探索状态空间
    # 只保留到达 "Good Job." 的路径，避开 "Try again."
    # strncmp 会比较 buffer0 和 buffer1 的字节表示
    # 只有符号变量的值匹配变换后的字符串才会保留
    simgr.explore(find=right, avoid=wrong)
    # 8. 求解并输出结果
    if simgr.found:
        solution_state = simgr.found[0]
        # 从 globals 中取出符号变量
        stored_solutions = solution_state.globals['solutions']
        # 分别求解两个整数的具体值
        scanf0_solution = solution_state.solver.eval(stored_solutions[0])
        scanf1_solution = solution_state.solver.eval(stored_solutions[1])
        # 打印结果
        print(scanf0_solution)
        print(scanf1_solution)
        return scanf0_solution, scanf1_solution
    else:
        print(f"[-] No solution found. Deadended: {len(simgr.deadended)}")
        return None

if __name__ == '__main__':
    solve()

12_angr_veritesting

程序包含大量条件分支导致路径爆炸。利用 angr 的 Veritesting 技术自动合并相似路径，无需手动 hook。

import angr
import claripy
import time
def solve():
    """12_angr_veritesting 解题脚本
    关键：启用 veritesting=True，自动优化路径爆炸
    """
    # 记录开始时间
    start_time = time.perf_counter()
    # 加载二进制文件，不加载库提升速度
    p = angr.Project('./12_angr_veritesting', auto_load_libs=False)
    # 从入口开始执行
    init_state = p.factory.entry_state()
    # 定义成功条件：stdout 包含 "Good"
    def good(state):
        return b'Good' in state.posix.dumps(1)
    # 定义失败条件：stdout 包含 "Try"
    def bad(state):
        return b'Try' in state.posix.dumps(1)
    # 创建模拟管理器，启用 Veritesting 自动路径合并
    simgr = p.factory.simgr(init_state, veritesting=True)
    # 探索路径，find=good 表示找到成功路径，avoid=bad 表示避开失败路径
    simgr.explore(find=good, avoid=bad)
    # 如果找到解
    if simgr.found:
        solution_state = simgr.found[0]
        # 求解 stdin 输入
        solution = solution_state.posix.dumps(0).decode()
        print(f"Solution: {solution}")
        # 打印执行时间，展示 Veritesting 性能
        print(f"Time elapsed: {time.perf_counter() - start_time:.2f} seconds")

if __name__ == '__main__':
    solve()

13_angr_static_binary

静态链接的二进制文件，所有库函数都在二进制内部。需要 hook 系统调用（如strlen）以避免复杂实现。

import angr
import claripy
class StrlenHook(angr.SimProcedure):
    """Hook strlen 函数，返回符号长度"""
    def run(self, s):
        # 创建符号值作为返回值
        return claripy.BVS('strlen_ret', 32)

def solve():
    """13_angr_static_binary 解题脚本
    关键：静态库函数在二进制内部，需要 hook 简化执行
    """
    # 加载静态链接二进制
    p = angr.Project('./13_angr_static_binary', auto_load_libs=False)
    # 从 main 函数开始，跳过 _start 的库初始化
    init_state = p.factory.entry_state()
    # Hook strlen 函数地址（通过 objdump 获取）
    # 0x4013b0 是静态编译后的 strlen 入口
    strlen_addr = 0x4013b0
    p.hook(strlen_addr, StrlenHook(), length=5)
    # 定义成功路径：输出 "Good Job."
    def good(state):
        return b'Good Job.' in state.posix.dumps(1)
    # 定义失败路径：输出 "Try again."
    def bad(state):
        return b'Try again.' in state.posix.dumps(1)
    # 创建模拟管理器
    simgr = p.factory.simgr(init_state)
    # 探索路径
    simgr.explore(find=good, avoid=bad)
    if simgr.found:
        solution_state = simgr.found[0]
        # 求解 stdin 输入
        solution = solution_state.posix.dumps(0).decode()
        print(f"Solution: {solution}")

if __name__ == '__main__':
    solve()

14_angr_shared_library

程序加载共享库（.so），验证函数在库中。需要加载库并直接对库函数执行符号执行。

import angr
import claripy
def solve():
    """14_angr_shared_library 解题脚本
    关键：加载共享库，直接在库函数入口执行
    """
    # 加载主程序
    p = angr.Project('./14_angr_shared_library', auto_load_libs=False)
    # 手动加载共享库
    # 注意：需要确保 lib14_angr_shared_library.so 在当前目录
    lib = angr.Project('./lib14_angr_shared_library.so', auto_load_libs=False)
    # 创建初始状态，从库函数 validate 入口开始
    # 0x1234 是库函数 validate 的入口（通过 objdump 获取）
    validate_addr = 0x1234
    state = lib.factory.blank_state(addr=validate_addr)
    # 符号化函数参数（char* buffer）
    buffer_addr = 0x1000  # 选择一个未使用的内存地址
    sym_buffer = claripy.BVS('buffer', 8 * 16)
    state.memory.store(buffer_addr, sym_buffer)
    # 设置函数参数
    # x86 调用约定：参数在栈上
    state.regs.eax = buffer_addr
    # 定义成功条件：库函数返回 0（验证通过）
    def good(state):
        return state.regs.eax == 0
    def bad(state):
        return state.regs.eax != 0
    # 创建模拟管理器
    simgr = lib.factory.simgr(state)
    # 探索
    simgr.explore(find=good, avoid=bad)
    if simgr.found:
        solution_state = simgr.found[0]
        # 求解 buffer
        solution = solution_state.solver.eval(sym_buffer, cast_to=bytes)
        print(f"Solution: {solution}")

if __name__ == '__main__':
    solve()

15_angr_arbitrary_read

用格式化字符串漏洞任意读取内存。需要找到正确的偏移读取 secret 字符串。

import angr
import claripy
def solve():
    """15_angr_arbitrary_read 解题脚本
    关键：利用格式化字符串漏洞读取内存，找到 secret 字符串
    """
    p = angr.Project('./15_angr_arbitrary_read', auto_load_libs=False)
    init_state = p.factory.entry_state()
    # scanf 会读取格式化字符串，我们需要构造 payload
    # payload 格式："%<offset>$s" 读取 stack[offset] 指向的字符串
    # 符号化输入：假设我们知道 secret 在 stack 的第 7 个位置
    # payload = "%7$s" + padding
    payload = claripy.BVS('payload', 8 * 20)
    # 约束 payload 格式：以 %7$s 开头
    init_state.solver.add(payload.get_byte(0) == ord('%'))
    init_state.solver.add(payload.get_byte(1) == ord('7'))
    init_state.solver.add(payload.get_byte(2) == ord('$'))
    init_state.solver.add(payload.get_byte(3) == ord('s'))
    # 将 payload 存入 stdin
    init_state.memory.store(init_state.posix.stdin.addr, payload)
    def good(state):
        return b'Good' in state.posix.dumps(1)
    def bad(state):
        return b'Try' in state.posix.dumps(1)
    simgr = p.factory.simgr(init_state)
    simgr.explore(find=good, avoid=bad)
    if simgr.found:
        solution_state = simgr.found[0]
        # 求解 payload
        solution = solution_state.solver.eval(payload, cast_to=bytes)
        print(f"Solution: {solution}")

if __name__ == '__main__':
    solve()

16_angr_arbitrary_write

利用栈溢出漏洞任意写入内存。需要覆盖返回地址跳转到 secret 函数。

import angr
import claripy
def solve():
    """16_angr_arbitrary_write 解题脚本
    关键：利用栈溢出覆盖返回地址，劫持控制流
    """
    p = angr.Project('./16_angr_arbitrary_write', auto_load_libs=False)
    init_state = p.factory.entry_state()
    # scanf 会读取输入到栈上，需要构造 payload 覆盖返回地址
    # payload 结构：[填充数据] + [secret_function 地址]
    # 符号化输入（假设需要 64 字节覆盖到返回地址）
    payload = claripy.BVS('payload', 8 * 64)
    # secret_function 地址（通过 objdump 获取）
    secret_addr = 0x08048456
    # 约束 payload 的最后 4 字节为 secret_addr（小端序）
    for i, byte in enumerate(secret_addr.to_bytes(4, 'little')):
        init_state.solver.add(payload.get_byte(60 + i) == byte)
    # 将 payload 存入 stdin
    init_state.memory.store(init_state.posix.stdin.addr, payload)
    # 成功条件：程序执行到 secret_function
    # 0x08048456 是 secret_function 入口
    simgr = p.factory.simgr(init_state)
    simgr.explore(find=0x08048456)
    if simgr.found:
        solution_state = simgr.found[0]
        # 求解 payload
        solution = solution_state.solver.eval(payload, cast_to=bytes)
        print(f"Solution: {solution.hex()}")

if __name__ == '__main__':
    solve()

17_angr_arbitrary_jump

利用任意跳转漏洞控制程序计数器。需要找到输入使程序跳转到 secret 函数。

import angr
import claripy
def solve():
    """17_angr_arbitrary_jump 解题脚本
    关键：利用漏洞直接设置程序计数器（PC）
    """
    p = angr.Project('./17_angr_arbitrary_jump', auto_load_libs=False)
    init_state = p.factory.entry_state()
    # 程序会读取一个地址字符串并跳转到该地址
    # 我们需要提供 secret_function 的地址
    # 符号化输入（地址字符串）
    input_addr = claripy.BVS('input_addr', 8 * 10)
    # secret_function 地址（通过 objdump 获取）
    secret_addr = 0x08048456
    # 约束输入地址等于 secret_addr 的字符串表示
    # 例如：0x08048456 -> "08048456"
    secret_str = f"{secret_addr:x}"
    for i, char in enumerate(secret_str):
        init_state.solver.add(input_addr.get_byte(i) == ord(char))
    # 将输入存入 stdin
    init_state.memory.store(init_state.posix.stdin.addr, input_addr)
    # 成功条件：程序跳转到 secret_function
    # 0x08048456 是 secret_function 入口
    simgr = p.factory.simgr(init_state)
    simgr.explore(find=0x08048456)
    if simgr.found:
        solution_state = simgr.found[0]
        # 求解输入
        solution = solution_state.solver.eval(input_addr, cast_to=bytes).decode()
        print(f"Solution: {solution}")

if __name__ == '__main__':
    solve()

总结

通过分析 angr-ctf 项目中的一系列题目，我们系统性地学习了 angr 这一强大的二进制分析框架。从最基础的路径查找（find）和规避（avoid），到符号化寄存器、栈、内存以及动态内存和文件系统，再到利用约束求解、Hook技术和SimProcedure处理复杂函数，最后还涉及到静态链接、共享库和漏洞利用场景。

每个题目都展示了如何通过 Python 脚本与angr交互，将二进制程序的分析转化为可解的约束问题。理解这些技术不仅对CTF解题有帮助，更是深入理解二进制文件的加载和执行、进行自动化漏洞挖掘和程序分析的重要基础。后续的学习需要将这些技术组合运用，并在更复杂的真实程序中实践。