symbolic-execution-tools

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

SKILL: Symbolic Execution Tools — Expert Analysis Playbook

SKILL: 符号执行工具 — 专家分析手册

AI LOAD INSTRUCTION: Expert symbolic execution techniques using angr, Z3, and Unicorn Engine. Covers CTF challenge automation, constraint solving patterns, function hooking, SimProcedure replacement, and emulation-based unpacking. Base models often produce broken angr scripts due to incorrect state initialization or missing hooks for libc functions.

AI加载说明：使用angr、Z3和Unicorn Engine的专家级符号执行技术。涵盖CTF挑战自动化、约束求解模式、函数挂钩、SimProcedure替换、基于仿真的脱壳。基础模型通常会生成存在问题的angr脚本，原因是状态初始化错误或缺少libc函数的挂钩。

0. RELATED ROUTING

0. 相关参考路由

anti-debugging-techniques when anti-debug checks need to be symbolically bypassed
code-obfuscation-deobfuscation when using symbolic execution for deobfuscation
vm-and-bytecode-reverse when applying angr to custom VM challenges

当需要符号绕过反调试校验时，参考anti-debugging-techniques
当使用符号执行做反混淆时，参考code-obfuscation-deobfuscation
当将angr应用到自定义VM挑战时，参考vm-and-bytecode-reverse

Advanced Reference

高级参考

Also load ANGR_COOKBOOK.md when you need:

15+ ready-to-use angr script patterns for common CTF challenges
Hook templates for scanf, printf, malloc, strcmp
Symbolic file input, stdin, argv patterns
Optimization tricks for path explosion management

当你需要以下内容时，也可以加载ANGR_COOKBOOK.md：

15+ 可直接用于常见CTF挑战的现成angr脚本模板
scanf、printf、malloc、strcmp的挂钩模板
符号化文件输入、stdin、argv模式
路径爆炸管理的优化技巧

When to use which tool

不同场景的工具选择

Scenario	Best Tool	Why
Pure math / equation system	Z3	Direct constraint solving, no binary needed
Binary with control flow	angr	Explores paths, manages constraints automatically
Emulate specific code region	Unicorn	Fast, no symbolic overhead, good for unpacking
Complex binary + custom VM	angr + Unicorn (combo)	angr for control flow, Unicorn for VM handlers
Kernel / firmware code	Qiling	Full system emulation with OS awareness

场景	最佳工具	原因
纯数学 / 方程组	Z3	直接约束求解，无需二进制
带控制流的二进制	angr	自动探索路径、管理约束
仿真特定代码区域	Unicorn	速度快，无符号执行开销，适合脱壳
复杂二进制 + 自定义VM	angr + Unicorn（组合）	angr处理控制流，Unicorn处理VM handler
内核 / 固件代码	Qiling	具备OS感知的全系统仿真

1. ANGR — CORE CONCEPTS

1. ANGR — 核心概念

1.1 Pipeline

1.1 执行流程

Project(binary)
  → Factory.entry_state() / blank_state(addr=)
    → SimulationManager(state)
      → explore(find=target, avoid=bad)
        → found[0].solver.eval(symbolic_var)

Project(binary)
  → Factory.entry_state() / blank_state(addr=)
    → SimulationManager(state)
      → explore(find=target, avoid=bad)
        → found[0].solver.eval(symbolic_var)

1.2 Essential Setup

1.2 基础配置

python

import angr
import claripy

proj = angr.Project('./challenge', auto_load_libs=False)

python

import angr
import claripy

proj = angr.Project('./challenge', auto_load_libs=False)

Entry state: start from program entry point

入口状态：从程序入口点开始执行

state = proj.factory.entry_state()

Blank state: start from arbitrary address

空白状态：从任意地址开始执行

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

Full init state: with command-line args

全初始化状态：带命令行参数

state = proj.factory.full_init_state(args=['./challenge', arg1_sym])

simgr = proj.factory.simulation_manager(state) simgr.explore(find=0x401234, avoid=[0x401300])

if simgr.found: found = simgr.found[0] solution = found.solver.eval(symbolic_input, cast_to=bytes) print(f"Solution: {solution}")

undefined

state = proj.factory.full_init_state(args=['./challenge', arg1_sym])

simgr = proj.factory.simulation_manager(state) simgr.explore(find=0x401234, avoid=[0x401300])

if simgr.found: found = simgr.found[0] solution = found.solver.eval(symbolic_input, cast_to=bytes) print(f"Solution: {solution}")

undefined

1.3 Symbolic Variables (claripy)

1.3 符号变量（claripy）

python

undefined

python

undefined

Bitvector (fixed-size integer)

位向量（固定大小整数）

sym_input = claripy.BVS("input", 64) # 64-bit symbolic sym_byte = claripy.BVS("byte", 8) # 8-bit symbolic sym_buf = claripy.BVS("buffer", 8 * 32) # 32-byte buffer

sym_input = claripy.BVS("input", 64) # 64位符号变量 sym_byte = claripy.BVS("byte", 8) # 8位符号变量 sym_buf = claripy.BVS("buffer", 8 * 32) # 32字节缓冲区

Concrete bitvector

具体位向量

concrete = claripy.BVV(0x41, 8) # concrete value 0x41

concrete = claripy.BVV(0x41, 8) # 具体值0x41

Constraints

约束条件

state.solver.add(sym_input > 0) state.solver.add(sym_input < 100) state.solver.add(sym_byte >= 0x20) # printable ASCII state.solver.add(sym_byte <= 0x7e)

state.solver.add(sym_input > 0) state.solver.add(sym_input < 100) state.solver.add(sym_byte >= 0x20) # 可打印ASCII state.solver.add(sym_byte <= 0x7e)

Evaluate

求值

value = state.solver.eval(sym_input) all_values = state.solver.eval_upto(sym_input, 10) # up to 10 solutions

undefined

value = state.solver.eval(sym_input) all_values = state.solver.eval_upto(sym_input, 10) # 最多返回10个解

undefined

1.4 Symbolic stdin

1.4 符号化标准输入

python

flag_len = 32
sym_stdin = claripy.BVS("stdin", 8 * flag_len)

state = proj.factory.entry_state(stdin=sym_stdin)

python

flag_len = 32
sym_stdin = claripy.BVS("stdin", 8 * flag_len)

state = proj.factory.entry_state(stdin=sym_stdin)

Constrain to printable ASCII

约束为可打印ASCII字符

for i in range(flag_len): byte = sym_stdin.get_byte(i) state.solver.add(byte >= 0x20) state.solver.add(byte <= 0x7e)

undefined

for i in range(flag_len): byte = sym_stdin.get_byte(i) state.solver.add(byte >= 0x20) state.solver.add(byte <= 0x7e)

undefined

1.5 Hooking Functions

1.5 函数挂钩

python

undefined

python

undefined

Hook by address (skip N bytes of original code)

按地址挂钩（跳过原代码的N个字节）

@proj.hook(0x401100, length=5) def skip_check(state): state.regs.eax = 1 # force success

@proj.hook(0x401100, length=5) def skip_check(state): state.regs.eax = 1 # 强制返回成功

SimProcedure: replace library function

SimProcedure：替换库函数

class MyStrcmp(angr.SimProcedure): def run(self, s1, s2): return claripy.If( self.state.memory.load(s1, 32) == self.state.memory.load(s2, 32), claripy.BVV(0, 32), claripy.BVV(1, 32) )

proj.hook_symbol('strcmp', MyStrcmp())

class MyStrcmp(angr.SimProcedure): def run(self, s1, s2): return claripy.If( self.state.memory.load(s1, 32) == self.state.memory.load(s2, 32), claripy.BVV(0, 32), claripy.BVV(1, 32) )

proj.hook_symbol('strcmp', MyStrcmp())

Hook common problematic functions

挂钩常见的问题函数

proj.hook_symbol('printf', angr.SIM_PROCEDURES['libc']'printf') proj.hook_symbol('scanf', angr.SIM_PROCEDURES['libc']'scanf') proj.hook_symbol('puts', angr.SIM_PROCEDURES['libc']'puts')

undefined

proj.hook_symbol('printf', angr.SIM_PROCEDURES['libc']'printf') proj.hook_symbol('scanf', angr.SIM_PROCEDURES['libc']'scanf') proj.hook_symbol('puts', angr.SIM_PROCEDURES['libc']'puts')

undefined

1.6 Memory Operations

1.6 内存操作

python

undefined

python

undefined

Read memory (symbolic-aware)

读取内存（支持符号感知）

data = state.memory.load(addr, size) # returns BV data_concrete = state.solver.eval(data, cast_to=bytes)

data = state.memory.load(addr, size) # 返回位向量 data_concrete = state.solver.eval(data, cast_to=bytes)

Write memory

写入内存

state.memory.store(addr, claripy.BVV(0x41, 8)) state.memory.store(addr, sym_buf)

Read/write registers

读写寄存器

rax = state.regs.rax state.regs.rdi = claripy.BVV(0x1000, 64)

---

rax = state.regs.rax state.regs.rdi = claripy.BVV(0x1000, 64)

---

2. Z3 CONSTRAINT SOLVING

2. Z3 约束求解

2.1 Core API

2.1 核心API

python

from z3 import *

python

from z3 import *

Sorts

数据类型

x = BitVec('x', 32) # 32-bit bitvector y = Int('y') # arbitrary precision integer b = Bool('b') # boolean

x = BitVec('x', 32) # 32位位向量 y = Int('y') # 任意精度整数 b = Bool('b') # 布尔值

Solver

求解器

s = Solver() s.add(x + y == 42) s.add(x > 0) s.add(y > 0)

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

undefined

s = Solver() s.add(x + y == 42) s.add(x > 0) s.add(y > 0)

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

undefined

2.2 Common CTF Patterns

2.2 常见CTF模式

python

undefined

python

undefined

Serial key validation: each char satisfies constraints

序列号验证：每个字符满足指定约束

key = [BitVec(f'k{i}', 8) for i in range(16)] s = Solver() for k in key: s.add(k >= 0x30, k <= 0x7a) # alphanumeric-ish

key = [BitVec(f'k{i}', 8) for i in range(16)] s = Solver() for k in key: s.add(k >= 0x30, k <= 0x7a) # 类字母数字范围

XOR key recovery

XOR密钥恢复

plaintext = b"known_plaintext" ciphertext = b"\x12\x34..." key_byte = BitVec('key', 8) s = Solver() for p, c in zip(plaintext, ciphertext): s.add(p ^ key_byte == c)

System of linear equations (modular)

线性方程组（模运算）

a, b, c = BitVecs('a b c', 32) s = Solver() s.add(3a + 5b + 7c == 0x12345678) s.add(2a + 4b + 6c == 0xDEADBEEF) s.add(a ^ b ^ c == 0xCAFEBABE)

undefined

a, b, c = BitVecs('a b c', 32) s = Solver() s.add(3a + 5b + 7c == 0x12345678) s.add(2a + 4b + 6c == 0xDEADBEEF) s.add(a ^ b ^ c == 0xCAFEBABE)

undefined

2.3 Optimization

2.3 优化

python

from z3 import Optimize

opt = Optimize()
x = BitVec('x', 32)
opt.add(x > 0)
opt.add(x < 1000)
opt.minimize(x)  # find smallest satisfying value
opt.check()
print(opt.model())

python

from z3 import Optimize

opt = Optimize()
x = BitVec('x', 32)
opt.add(x > 0)
opt.add(x < 1000)
opt.minimize(x)  # 查找最小的满足条件的值
opt.check()
print(opt.model())

3. UNICORN ENGINE — CODE EMULATION

3. UNICORN ENGINE — 代码仿真

3.1 Basic Setup

3.1 基础配置

python

from unicorn import *
from unicorn.x86_const import *
from capstone import Cs, CS_ARCH_X86, CS_MODE_64

mu = Uc(UC_ARCH_X86, UC_MODE_64)

CODE_ADDR = 0x400000
STACK_ADDR = 0x7fff0000
STACK_SIZE = 0x10000

mu.mem_map(CODE_ADDR, 0x10000)
mu.mem_map(STACK_ADDR, STACK_SIZE)

mu.mem_write(CODE_ADDR, code_bytes)
mu.reg_write(UC_X86_REG_RSP, STACK_ADDR + STACK_SIZE - 0x1000)
mu.reg_write(UC_X86_REG_RBP, STACK_ADDR + STACK_SIZE - 0x1000)

mu.emu_start(CODE_ADDR, CODE_ADDR + len(code_bytes))

result = mu.reg_read(UC_X86_REG_RAX)

python

from unicorn import *
from unicorn.x86_const import *
from capstone import Cs, CS_ARCH_X86, CS_MODE_64

mu = Uc(UC_ARCH_X86, UC_MODE_64)

CODE_ADDR = 0x400000
STACK_ADDR = 0x7fff0000
STACK_SIZE = 0x10000

mu.mem_map(CODE_ADDR, 0x10000)
mu.mem_map(STACK_ADDR, STACK_SIZE)

mu.mem_write(CODE_ADDR, code_bytes)
mu.reg_write(UC_X86_REG_RSP, STACK_ADDR + STACK_SIZE - 0x1000)
mu.reg_write(UC_X86_REG_RBP, STACK_ADDR + STACK_SIZE - 0x1000)

mu.emu_start(CODE_ADDR, CODE_ADDR + len(code_bytes))

result = mu.reg_read(UC_X86_REG_RAX)

3.2 Hooking Memory & Instructions

3.2 内存与指令挂钩

python

undefined

python

undefined

Hook memory access

挂钩内存访问

def hook_mem(uc, access, address, size, value, user_data): if access == UC_MEM_WRITE: print(f"Write {value:#x} to {address:#x}") elif access == UC_MEM_READ: print(f"Read from {address:#x}")

mu.hook_add(UC_HOOK_MEM_READ | UC_HOOK_MEM_WRITE, hook_mem)

def hook_mem(uc, access, address, size, value, user_data): if access == UC_MEM_WRITE: print(f"Write {value:#x} to {address:#x}") elif access == UC_MEM_READ: print(f"Read from {address:#x}")

mu.hook_add(UC_HOOK_MEM_READ | UC_HOOK_MEM_WRITE, hook_mem)

Hook specific instruction (for tracing)

挂钩指定指令（用于追踪）

def hook_code(uc, address, size, user_data): code = uc.mem_read(address, size) md = Cs(CS_ARCH_X86, CS_MODE_64) for insn in md.disasm(bytes(code), address): print(f" {insn.address:#x}: {insn.mnemonic} {insn.op_str}")

mu.hook_add(UC_HOOK_CODE, hook_code)

undefined

mu.hook_add(UC_HOOK_CODE, hook_code)

undefined

3.3 Use Cases

3.3 使用场景

Use Case	Approach
Unpack shellcode	Map shellcode, emulate, dump decoded payload
Decrypt strings	Emulate decryption function with controlled inputs
Brute-force short keys	Loop emulation with different key inputs
Analyze obfuscated function	Emulate function, observe register/memory state
Firmware code emulation	Map firmware memory layout, emulate routines

用途	实现方式
脱壳Shellcode	映射Shellcode，仿真执行，导出解码后的 payload
字符串解密	用可控输入仿真解密函数
短密钥暴力破解	循环传入不同密钥输入执行仿真
分析混淆函数	仿真函数执行，观察寄存器/内存状态
固件代码仿真	映射固件内存布局，仿真例程

4. ANGR EXPLORATION STRATEGIES

4. ANGR 探索策略

4.1 find/avoid

python

simgr.explore(
    find=lambda s: b"Correct" in s.posix.dumps(1),   # stdout contains "Correct"
    avoid=lambda s: b"Wrong" in s.posix.dumps(1)      # avoid "Wrong" output
)

python

simgr.explore(
    find=lambda s: b"Correct" in s.posix.dumps(1),   # 标准输出包含"Correct"
    avoid=lambda s: b"Wrong" in s.posix.dumps(1)      # 跳过输出"Wrong"的路径
)

4.2 Managing Path Explosion

4.2 路径爆炸管理

Strategy	Implementation
Constrain input space	Add constraints (printable, length limits)
Avoid dead-end paths	Use `avoid=` for known failure addresses
Hook complex functions	Replace with simplified SimProcedure
Limit loop iterations	`state.options.add(angr.options.LAZY_SOLVES)`
Use veritesting	`simgr.explore(..., technique=angr.exploration_techniques.Veritesting())`
DFS instead of BFS	`simgr.use_technique(angr.exploration_techniques.DFS())`
Timeout per path	`simgr.explore(..., num_find=1)` + timeout wrapper

策略	实现方式
约束输入空间	添加约束（可打印字符、长度限制）
避免死路径	用 `avoid=` 指定已知失败地址
挂钩复杂函数	替换为简化的SimProcedure
限制循环迭代次数	`state.options.add(angr.options.LAZY_SOLVES)`
使用Veritesting	`simgr.explore(..., technique=angr.exploration_techniques.Veritesting())`
用DFS替代BFS	`simgr.use_technique(angr.exploration_techniques.DFS())`
单路径超时	`simgr.explore(..., num_find=1)` + 超时封装

4.3 Concrete + Symbolic Hybrid

4.3 具体执行+符号执行混合模式

python

state = proj.factory.entry_state(
    add_options={angr.options.UNICORN}  # use Unicorn for concrete regions
)

This dramatically speeds up execution: concrete code runs natively via Unicorn, switching to symbolic only when symbolic variables are involved.

python

state = proj.factory.entry_state(
    add_options={angr.options.UNICORN}  # 具体执行区域使用Unicorn
)

这种方式可以大幅提升执行速度：具体代码通过Unicorn原生运行，只有涉及符号变量时才切换到符号执行模式。

5. PRACTICAL WORKFLOW

5. 实用工作流

5.1 CTF Binary Solving Workflow

5.1 CTF二进制解题工作流

1. Static analysis: identify input method, success/fail conditions
   └─ Find "Correct" / "Wrong" strings → get their xref addresses

2. Choose tool:
   ├─ Pure math (no binary needed) → Z3
   ├─ Small binary, clear success/fail → angr explore
   └─ Specific function to emulate → Unicorn

3. Set up symbolic input:
   ├─ stdin → claripy.BVS + entry_state(stdin=)
   ├─ argv → full_init_state(args=[...])
   ├─ file input → SimFile
   └─ specific memory → state.memory.store(addr, sym)

4. Hook problematic functions:
   ├─ printf/puts → SimProcedure or no-op
   ├─ scanf → custom handler
   ├─ time/random → return concrete value
   └─ anti-debug → skip entirely

5. Explore and extract:
   └─ simgr.explore(find=, avoid=) → solver.eval()

1. 静态分析：识别输入方式、成功/失败条件
   └─ 查找"Correct" / "Wrong"字符串 → 获取交叉引用地址

2. 选择工具：
   ├─ 纯数学问题（无需二进制） → Z3
   ├─ 小型二进制，成功/失败条件明确 → angr探索
   └─ 需要仿真特定函数 → Unicorn

3. 设置符号输入：
   ├─ 标准输入 → claripy.BVS + entry_state(stdin=)
   ├─ 命令行参数 → full_init_state(args=[...])
   ├─ 文件输入 → SimFile
   └─ 指定内存位置 → state.memory.store(addr, sym)

4. 挂钩问题函数：
   ├─ printf/puts → SimProcedure或空操作
   ├─ scanf → 自定义处理逻辑
   ├─ time/random → 返回具体值
   └─ 反调试逻辑 → 直接跳过

5. 探索并提取解：
   └─ simgr.explore(find=, avoid=) → solver.eval()

6. DECISION TREE

6. 决策树

Need to solve a reversing challenge?
│
├─ Is the challenge pure math / equations?
│  └─ Yes → Z3
│     ├─ Linear equations → BitVec + Solver
│     ├─ Modular arithmetic → BitVec (natural mod 2^n)
│     ├─ Boolean logic → Bool + Solver
│     └─ Optimization → Optimize + minimize/maximize
│
├─ Is it a compiled binary with clear success/fail?
│  └─ Yes → angr
│     ├─ Input via stdin → symbolic stdin
│     ├─ Input via argv → full_init_state with symbolic args
│     ├─ Input via file → SimFile
│     ├─ Path explosion → add constraints, avoid paths, hook loops
│     └─ Complex library calls → hook with SimProcedure
│
├─ Need to emulate a specific function/region?
│  └─ Yes → Unicorn Engine
│     ├─ Decryption routine → map code + data, emulate, read result
│     ├─ Shellcode analysis → map shellcode, hook syscalls
│     └─ Key schedule → emulate with different inputs
│
├─ Need to analyze firmware / exotic arch?
│  └─ Yes → Qiling (full system emulation with OS support)
│
├─ Binary has VM protection?
│  └─ angr for handler analysis + Z3 for bytecode constraints
│
└─ None of the above working?
   ├─ Combine: Unicorn for concrete regions + Z3 for constraints
   ├─ Manual reverse engineering with debugger
   └─ Side-channel approach (timing, power analysis for hardware)

需要解决逆向挑战？
│
├─ 挑战是纯数学/方程问题？
│  └─ 是 → Z3
│     ├─ 线性方程组 → BitVec + Solver
│     ├─ 模运算 → BitVec（天然模2^n）
│     ├─ 布尔逻辑 → Bool + Solver
│     └─ 优化问题 → Optimize + minimize/maximize
│
├─ 是有明确成功/失败条件的编译后二进制？
│  └─ 是 → angr
│     ├─ 输入通过标准输入 → 符号化stdin
│     ├─ 输入通过命令行参数 → 带符号参数的full_init_state
│     ├─ 输入通过文件 → SimFile
│     ├─ 路径爆炸 → 添加约束、跳过无效路径、挂钩循环
│     └─ 复杂库调用 → 用SimProcedure挂钩
│
├─ 需要仿真特定函数/代码区域？
│  └─ 是 → Unicorn Engine
│     ├─ 解密例程 → 映射代码+数据，仿真执行，读取结果
│     ├─ Shellcode分析 → 映射Shellcode，挂钩系统调用
│     └─ 密钥生成逻辑 → 传入不同输入仿真执行
│
├─ 需要分析固件/特殊架构？
│  └─ 是 → Qiling（支持OS的全系统仿真）
│
├─ 二进制有VM保护？
│  └─ angr做handler分析 + Z3处理字节码约束
│
└─ 以上方案都不生效？
   ├─ 组合方案：Unicorn处理具体区域 + Z3处理约束
   ├─ 配合调试器手动逆向
   └─ 侧信道方案（硬件场景用时序、功耗分析）

7. COMMON PITFALLS & FIXES

7. 常见问题与修复方案

Problem	Cause	Fix
angr hangs forever	Path explosion in loops	Add `avoid=` for loop-back edges, or hook the loop
Z3 returns `unknown`	Non-linear constraints too complex	Simplify, split into sub-problems, use `set_param("timeout", 5000)`
Unicorn crashes on syscall	Syscall not handled	Hook syscall interrupt, handle or skip
angr wrong result	Incorrect state initialization	Verify initial memory layout matches actual binary
Symbolic memory too large	Unbounded symbolic reads	Concretize array indices where possible
SimProcedure wrong types	Argument type mismatch	Check calling convention (cdecl vs fastcall)
angr can't load binary	Missing libraries	Use `auto_load_libs=False` + hook needed symbols

问题	原因	修复方案
angr永久挂起	循环导致路径爆炸	为循环回边添加 `avoid=` ，或挂钩循环逻辑
Z3返回 `unknown`	非线性约束过于复杂	简化问题、拆分为子问题，使用 `set_param("timeout", 5000)`
Unicorn遇到系统调用崩溃	系统调用未处理	挂钩系统调用中断，处理或跳过
angr返回错误结果	状态初始化错误	验证初始内存布局与实际二进制是否匹配
符号内存过大	无界符号读取	尽可能具体化数组索引
SimProcedure类型错误	参数类型不匹配	检查调用约定（cdecl vs fastcall）
angr无法加载二进制	缺少依赖库	使用 `auto_load_libs=False` + 挂钩需要的符号

8. TOOL VERSIONS & INSTALLATION

8. 工具版本与安装

bash

undefined

bash

undefined

angr (Python 3.8+)

pip install angr

Z3

pip install z3-solver

Unicorn Engine

pip install unicorn

Capstone (disassembly, pairs with Unicorn)

Capstone（反汇编，配合Unicorn使用）

pip install capstone

Keystone (assembly)

Keystone（汇编）

pip install keystone-engine

undefined

pip install keystone-engine

undefined