例如，对于代码 y = x * 2 + 3，如果 x 是符号变量 X，则 y 的值就是表达式 2X + 3。当程序遇到分支 if (y > 10) 时，符号执行不会只走一条路径，而是记录两个路径约束：True 分支的约束是 2X + 3 > 10（即 X > 3.5），False 分支的约束是 2X + 3 <= 10（即 X <= 3.5）。

这样，程序的每条执行路径都对应一组约束条件。路径的终点要么是正常返回，要么是错误/成功状态。如果要找到使程序走到某个特定路径的输入，只需要将该路径上的所有约束条件收集起来，交给约束求解器（如 Z3）求解即可。

符号执行与具体执行的关键区别在于：具体执行一次只能探索一条路径，符号执行可以同时表示所有路径。但这也带来了路径爆炸的问题——分支越多，路径数量呈指数增长。

什么时候适合

符号执行适合：

输入长度有限。
分支条件清晰。
算法不是大量哈希或加密黑盒。
路径数量可控。
成功分支明确。

如果路径爆炸、环境调用复杂、循环巨大，就需要剪枝、hook 或手动建模。

路径爆炸（Path Explosion）：这是最核心的问题。每遇到一个依赖符号变量的分支，路径数量翻倍。一个有 n 个符号相关分支的程序，理论上有 2^n 条路径。即使大多数路径很快终止或被剪枝，路径数量仍然可能大到无法处理。对于有复杂循环的程序（循环 1000 次，每次有一个分支），路径数量是天文数字。应对策略包括：限制循环次数（LoopBound）、深度优先搜索优先探索一条路径、以及使用 Veritesting 等技术合并相似路径。

系统调用和库函数处理：angr 不会真正执行系统调用（read、write、mmap 等），而是用模拟器（SimProcedure）替代。如果程序依赖复杂的系统交互（网络通信、文件系统操作、多进程），angr 的模拟可能不准确或直接失败。常见的应对方式是 hook 相关函数，提供简化的实现或直接返回固定值。

加密和哈希函数：如果程序内部使用 SHA256、AES 等加密算法对输入做变换，符号执行会产生极其复杂的约束表达式，求解器几乎不可能在合理时间内求解。遇到这种情况，应该跳过符号执行，改用已知明文攻击或手动分析算法弱点。

浮点运算和复杂数据结构：符号执行对浮点数的支持有限，涉及浮点比较的分支可能无法正确处理。复杂的动态数据结构（链表、树、哈希表）也会让符号内存模型变得非常复杂。

angr 和 Z3

angr 可以对二进制进行符号执行。

Z3 可以求解你手动提取的约束。

很多 CTF 逆向题其实不需要完整 angr，手动把校验逻辑翻译成 Z3 约束更稳。

选择工具前要先看问题规模。

angr 的基本工作流程

angr 是一个功能强大的二进制分析框架，其符号执行的典型工作流程分为四个阶段：

加载（Load）：angr.Project('./binary') 加载目标二进制文件，自动识别架构（x86、ARM、MIPS 等）和调用约定。angr 使用 CLE（CLE Loads Everything）库来加载各种格式的二进制文件和依赖库。

状态初始化（Init State）：p.factory.entry_state() 创建从程序入口点开始的初始状态。状态包含寄存器值、内存内容、符号变量等。也可以用 p.factory.call_state(addr) 从某个函数地址开始。对于符号输入，可以用 claripy.BVS('input', size) 创建符号变量并注入到 stdin 或内存中。

符号执行与探索（Explore）：simgr.explore(find=target, avoid=bad) 是最常用的探索策略。angr 会维护一个状态集合（simulation manager），每步执行后分裂出新的状态。find 参数指定目标地址，当某个状态到达该地址时被标记为 found；avoid 参数指定要避免的地址。

约束求解（Solve）：找到目标状态后，用 state.solver.eval(symbolic_var) 求解符号变量的具体值。angr 内部使用 Z3 或 Claripy 作为约束求解器。可以求出一个解、多个解、或验证约束是否可满足。

angr 基本工作流

angr 是一个二进制分析框架，支持符号执行：

import angr
import claripy

# 基本用法
def angr_basic():
    # 加载二进制
    p = angr.Project('./vuln', auto_discover=False)

    # 创建初始状态
    state = p.factory.entry_state()

    # 创建模拟管理器
    simgr = p.factory.simulation_manager(state)

    # 执行到目标地址
    target = 0x401234  # 成功分支地址
    avoid = [0x401256]  # 失败分支地址

    simgr.explore(find=target, avoid=avoid)

    if simgr.found:
        found_state = simgr.found[0]
        # 获取输入
        input_data = found_state.posix.dumps(0)
        print(f"找到输入: {input_data}")
        return input_data
    else:
        print("未找到路径")
        return None

angr 进阶用法

def angr_advanced():
    p = angr.Project('./vuln')

    # 创建符号输入
    # 方式 1：标准输入
    state = p.factory.entry_state()

    # 方式 2：符号变量
    sym_input = claripy.BVS('input', 64)  # 64 位符号变量
    state = p.factory.entry_state(stdin=angr.SimFileStream(
        name='stdin',
        content=sym_input,
        has_end=False
    ))

    # 设置约束
    # 限制输入为可打印字符
    for i in range(8):
        byte = sym_input.get_byte(i)
        state.solver.add(byte >= 0x20)
        state.solver.add(byte <= 0x7e)

    # 运行
    simgr = p.factory.simulation_manager(state)
    simgr.explore(find=0x401234)

    if simgr.found:
        found = simgr.found[0]
        # 求解约束
        solution = found.solver.eval(sym_input)
        print(f"解: {solution}")

约束求解示例

from z3 import *

def z3_basic():
    # 基本约束求解
    x = BitVec('x', 32)
    y = BitVec('y', 32)

    s = Solver()
    s.add(x + y == 100)
    s.add(x > 0)
    s.add(y > 0)
    s.add(x < 50)

    if s.check() == sat:
        m = s.model()
        print(f"x = {m[x]}, y = {m[y]}")

def z3_string():
    # 字符串约束
    flag = [BitVec(f'flag_{i}', 8) for i in range(16)]

    s = Solver()

    # 限制为可打印字符
    for c in flag:
        s.add(c >= 0x20)
        s.add(c <= 0x7e)

    # 约束条件（模拟校验逻辑）
    s.add(flag[0] == ord('f'))
    s.add(flag[1] == ord('l'))
    s.add(flag[2] == ord('a'))
    s.add(flag[3] == ord('g'))
    s.add(flag[4] == ord('{'))

    # 更多约束...
    for i in range(5, 15):
        s.add(flag[i] ^ 0x42 == some_value[i])

    s.add(flag[15] == ord('}'))

    if s.check() == sat:
        m = s.model()
        result = ''.join(chr(m[c].as_long()) for c in flag)
        print(f"Flag: {result}")

def z3_reverse():
    # 逆向算法求解
    x = BitVec('x', 32)

    # 模拟复杂的变换
    y = x
    y = y ^ 0x12345678
    y = y + 0xabcdef01
    y = y ^ (y << 13)
    y = y ^ (y >> 17)
    y = y ^ (y << 5)

    # 目标值
    target = 0xdeadbeef

    s = Solver()
    s.add(y == target)

    if s.check() == sat:
        m = s.model()
        print(f"x = {hex(m[x].as_long())}")

angr 与 Z3 的选择

# 什么时候用 angr：
# 1. 程序逻辑复杂，手动分析困难
# 2. 需要处理系统调用、内存访问
# 3. 路径较多，需要自动探索
# 4. 二进制程序，没有源码

# 什么时候用 Z3：
# 1. 校验逻辑相对简单
# 2. 可以手动提取约束
# 3. angr 路径爆炸太严重
# 4. 需要精确控制约束
# 5. 算法是纯数学运算

# 通常：先尝试 angr，失败后手动用 Z3

路径探索策略

def angr_path_exploration():
    p = angr.Project('./vuln')
    state = p.factory.entry_state()
    simgr = p.factory.simulation_manager(state)

    # 策略 1：深度优先
    simgr.use_technique(angr.exploration_techniques.DFS())

    # 策略 2：广度优先（默认）
    # simgr.explore(find=target)

    # 策略 3：循环限制
    simgr.use_technique(angr.exploration_techniques.LoopSeer(
        cfg=None,
        bound=10  # 最多循环 10 次
    ))

    # 策略 4：手动步骤执行
    while len(simgr.active) > 0:
        simgr.step()

        # 检查是否到达目标
        for active in simgr.active:
            if active.addr == target_addr:
                return active

        # 丢弃不需要的路径
        simgr.move('active', 'pruned', filter_func=lambda s: s.addr in bad_addrs)

    return None

符号执行 vs 模糊测试

# 符号执行（Symbolic Execution）
# 优点：
# - 可以系统地探索所有路径
# - 能找到边界情况
# - 可以生成达到特定路径的输入
# 缺点：
# - 路径爆炸问题
# - 环境建模困难
# - 可能很慢

# 模糊测试（Fuzzing）
# 优点：
# - 快速，能覆盖大量代码
# - 不需要深入理解程序
# - 可以处理复杂环境交互
# 缺点：
# - 可能遗漏深层路径
# - 难以达到特定条件
# - 覆盖率可能有限

# 实际使用中常结合两者：
# 1. 用 fuzzer 快速探索
# 2. 对难覆盖的路径用符号执行

angr 处理复杂程序

def angr_complex():
    p = angr.Project('./vuln')

    # hook 外部函数
    @p.hook_symbol('printf')
    def hook_printf(state):
        """简化 printf：读取格式字符串，记录输出"""
        fmt_addr = state.regs.rdi
        fmt_str = state.solver.eval(fmt_addr, cast_to=bytes)
        # 提取 %s/%x/%d 参数并记录
        state.globals['printf_output'] = fmt_str

    @p.hook_symbol('scanf')
    def hook_scanf(state):
        """简化 scanf：为输入创建符号变量"""
        fmt_addr = state.regs.rdi
        # 为每个输入创建一个符号字节
        input_var = state.solver.BVS('scanf_input', 8 * 32)
        buf_addr = state.regs.rsi
        state.memory.store(buf_addr, input_var)

    # 设置初始状态
    state = p.factory.entry_state()

    # 处理动态内存
    state.heap.heap_base = 0x400000

    # 运行
    simgr = p.factory.simulation_manager(state)
    simgr.explore(find=0x401234, avoid=[0x401256])

    if simgr.found:
        found = simgr.found[0]
        # 获取所有解
        solutions = found.solver.eval_upto(sym_input, 10)
        for sol in solutions:
            print(f"解: {sol}")

常见失败原因

把符号执行当成万能自动解题器：它适合约束清晰的输入校验，不适合所有逆向题。
不限制输入字符范围：求解器可能给不可打印字节，导致结果不可用或路径错误。
位宽建错：字节运算用 8 位 BitVec，整数运算要注意溢出和符号扩展。
把 Python Int 和 C 无符号溢出混用：C 里 uint8_t/uint32_t 溢出要用 BitVec 建模。
遇到哈希/AES 还硬求：标准加密应先识别算法和弱点，不要让 Z3 解黑盒。
求出输入后不验证：solver 模型可能和实际程序语义有差异，必须回到原程序运行。
路径爆炸不剪枝：增加格式约束、avoid 地址、hook 函数或改用手动建模。

迷你案例

一个 check 函数对 8 字节输入做多组判断：

(s[0] ^ 0x12) == 0x74
s[1] + s[2] == 0xd6
s[3] * 3 == 0x129
s[4] == '_'

静态读出所有条件后，用 8 个 BitVec(8) 建模，并给每个字节加可打印范围。Z3 求出 b'flag_xx}'，回到程序运行，输出 Correct。这个案例的闭环是：定位 check -> 提取约束 -> Z3 求解 -> 原程序验证。

符号执行与约束求解

符号执行与约束求解

一句话判断

题目中常见信号

核心概念

最小分析流程

最小验证示例

常见利用 / 解题路线

具体执行和符号执行

符号执行的核心思想

约束是什么