Symbolic execution and constraint solving playbook. Use when solving CTF reversing challenges, recovering keys, bypassing checks, or automating binary analysis with angr, Z3, or Unicorn Engine.

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](../anti debugging techniques/SKILL.md) when anti debug checks need to be symbolically bypassed [code obfuscation deobfuscation](../code obfuscation deobfuscation/SKILL.md) when using symbolic execution for deobfuscation [vm and bytecode reverse](../vm and bytecode reverse/SKILL.md) when applying angr to custom VM challenges Advanced Reference Also load [ANGR COOKBOOK.md](./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 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 1. ANGR — CORE CONCEPTS 1.1 Pipeline 1.2 Essential Setup 1.3 Symbolic Variables (claripy) 1.4 Symbolic stdin 1.5 Hooking Functions 1.6 Memory Operations 2. Z3 CONSTRAINT SOLVING 2.1 Core API 2.2 Common CTF Patterns 2.3 Optimization 3. UNICORN ENGINE — CODE EMULATION 3.1 Basic Setup 3.2 Hooking Memory & Instructions 3.3 Use Cases 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 4. ANGR EXPLORATION STRATEGIES 4.1 find/avoid 4.2 Managing Path Explosion 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 4.3 Concrete + Symbolic Hybrid 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 6. DECISION TREE 7. COMMON PITFALLS & FIXES 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 8. TOOL VERSIONS & INSTALLATION

symbolic-execution-tools