Symbolic Execution Tools

SKILL: Symbolic Execution Tools — Expert Analysis Playbook

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.

0. RELATED ROUTING

• 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

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

When to use which tool

---

1. ANGR — CORE CONCEPTS

1.1 Pipeline

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

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}")

1.3 Symbolic Variables (claripy)

# 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

# Concrete bitvector
concrete = claripy.BVV(0x41, 8)             # concrete value 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)

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

1.4 Symbolic stdin

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

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

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

1.5 Hooking Functions

# Hook by address (skip N bytes of original code)
@proj.hook(0x401100, length=5)
def skip_check(state):
    state.regs.eax = 1  # force success

# SimProcedure: replace library function
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']())

1.6 Memory Operations

# Read memory (symbolic-aware)
data = state.memory.load(addr, size)          # returns BV
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)

---

2. Z3 CONSTRAINT SOLVING

2.1 Core API

from z3 import *

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

# 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]}")

2.2 Common CTF Patterns

# 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

# XOR key recovery
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(3*a + 5*b + 7*c == 0x12345678)
s.add(2*a + 4*b + 6*c == 0xDEADBEEF)
s.add(a ^ b ^ c == 0xCAFEBABE)

2.3 Optimization

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())

---

3. UNICORN ENGINE — CODE EMULATION

3.1 Basic Setup

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

# 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)

# 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)

3.3 Use Cases

---

4. ANGR EXPLORATION STRATEGIES

4.1 find/avoid

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
)

4.2 Managing Path Explosion

4.3 Concrete + Symbolic Hybrid

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.

---

5. PRACTICAL WORKFLOW

5.1 CTF Binary Solving Workflow

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()

---

6. DECISION TREE

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)

---

7. COMMON PITFALLS & FIXES

---

8. TOOL VERSIONS & INSTALLATION

# angr (Python 3.8+)
pip install angr

# Z3
pip install z3-solver

# Unicorn Engine
pip install unicorn

# Capstone (disassembly, pairs with Unicorn)
pip install capstone

# Keystone (assembly)
pip install keystone-engine

angr Cookbook — Ready-to-Use Script Patterns for CTF Challenges

AI LOAD INSTRUCTION: Load this when you need drop-in angr script templates for common CTF challenge patterns. Each recipe includes the scenario description, complete script, and adaptation notes. Assumes the main SKILL.md is already loaded for angr fundamentals.

---

Recipe 1: Basic find/avoid by Address

Scenario: Binary prints "Correct" at 0x401234, "Wrong" at 0x401300. Input via stdin.

import angr

proj = angr.Project('./challenge', auto_load_libs=False)
state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)

simgr.explore(find=0x401234, avoid=[0x401300])

if simgr.found:
    print(simgr.found[0].posix.dumps(0))  # fd 0 = stdin

---

Recipe 2: Find by stdout Content

Scenario: Success/failure messages not at fixed addresses (PIE binary or indirect calls).

import angr

proj = angr.Project('./challenge', auto_load_libs=False)
state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)

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

if simgr.found:
    print(simgr.found[0].posix.dumps(0))

---

Recipe 3: Symbolic stdin with Printable Constraint

Scenario: Flag is 32 printable characters read via scanf/fgets.

import angr
import claripy

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

FLAG_LEN = 32
flag = claripy.BVS("flag", 8 * FLAG_LEN)

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

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

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

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

---

Recipe 4: Symbolic argv

Scenario: Binary takes flag as command-line argument ./challenge FLAG.

import angr
import claripy

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

flag = claripy.BVS("flag", 8 * 32)
state = proj.factory.full_init_state(
    args=['./challenge', flag],
    add_options=angr.options.unicorn
)

for i in range(32):
    b = flag.get_byte(i)
    state.solver.add(b >= 0x20, b <= 0x7e)

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

if simgr.found:
    print(simgr.found[0].solver.eval(flag, cast_to=bytes))

---

Recipe 5: Symbolic File Input

Scenario: Binary reads flag from a file.

import angr
import claripy

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

flag = claripy.BVS("flag", 8 * 64)
sim_file = angr.SimFile("flag.txt", content=flag)

state = proj.factory.entry_state(fs={'/tmp/flag.txt': sim_file})

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

if simgr.found:
    print(simgr.found[0].solver.eval(flag, cast_to=bytes))

---

Recipe 6: Hook scanf

Scenario: Custom scanf that angr's default SimProcedure handles incorrectly.

import angr
import claripy

class MyScanf(angr.SimProcedure):
    def run(self, fmt, ptr):
        buf = claripy.BVS("scanf_input", 8 * 32)
        self.state.memory.store(ptr, buf)
        self.state.globals['scanf_buf'] = buf
        return 1

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

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

if simgr.found:
    found = simgr.found[0]
    buf = found.globals['scanf_buf']
    print(found.solver.eval(buf, cast_to=bytes))

---

Recipe 7: Hook strcmp to Leak Expected Value

Scenario: Binary compares input against computed value. Hook strcmp to extract the expected string.

import angr
import claripy

class LeakStrcmp(angr.SimProcedure):
    def run(self, s1, s2):
        # Read both strings up to null
        str1 = self.state.memory.load(s1, 64)
        str2 = self.state.memory.load(s2, 64)
        self.state.globals['cmp_s1'] = s1
        self.state.globals['cmp_s2'] = s2
        return claripy.If(str1 == str2, claripy.BVV(0, 32), claripy.BVV(1, 32))

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

state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=0x401234)

if simgr.found:
    found = simgr.found[0]
    s2_addr = found.solver.eval(found.globals['cmp_s2'])
    expected = found.memory.load(s2_addr, 32)
    print(found.solver.eval(expected, cast_to=bytes))

---

Recipe 8: Start from Specific Function (skip initialization)

Scenario: Large binary, but the check function is known. Skip everything before it.

import angr
import claripy

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

CHECK_FUNC = 0x401500
BUF_ADDR = 0x600000

flag = claripy.BVS("flag", 8 * 32)

state = proj.factory.blank_state(addr=CHECK_FUNC)
state.memory.store(BUF_ADDR, flag)
state.regs.rdi = BUF_ADDR  # first arg = buffer pointer (System V ABI)
state.regs.rsi = 32         # second arg = length

state.stack_push(0xDEADBEEF)  # fake return address

simgr = proj.factory.simulation_manager(state)
simgr.explore(
    find=lambda s: b"OK" in s.posix.dumps(1),
    avoid=lambda s: b"FAIL" in s.posix.dumps(1)
)

if simgr.found:
    print(simgr.found[0].solver.eval(flag, cast_to=bytes))

---

Recipe 9: Veritesting (Merge Paths at Branches)

Scenario: Path explosion due to many conditional branches (e.g., per-character check).

import angr

proj = angr.Project('./challenge', auto_load_libs=False)
state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)

simgr.use_technique(angr.exploration_techniques.Veritesting())
simgr.explore(find=0x401234, avoid=[0x401300])

if simgr.found:
    print(simgr.found[0].posix.dumps(0))

---

Recipe 10: Unicorn Concrete Execution Speedup

Scenario: Most code is concrete (no symbolic data), only small portion needs symbolic reasoning.

import angr

proj = angr.Project('./challenge', auto_load_libs=False)
state = proj.factory.entry_state(
    add_options=angr.options.unicorn  # enable Unicorn backend
)
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=0x401234, avoid=[0x401300])

if simgr.found:
    print(simgr.found[0].posix.dumps(0))

---

Recipe 11: Multi-Stage Binary (Sequential Checks)

Scenario: Binary has multiple stages, each validating part of the flag.

import angr
import claripy

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

stages = [
    {"find": 0x401100, "avoid": [0x401150]},
    {"find": 0x401200, "avoid": [0x401250]},
    {"find": 0x401300, "avoid": [0x401350]},
]

flag = claripy.BVS("flag", 8 * 48)
state = proj.factory.entry_state(stdin=flag)

for i, stage in enumerate(stages):
    simgr = proj.factory.simulation_manager(state)
    simgr.explore(find=stage["find"], avoid=stage["avoid"])
    if simgr.found:
        state = simgr.found[0]
        partial = state.solver.eval(flag, cast_to=bytes)
        print(f"Stage {i+1}: {partial}")
    else:
        print(f"Stage {i+1} failed")
        break

---

Recipe 12: Constrain Flag Format (CTF{...})

Scenario: Flag format is known: flag{...} with alphanumeric content.

import angr
import claripy

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

FLAG_LEN = 40
flag = claripy.BVS("flag", 8 * FLAG_LEN)
state = proj.factory.entry_state(stdin=flag)

prefix = b"flag{"
for i, c in enumerate(prefix):
    state.solver.add(flag.get_byte(i) == c)
state.solver.add(flag.get_byte(FLAG_LEN - 1) == ord('}'))

for i in range(len(prefix), FLAG_LEN - 1):
    b = flag.get_byte(i)
    state.solver.add(
        claripy.Or(
            claripy.And(b >= ord('0'), b <= ord('9')),
            claripy.And(b >= ord('a'), b <= ord('z')),
            claripy.And(b >= ord('A'), b <= ord('Z')),
            b == ord('_'), b == ord('-')
        )
    )

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

if simgr.found:
    print(simgr.found[0].solver.eval(flag, cast_to=bytes))

---

Recipe 13: Replace rand() with Concrete Value

Scenario: Binary uses rand() making execution non-deterministic.

import angr

class ConcreteRand(angr.SimProcedure):
    def run(self):
        return 42  # deterministic

proj = angr.Project('./challenge', auto_load_libs=False)
proj.hook_symbol('rand', ConcreteRand())
proj.hook_symbol('srand', angr.SIM_PROCEDURES['libc']['srand']())

state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=0x401234)

if simgr.found:
    print(simgr.found[0].posix.dumps(0))

---

Recipe 14: Timeout + DFS for Deep Binaries

Scenario: Binary has deep execution path, BFS runs out of memory.

import angr
import signal

def timeout_handler(signum, frame):
    raise TimeoutError("angr timed out")

signal.signal(signal.SIGALRM, timeout_handler)
signal.alarm(300)  # 5-minute timeout

proj = angr.Project('./challenge', auto_load_libs=False)
state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)

simgr.use_technique(angr.exploration_techniques.DFS())

try:
    simgr.explore(find=0x401234, avoid=[0x401300])
    if simgr.found:
        print(simgr.found[0].posix.dumps(0))
except TimeoutError:
    print("Timed out — try narrowing search space")

---

Recipe 15: Symbolic Memory at Global Buffer

Scenario: Input is read into a global buffer at a known address, but through a complex path.

import angr
import claripy

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

GLOBAL_BUF = 0x604080
CHECK_START = 0x401200
FLAG_LEN = 24

flag = claripy.BVS("flag", 8 * FLAG_LEN)
state = proj.factory.blank_state(addr=CHECK_START)
state.memory.store(GLOBAL_BUF, flag)

for i in range(FLAG_LEN):
    b = flag.get_byte(i)
    state.solver.add(b >= 0x20, b <= 0x7e)

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

if simgr.found:
    print(simgr.found[0].solver.eval(flag, cast_to=bytes))

---

Adaptation Checklist

When adapting any recipe to your specific challenge:

1. Update addresses: find=, avoid=, function addresses, buffer addresses 2. Match input method: stdin, argv, file, or memory — use the right recipe 3. Set correct flag length: Too short = can't find solution; too long = slow 4. Add format constraints: Known prefix, charset, null terminator 5. Hook problematic functions: Any function causing path explosion or crashes 6. Choose exploration technique: BFS (default) for short paths, DFS for deep, Veritesting for branchy 7. Enable Unicorn: add_options=angr.options.unicorn for speed on mostly-concrete paths 8. Check architecture: Ensure auto_load_libs=False doesn't break needed functionality