re-angr

angr symbolic execution (symbolic input / automatic solving)

When to use / when not to use

• Use: CTF reversing challenges—input is checked byte by byte in a long loop / deep comparison chain (the check-pass address is known or can be located), and manual reverse reasoning is tedious and error-prone
• Use: when it is known that "the input must reach a certain address / avoid a certain address", and you want to hand the path conditions to a solver (find / avoid mode)
• Use: when the input source is complex (argv / file / stdin), and it needs to be symbolized by channel before solving
• Do not use: simple XOR / plaintext comparison (within one screen of pseudocode)—manual work is faster ([[re-binary-core]])
• Do not use: when the check contains non-symbolizable content (environment-dependent values, random numbers, unsymbolized input)—it will be unsolvable or misunderstood (see pitfall 3)
• Do not use: when an exact constraint set rather than one path is needed—pure constraint solving with [[re-z3]] is lighter (see pitfall 2)
• Note: symbolic execution is a double-edged sword—first manually locate the key check function to narrow the symbolic execution scope (see pitfall 2); run verification in a sandbox ([[re-analyze/platform-tips]] highest principle)

Tool preparation

Refer to [[re-analyze/platform-tips]] highest principle—when using the solving result to run the target for verification, default to a sandbox; angr itself is an in-process emulator, does not touch real system calls, and the solving process does not need a sandbox.

angr (installed via pip)

• pip install angr(Linux / macOS / Windows all work; on Windows install the win32 wheel with pip, or install the Linux version inside WSL)
• Python version compatibility (important)：angr 9.3.0 and later requires Python 3.12+（requires-python >=3.12; the current mainline 10.x is the same);9.2.x is not a fixed range—the lower bound rises with patch versions (9.2.91 requires ≥3.8, 9.2.203 already requires ≥3.10), so you cannot judge by the whole "9.2.x" line. Before installing, use the PyPI requires-python of the target version as the standard (pip index versions angr to see available versions), then choose according to the system Python:
  • System comes with Python 3.12+ (Ubuntu 24.04 defaults to 3.12) → directly pip install angr(current mainline 10.x; Python >=3.12)
  • System is Python 3.11 or below → pip install "angr<9.3"(9.2.x line),do not force-install 9.3+
  • For multiple coexisting versions, isolate with venv:python3.12 -m venv ~/venvs/angr && source ~/venvs/angr/bin/activate(or brew install python@3.12 / py -3.12 -m venv angr-venv）
• Before installing, first upgrade the basic tools:pip install --upgrade pip setuptools wheel(to avoid native component compilation failures)
• On Linux, it is recommended to add binutils(angr calls objcopy when processing / rewriting binaries):apt install binutils
• Verify: python3 -c "import angr; print(angr.__version__)"

python3

• Linux: apt install python3(mostly bundled); macOS: brew install python; Windows: official installer / choco install python
• Verify: python3 --version

Target binary

• Original sample copy (back up first: symbolic execution does not modify files, but modeling requires repeated comparison, see pitfall 5) + [[re-triage]] preliminary reconnaissance output (architecture / bitness / whether statically linked / whether packed)
• Verify: file target confirm architecture and bitness (angr supports ARM targets, pay attention to endianness)

Operation steps

Execute in order, record the result of each step (address / constraints / solving script / flag, for evidence paths see [[re-triage]]).Manual first, then automated: The smaller the symbolized range, the more stable it is (see Pitfall 2).

1. Input Adapter: determine the symbol source：

   • Decompile to locate the input read point:read / scanf / fgets / getline / main(int argc, char **argv) where argv is used ([[re-ghidra]] / [[re-ida]] / [[re-radare2]])

   • Bysymbol source typechoose the access method (CTF stdin is only one of them—real target input may be network packets/file mappings/JNI arguments/custom bytecode):

     Symbol source	Access method
     stdin (standard input)	project.factory.full_init_state(stdin=claripy.BVS('in', 32*8))
     argv (command-line arguments)	project.factory.full_init_state(args=["./target", claripy.BVS("arg1", 64*8)])
     file (file input)	state.fs.insert('/tmp/in', angr.SimFile('in', content=claripy.BVS('in', 32*8)))—symbolize immediately after fopen; when operating by fd use state.posix.fd[0](fd 0=stdin; fd 1/2 are stdout/stderr, do not mix them up)
     memory (mmap/heap/global buffer)	Directly symbolize the target memory region:state.memory.store(addr, claripy.BVS('buf', n*8))—the program reads from that address and it is symbolized (works generally for mmap files, decryption buffers, shared memory)
     network buffer (network packets/recv)	hook recv/read：Take the buf argument according to the calling convention(x86-64 SysV is RSI=buf, RDX=len), write the symbolic bytes to that address,the return value is the ssize_t byte count, not a buffer pointer—only by returning the symbolic length can if (recv(...) > 0) and similar control flow become variable. Implementing it as "return a symbolic pointer" will make all subsequent control flow wrong
     jni argument (Android native input parameters)	For JNIEnv method arguments, symbolize: from GetByteArrayElements/GetStringUTFChars return point symbolize (use [[re-android-native]]/[[re-frida]] to confirm the input parameter form)
     custom VM bytecode (custom VM instruction stream)	Symbolize the entire bytecode buffer + constrain the opcode range (0x00-0x0F type)—the symbolic execution path for VM reverse engineering ([[re-deobfuscate]] linkage)

   • Record: symbolization channel + byte count + read point address (used later for find / hook); confirm the N-byte length against the read point logic (see Pitfall 3)

2. Reach target address / avoid address modeling (find / avoid)：

   • Decompile to confirmsuccess path address(the address that prints the flag after verification passes) andfailure path addresses(the places that print "wrong", etc.; if there are multiple failure points, list them all)
   • Modeling:simgr.explore(find=<入口地址>, avoid=[<失败分支地址>])(find can take multiple addresses or a lambda lambda s: b"flag{" in s.posix.dumps(0)）
   • Tips for choosing the find address: choosethe verification loop exitrather than the program exit—just find the state of "having passed the verification success branch", no need to wait for printing (see Pitfall 5)
   • Verification is determined by the return value of a called function (if (check(input))) → set find at the success branch address after check returns, and avoid at the failure branch

3. Path constraints and solving (solver)：

   • After finding the state, the constraints are the conditions accumulated along that state's path:found = simgr.found[0]
   • Solving: evaluate the symbolic variables directly (without relying on the posix plugin):flag = found.solver.eval(inp, cast_to=bytes)(inp is the stdin/argv symbol created in step 1) or solve by symbol variable name:found.solver.eval(flag_sym, cast_to=bytes)
   • When there are multiple solutions, add constraints as needed (length / printable characters, see pitfall 4):

     for c in flag_sym.chop(8): found.solver.add(0x20 <= c, c <= 0x7e)
     

   • Output to file:open('flag.bin','wb').write(flag), and also print repr to check (non-printable characters are often a symbolic length issue, see pitfall 3)

4. Handling path explosion (hook / limit depth / segmentation)：

   • Hook irrelevant calls: replace heavy / system calls unrelated to the check with lightweight procedures:

     project.hook(addr_of_sleep_or_memset_impl, angr.SIM_PROCEDURES["stubs"]["ReturnUnconstrained"]())
     

     angr.SIM_PROCEDURES built-in libraries (libc.sleep、linux_kernel etc.) take priority:project.hook_symbol("sleep", angr.SIM_PROCEDURES["libc"]["sleep"])(sleep belongs to the libc category, not posix)
   • Limit exploration scale：simgr = proj.factory.simgr(state, veritesting=True)(veritesting merges paths, commonly used for long-loop challenges, see pitfall 2);simgr.explore(find=..., avoid=..., num_find=1) stop when found;stash upper limit / lazy_solves option controls
   • Segmented exploration: for long loops, hook the entry address, first explore to the loop boundary, then symbolically expand the loop body separately (after manually locating the loop invariant, narrow the scope)
   • Still exploding → go back to step 1 to narrow the symbolic scope / combine with manual analysis (see pitfall 2), or switch to [[re-z3]] to model the already-expanded loop body

5. Typical template (find / avoid pattern)：

   import angr, claripy
   p = angr.Project("./target", auto_load_libs=False)   # 关库加载，快且稳
   inp = claripy.BVS("inp", 32 * 8)                      # 32 字节符号化输入
   state = p.factory.full_init_state(stdin=inp)
   simgr = p.factory.simgr(state, veritesting=True)
   simgr.explore(find=0x401100, avoid=[0x401200, 0x401300])   # 示意地址：按目标实际入口/分支替换
   if simgr.found:
       sol = simgr.found[0].solver.eval(inp, cast_to=bytes)
       print(sol)                                        # 直接保存进证据目录
   else:
       print("no path found")                            # 排查：地址错 / 输入长度 / 未符号化
   

   • Template parameterization:find / avoid / input length / symbolic channel written into the script header comments, run with parameters changed one by one (see pitfall 5)

Verification: inside the sandbox ([[re-sandbox]]), run the target as-is with the solved input (stdin redirection ./target < flag.bin or via argv / file channel), must print flag{...}; cross-check with [[re-z3]] / manual restoration results (see pitfall 4).

Cross-domain combination

• [[re-address-space]]: align mapped_base/rebase with the target addresses

• [[re-ctf]]: this skill is the automated solving path for step 3 of the re-ctf gateway workflow (byte-by-byte long-loop check challenges)

• [[re-binary-core]]: the preceding workbench—decompile to locate the input reading point / success and failure branch addresses ([[re-ghidra]] / [[re-ida]] / [[re-radare2]]); [[re-triage]] initial survey determines architecture / bitness / packer

• [[re-deobfuscate]]: deobfuscate first, then symbolic execution (direct symbolic execution of junk instructions / flattened functions will cause path explosion)

• [[re-z3]]: sister skill—for constraint sets with no loops / already manually expanded, z3 is lighter and faster; when angr solving is slow, convert a subset of constraints to z3

• [[re-crypto-decrypt]]: its "tool preparation" lists angr as an optional decryption emulation approach (symbolically execute the decryption function when algorithm restoration fails)

• [[re-sandbox]]: the sandbox for run verification of solved inputs ([[re-analyze/platform-tips]] highest principle)

• [[re-gdb]] / [[re-tracing]]: dynamic cross-verification (use breakpoints to see the actual direction of the check branch, cross-check with angr path conclusions)

Common pitfalls and traps

• Path explosion: symptom—explore after running for over ten minutes the state count skyrockets and memory is exhausted; cause—symbolic scope too large (the entire program is symbolized), irrelevant branches (strlen / memcpy expansion, error handling branches) are explored one by one, long loops are not merged; countermeasures—hook irrelevant system calls (step 4),veritesting=True merge paths,num_find=1 Stop as soon as it is found and narrow the symbolized input range (step 1 symbolizes only the bytes actually read for verification); if it still does not work, explore in segments or switch to manual analysis
• Complex verification is slow → combine with manual analysis: Symptom—a seemingly simple challenge gets no result from angr after several minutes; Cause—the verification chain is interleaved with table lookups / random numbers / syscall side effects, where symbolic execution is inefficient; Countermeasure—first manually decompile to locatethe key verification function, set the symbolic entry point to the verification function entry (blank_state + manually set registers / memory), skipping the preceding irrelevant code; when the verification is a pure set of equations, directly switch to [[re-z3]]
• Unsymbolized input → no solution: Symptom—explore returns in seconds with no path found, or the solved value does not pass when run on the original program; Cause—the input was not symbolized (what is read is the real stdin / file contents), the number of symbolized bytes < the actual read length (fgets(buf, 0x40) but only 16 bytes are symbolized), the input contains quantities that can only be determined at runtime (random numbers / timestamps); Countermeasure—check the decompilation to confirm the read point and length (step 1), symbolize the stdin length according to the read upper bound; fix random value points with a hook (hook_symbol("rand", ...)) and then symbolize
• Python version compatibility: Symptom—pip install angr reports a compilation error / crashes on import (ImportError points to a C extension); Cause—angr 9.3.0+ officially requires Python 3.12+, and the lower bound of the 9.2.x line rises with the patch version (9.2.91 requires ≥3.8, 9.2.203 already requires ≥3.10), so installing a new version on an overly old interpreter (or installing an old dependency without a wheel on 3.13) compiles on the spot or even fails; Countermeasure—checkthe target version's Python requirement (PyPI requires-python): for 9.3+ use 3.12+, for 9.2 choose the interpreter according to the metadata of the specific patch version, create an independent venv to install (tool preparation section); before installing pip install --upgrade pip setuptools wheel
• Wrong find address → the solved "flag" does not run: Symptom—the solve succeeds but the output contains non-printable characters / the program does not print the flag; Cause—find is set in the wrong handling loop (failures also pass through it), only one of multiple failure points is avoided, the symbolized length is inconsistent with what the program reads; Countermeasure—choose find asthe verification loop exit(use decompilation to confirm the unique success path), and list all failure branches in avoid; first check the output with repr() and then replay it as-is (see step 3 verification); take multiple solutions and run them one by one against the target for verification
• PIE base address offset → find address filled in wrong: Symptom—using the address shown by Ghidra (such as 0x00101231) as find, angr never finds it; Cause—for PIE binaries Ghidra displays addresses based on a 0x100000 base, while angr loads from 0x400000; Countermeasure—convert the address (a fixed offset like 0x300000), or first check the actual load base address of the module inside angr before determining the find address, and annotate the conversion relationship in a comment at the top of the script
• Direct symbolic execution is inefficient for custom VM/heavily obfuscated challenges: Symptom—the verification is wrapped in a custom bytecode VM (Tigress, etc.), and angr has state explosion / no solution; Cause—the VM's dispatch loop repeatedly symbolizes + obfuscated path branches (first eliminate opaque predicates, see [[re-deobfuscate]]); Countermeasure—use Unicorn to instantiate and emulate the VM handler (angr is only responsible for the outer control flow), or after exploring to dead paths export the SMT equations of each path and hand them to [[re-z3]] to generate the input (the Tigress case achieves 100% branch coverage)
• Inaccurate SimProcedure summary → bizarre results: Symptom—explore the results clearly violate intuition (wrong return values, bypassed checks), or the same logic produces inconsistent results when run a different way; Cause—angr uses Python summaries (SimProcedure) to replace library functions to avoid path explosion (strlen/malloc, etc.), but the summaries have bugs or are incomplete; Countermeasure—when behavior is abnormal, suspect SimProcedure first: disable the corresponding summary (note that if input constraints are not tight, path explosion may occur) or use project.hook to customize a summary according to the actual scenario (e.g., write your own scanf hook for a single format string)
• Missing division-by-zero constraint → solving produces weird values like 4294967295: Symptom—the solved input contains 0xFFFFFFFF and the like, and running the original program will definitely crash; Cause—Z3 evaluates a/b(denominator is 0) as all 1s (4294967295), and angr only intercepts division by zero on some paths (VEX-side exits); SimProcedure/custom analysis code may slip past it; Countermeasure—explicitly add a "denominator is nonzero" constraint to symbolic expressions involving division; do not rely on angr to handle it automatically
• Uninitialized registers/memory are automatically symbolized → bloated solution space: Symptom—solving is extremely slow or the results contain junk values, and the log has unconstrained warnings; Cause—entry_state generates unconstrained symbolic variables for uninitialized registers/memory, symbolizing irrelevant state as well; Countermeasure—set the state option ZERO_FILL_UNCONSTRAINED_MEMORY/ZERO_FILL_UNCONSTRAINED_REGISTERSaccording to the warnings (or SYMBOL_FILL_* to suppress warnings), or explicitly set known initial values to shrink the solution space
• cmovxx does not automatically split branches (ollvm successor recovery): Symptom—when angr simulates ollvm real blocks to find successors, cmov branches are lost and the successor relationships are incomplete; Cause—angr accumulates constraints on cmov-type instructions viarather than splitting into two states; Countermeasure—split manually:state.copy() two copies (one executes Move:setattr(regs, dst, getattr(regs, src)), one does not), andmanually skip the cmov instruction（state.regs.ip += ins.size) to prevent angr from executing it again, then step each simgr separately to find successors
• Dispatcher hook requires unhook + address offset calibration: Symptom—after the hook hooks the main dispatcher's last instruction and jumps to a real block, execution jumps back to the dispatcher in an infinite loop, or angr decodes garbled instructions; Cause—the hook was not removed (execution returns and enters the hook again); capstone decodes from the wrong boundary (instruction misalignment); Countermeasure—unhook immediately after jumping to the target block; when decoding is garbled, adjust the hook address (empirical offset such as -6, try bit by bit and output the disassembly for comparison to confirm, see the method in the next item)
• ollvm real block identification and patch order: Symptom—static plugins (D-810) are powerless against mutated ollvm (double loop headers, merge block merged with loop header); Cause—static analysis struggles with variants; Countermeasure—use dynamic execution to find the real order: BFS to find the loop header (returning to an already visited block means it is the loop header) → the loop header's two predecessors = prologue + merge block (the one with multiple predecessors is the merge block) → the merge block's predecessors = real blocks, and also find the ret block (no successors and the last instruction is retn);patch order is fixed: first collect the full list of useless blocks (including start and end addresses) → then patch the control flow → finally nop the useless blocks according to the earlier list (patching first and then finding useless blocks will find them incorrectly)
• API quick reference (loading/state/solving/hook families) and combination patterns are in [[commands]]; version differences, solving semantics, and loading boundaries are in [[gotchas]]