Project 11: Symbolic Execution with angr

Expanded deep-dive guide for Project 11 from the Binary Analysis sprint.

Quick Reference

Attribute Value
Difficulty Level 4: Expert
Time Estimate 2-3 weeks
Main Programming Language Python
Alternative Programming Languages None (angr is Python-only)
Coolness Level Level 5: Pure Magic (Super Cool)
Business Potential 1. The “Resume Gold”
Knowledge Area Program Analysis / Constraint Solving
Software or Tool angr framework, Python 3
Main Book angr documentation

1. Learning Objectives

  1. Build a working implementation with reproducible outputs.
  2. Justify key design choices with binary-analysis principles.
  3. Produce an evidence-backed report of findings and limitations.
  4. Document hardening or next-step improvements.

2. All Theory Needed (Per-Concept Breakdown)

This project depends on concepts from the main sprint primer: loader semantics, control/data-flow recovery, runtime observation, and mitigation-aware vulnerability reasoning. Before implementation, restate the project’s core assumptions in your own words and define how you will validate them.

3. Project Specification

3.1 What You Will Build

Use symbolic execution to automatically find inputs that reach specific program states, solving CTF challenges and finding bugs.

3.2 Functional Requirements

  1. Accept the target binary/input and validate format assumptions.
  2. Produce analyzable outputs (console report and/or artifacts).
  3. Handle malformed inputs safely with explicit errors.

3.3 Non-Functional Requirements

  • Reproducibility: same input should produce equivalent findings.
  • Safety: unknown samples run only in isolated lab contexts.
  • Clarity: separate facts, hypotheses, and inferred conclusions.

3.4 Expanded Project Brief

  • File: P11-symbolic-execution-with-angr.md

  • Main Programming Language: Python
  • Alternative Programming Languages: None (angr is Python-only)
  • Coolness Level: Level 5: Pure Magic (Super Cool)
  • Business Potential: 1. The “Resume Gold”
  • Difficulty: Level 4: Expert
  • Knowledge Area: Program Analysis / Constraint Solving
  • Software or Tool: angr framework, Python 3
  • Main Book: angr documentation

What you’ll build: Use symbolic execution to automatically find inputs that reach specific program states, solving CTF challenges and finding bugs.

Why it teaches binary analysis: Symbolic execution represents the frontier of automated program analysis. It finds paths humans might miss.

Core challenges you’ll face:

  • Setting up states → maps to defining where to start
  • Avoiding path explosion → maps to constraining exploration
  • Finding target addresses → maps to what state do you want?
  • Extracting solutions → maps to getting concrete inputs

Resources for key challenges:

Key Concepts:

  • Symbolic State: angr docs - Core Concepts
  • Exploration Techniques: angr docs - Simulation
  • Constraint Solving: Z3 solver basics

Difficulty: Expert Time estimate: 2-3 weeks Prerequisites: Projects 1-8, Python proficiency

Real World Outcome

Deliverables:

  • Analysis output or tooling scripts
  • Report with control/data flow notes

Validation checklist:

  • Parses sample binaries correctly
  • Findings are reproducible in debugger
  • No unsafe execution outside lab ```python import angr import claripy

Load binary

proj = angr.Project(‘./crackme’, auto_load_libs=False)

Create symbolic input (32 bytes)

password = claripy.BVS(‘password’, 32 * 8)

Create initial state at entry point

state = proj.factory.entry_state( args=[’./crackme’], stdin=angr.SimFile(‘/dev/stdin’, content=password) )

Create simulation manager

simgr = proj.factory.simulation_manager(state)

Explore: find ‘success’, avoid ‘failure’

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

Extract solution

if simgr.found: solution = simgr.found[0].solver.eval(password, cast_to=bytes) print(f”Password: {solution.decode()}”) else: print(“No solution found”)

Output:

Password: sup3r_s3cr3t_k3y


#### Hints in Layers
angr workflow:
1. Load binary with `angr.Project()`
2. Create symbolic variables with `claripy.BVS()`
3. Create initial state with `factory.entry_state()`
4. Create simulation manager with `factory.simulation_manager()`
5. Explore with `simgr.explore(find=..., avoid=...)`
6. Extract solution with `solver.eval()`

Tips for avoiding path explosion:
- Use `avoid` to skip irrelevant paths
- Set memory limits on states
- Use hooks to skip complex functions
- Start exploration from specific addresses

Common patterns:
```python
# Find by address
simgr.explore(find=0x401234, avoid=0x401111)

# Find by output string
simgr.explore(
    find=lambda s: b"WIN" in s.posix.dumps(1),
    avoid=lambda s: b"LOSE" in s.posix.dumps(1)
)

# Hook a function
@proj.hook(0x401000, length=5)
def skip_check(state):
    state.regs.eax = 1  # Always succeed

Learning milestones:

  1. Solve simple crackme → Basic symbolic execution
  2. Handle complex inputs → Symbolic arrays
  3. Use hooks → Skip annoying functions
  4. Solve CTF challenges → Real-world application

The Core Question You Are Answering

“Can we automatically explore all possible execution paths in a program and mathematically prove which inputs reach specific program states—without manually testing every input?”

This project introduces symbolic execution, a technique that treats program inputs as mathematical symbols rather than concrete values. Instead of testing one input at a time, you’ll explore entire classes of inputs simultaneously, using constraint solvers to find the exact input that triggers a bug or reaches a target state.

Concepts You Must Understand First

  1. Concrete vs. Symbolic Execution
    • Concrete execution: run program with specific input (“test123”), get specific output
    • Symbolic execution: run program with symbolic input (x₀, x₁, x₂…), track constraints
    • How symbolic execution explores multiple paths simultaneously

    Guiding Questions:

    • What happens when a program branches on symbolic input (if (input[0] == 'A'))?
    • How does symbolic execution differ from fuzzing (which uses random concrete inputs)?
    • Why is symbolic execution deterministic while fuzzing is probabilistic?

    Book References:

    • “Practical Binary Analysis” by Dennis Andriesse - Chapter 11.4: Symbolic Execution
    • angr documentation - Core Concepts: Symbolic Variables
    • Academic paper: “A Survey of Symbolic Execution Techniques” (Baldoni et al., 2018)
  2. SMT Solvers and Constraint Solving
    • Satisfiability Modulo Theories (SMT): solving logical formulas over different domains
    • Z3 solver (used by angr): determines if constraints are satisfiable
    • Constraints accumulate as execution proceeds: x[0] == 'A' AND x[1] != 'B' AND ...

    Guiding Questions:

    • What does it mean for a set of constraints to be “unsatisfiable”?
    • How does angr use Z3 to generate concrete inputs from symbolic constraints?
    • Why is SMT solving computationally expensive (NP-complete in general)?

    Book References:

    • Z3 Tutorial: “Programming Z3” (De Moura & Bjørner)
    • “Computer Systems: A Programmer’s Perspective” - Chapter 2.2: Integer Representations (foundation for bitvector logic)
  3. Path Explosion Problem
    • Exponential growth of paths: n branches → 2ⁿ possible paths
    • Loops amplify explosion: 100-iteration loop creates astronomical path count
    • Mitigations: path merging, state pruning, selective exploration

    Guiding Questions:

    • Why does a simple loop for(i=0; i<100; i++) create path explosion?
    • How do you prioritize which paths to explore first?
    • What’s the trade-off between path coverage and analysis time?

    Book References:

    • “Practical Binary Analysis” - Chapter 11.4: Symbolic Execution (discusses path explosion)
    • angr documentation - Exploration Techniques
  4. Intermediate Representation (IR)
    • angr uses VEX IR (from Valgrind) to represent machine code abstractly
    • Why IR: easier to analyze than raw assembly, architecture-independent
    • Statements, expressions, and temporary variables in VEX

    Guiding Questions:

    • Why doesn’t angr operate directly on x86/ARM assembly?
    • What information is lost when translating assembly → IR?
    • How do you map a VEX IR address back to assembly for debugging?

    Book References:

    • angr documentation - Core Concepts: Intermediate Representation
    • “Practical Binary Analysis” - Chapter 11.3: Dynamic Binary Instrumentation (similar IR concepts)
  5. Simulation State and Memory Models
    • angr’s SimState: CPU registers, memory, file system, all symbolic or concrete
    • Symbolic memory: can read/write symbolic values
    • Lazy memory model: only allocates pages when accessed

    Guiding Questions:

    • What happens when you read from a symbolic memory address?
    • How does angr decide whether a memory value is symbolic or concrete?
    • Why is lazy memory initialization important for performance?

    Book References:

    • angr documentation - Core Concepts: States
    • angr documentation - Top-Level Interfaces: Simulation Managers
  6. Control Flow Graph (CFG) Recovery
    • angr builds CFG by discovering basic blocks and edges
    • Static CFG (fast, incomplete) vs. Dynamic CFG (slower, more accurate)
    • Function boundaries, indirect jumps, and obfuscation challenges

    Guiding Questions:

    • How does angr discover code in a stripped binary without symbols?
    • What makes indirect jumps (jmp rax) hard for CFG recovery?
    • Why might a packed binary confuse CFG analysis?

    Book References:

    • “Practical Binary Analysis” - Chapter 6.3: Control Flow Graph Recovery
    • angr documentation - Advanced Topics: CFG
  7. Symbolic Execution Strategies
    • DFS (Depth-First Search): go deep, might miss states
    • BFS (Breadth-First Search): explore level-by-level, memory intensive
    • Veritesting: smart path merging to reduce state explosion
    • Custom exploration: prioritize based on distance to target

    Guiding Questions:

    • When would DFS find a solution faster than BFS?
    • What’s path merging and why does it help with loops?
    • How do you write a custom exploration technique?

    Book References:

    • angr documentation - Simulation Managers: Exploration Techniques
    • Paper: “Enhancing Symbolic Execution with Veritesting” (Avgerinos et al., 2014)
  8. Hooking and Environment Interaction
    • Replacing library functions with Python summaries (SimProcedures)
    • Modeling system calls without actually executing them
    • Creating simplified environments for complex functions

    Guiding Questions:

    • Why hook strlen() instead of symbolically executing it?
    • How do you model a network socket in symbolic execution?
    • What happens if you don’t hook malloc() and the program allocates GB of memory?

    Book References:

    • angr documentation - Advanced Topics: SimProcedures
    • angr documentation - Examples: Hooking
  9. Constraint Optimization and Caching
    • Incremental solving: reuse previous solutions
    • Constraint simplification before sending to Z3
    • State cloning and copy-on-write optimizations

    Guiding Questions:

    • Why is solving x == 5 much faster than x * y + z == 1000?
    • How does angr cache solver results to speed up analysis?
    • What’s the cost of cloning a state with gigabytes of symbolic memory?

    Book References:

    • angr documentation - Solver Engine
    • Academic paper on symbolic execution optimization techniques
  10. Concretization Strategies
    • When symbolic execution can’t continue symbolically (e.g., symbolic jump target)
    • Concretization: picking a concrete value for a symbolic variable
    • Strategies: max/min value, single solution, all solutions (fork)

    Guiding Questions:

    • What happens when a program does jmp [symbolic_address]?
    • Why might concretization cause you to miss valid paths?
    • How do you decide which value to concretize to?

    Book References:

    • angr documentation - Solver: Concretization Strategies

Questions to Guide Your Design

  1. How do you choose the right starting point for symbolic execution?
    • Start at entry point (complete but slow) vs. start at function of interest (fast but requires setup)
    • How do you set up registers/memory when starting mid-program?
  2. How do you write a find condition that’s neither too broad nor too narrow?
    • Too broad: “any state that prints output” (finds wrong solution)
    • Too narrow: “state at address 0x401234” (misses alternate paths)
    • Consider: output strings, register values, success indicators
  3. What’s your strategy for dealing with loops in symbolic execution?
    • Hook and skip them? Bound the iteration count? Use loop summarization?
    • When is it safe to unroll a loop symbolically?
  4. How do you handle programs that read from files or network?
    • Model file contents as symbolic variables
    • Create SimFiles with symbolic or concrete content
    • What if the file size itself affects control flow?
  5. When should you use hooks vs. letting angr execute the real code?
    • Hook when: function is complex (encryption), irrelevant (logging), or environment-dependent (network)
    • Don’t hook when: function contains target logic, or you need exact behavior
  6. How do you extract useful information from an “avoided” state?
    • Sometimes you want to know why a path was avoided (e.g., failed authentication)
    • Can you extract constraints from avoided states to understand preconditions?
  7. How would you use angr to find buffer overflow vulnerabilities?
    • Create symbolic buffer, look for states where return address is symbolic
    • Check if constraints allow attacker-controlled values in RIP/EIP
  8. What’s the difference between angr and a fuzzer like AFL++?
    • angr: deterministic, finds exact inputs, but slow and suffers path explosion
    • AFL++: probabilistic, fast, but might miss rare conditions
    • When would you use one over the other?

Thinking Exercise

Exercise 1: Understanding Symbolic Constraints

Consider this simple program:

int check_password(char *input) {
    if (input[0] == 'P' && input[1] == 'W' && input[2] - input[3] == 5) {
        return 1;  // Success
    }
    return 0;  // Fail
}

If input is symbolic, answer:

  1. What constraint is added after the first comparison (input[0] == 'P')?
  2. What are ALL the constraints accumulated by the time we reach return 1?
  3. Give one concrete input that satisfies these constraints (besides “PW…”).
  4. How many possible concrete inputs exist? (Hint: think about input[2] and input[3])

Exercise 2: Path Explosion Calculation

Consider this code:

for (int i = 0; i < N; i++) {
    if (input[i] == 'A') {
        process_A();
    } else {
        process_B();
    }
}

Questions:

  1. How many paths exist for N=5?
  2. How many paths for N=20?
  3. If each state takes 1 second to solve, how long for N=30?
  4. What techniques could angr use to reduce this explosion?

Exercise 3: Writing a Find Condition

You’re analyzing a crackme that prints either “Correct password!” or “Try again.” to stdout. Write the angr find and avoid conditions:

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

Consider:

  • Should you search for output strings? Address? Register values?
  • What if the program prints both messages under different conditions?
  • How do you avoid false positives?

Exercise 4: Designing a Hook

The target program calls strlen(user_input) and you want to hook it for performance:

@proj.hook(strlen_address)
def strlen_hook(state):
    # Your implementation here
    pass

Questions:

  1. How do you get the string pointer from the function argument?
  2. How do you calculate symbolic string length?
  3. What do you return and where do you put it?
  4. What edge cases might break your hook?

Exercise 5: Debugging Symbolic Execution

You run angr on a crackme and it explores 10,000 states in 5 minutes without finding a solution. What do you check?

  1. Is path explosion happening? (Check active/deadended states count)
  2. Is the find condition correct? (Print state info when states reach suspected area)
  3. Are you starting from the right place?
  4. Should you add hooks to skip expensive functions?
  5. Are there loops that need bounding?

Write a debugging checklist for troubleshooting angr scripts.

The Interview Questions They’ll Ask

  1. “Explain symbolic execution to someone who only knows basic programming.”
    • Expected Answer: “Instead of running a program with one specific input like ‘hello’, symbolic execution runs it with a placeholder ‘X’ that represents ANY possible input. As the program runs, it tracks rules like ‘if X[0] == ‘h’ then take this branch, else take that branch’. At the end, it uses a math solver to find what X should be to reach a specific goal, like printing ‘success’.”
  2. “What’s the path explosion problem and how do you mitigate it?”
    • Expected Answer: Each branch doubles possible paths (2ⁿ growth). Loops amplify this massively. Mitigations: (1) Bound loop iterations. (2) Use avoid to prune uninteresting paths. (3) Path merging (veritesting). (4) Start execution closer to target. (5) Hook complex functions. (6) Use exploration strategies like DFS or prioritized search. (7) Set state limits and timeouts.
  3. “When would you use symbolic execution instead of fuzzing?”
    • Expected Answer: Use symbolic execution when: (1) You need to find exact input for rare condition (e.g., exact password, magic number). (2) Path requires multiple constraints (fuzzing unlikely to hit). (3) You need proof input exists vs. probabilistic search. Use fuzzing when: (1) Fast results needed. (2) Program is large (path explosion). (3) Target is common bugs (crashes) not specific paths.
  4. “How does angr use Z3 solver?”
    • Expected Answer: angr accumulates constraints as path conditions (e.g., x[0] == 'P' AND x[1] == 'W' AND x[2] > 100). When you ask for a solution, angr converts these to Z3’s bitvector logic and asks “is this satisfiable?” Z3 uses SMT solving algorithms to either find values that satisfy all constraints, or prove none exist.
  5. “You’re symbolically executing a program and angr hangs. What do you do?”
    • Expected Answer: (1) Check state counts - are active states growing infinitely? (2) Look for unbounded loops in source/assembly. (3) Enable debug logging to see where it’s stuck. (4) Try different exploration strategy (DFS vs BFS). (5) Add hooks to skip expensive functions. (6) Set state limits (max_states parameter). (7) Check if solver is the bottleneck (complex constraints). (8) Start execution closer to target to reduce state space.
  6. “What’s the difference between angr’s static CFG and dynamic CFG?”
    • Expected Answer: Static CFG (CFGFast): analyzes binary without execution, fast, incomplete (misses computed jumps, self-modifying code). Uses pattern matching for function prologue/epilogue. Dynamic CFG (CFGEmulated): traces execution symbolically, slower, more accurate, finds code through actual control flow. Use static for quick overview, dynamic for precision.
  7. “How would you use angr to find a buffer overflow?”
    • Expected Answer: (1) Create symbolic buffer as input. (2) Track stack pointer and return address. (3) Look for states where return address contains symbolic bits (means we control it). (4) Check if constraints allow attacker values (not just symbolic). (5) Use solver to generate overflow payload. (6) Alternatively: look for states where rip/eip is symbolic, or where invalid memory access occurs.
  8. “Explain what happens when you hit a symbolic jump target (jmp [symbolic_address]).”
    • Expected Answer: angr can’t symbolically execute jump to unknown location. It must concretize: choose a concrete value for the address. Strategies: (1) Try all possible values (forks states - explosion!). (2) Use concretization strategy (max, min, or random value). (3) Constrain address to valid code region. (4) This can cause path loss if you concretize to wrong value. Ideally, constrain jump target based on prior analysis.
  9. “How do angr hooks (SimProcedures) work and when should you use them?”
    • Expected Answer: Hooks replace function execution with Python code. When PC reaches hooked address, angr calls Python instead of executing instructions. Use when: (1) Function is expensive (crypto). (2) Environment interaction (file I/O, network). (3) Known behavior (strlen, memcpy) - summarize rather than execute. How: Read arguments from state.regs/memory, compute result, write to return value, adjust stack/PC. Example: hook strcmp to just compare symbolic strings symbolically without executing assembly.
  10. “What’s veritesting and why is it useful?”
    • Expected Answer: Veritesting merges multiple execution paths into a single state using conditional expressions. Instead of forking at each branch (exponential states), it creates merged state: result = if(cond) then A else B. Dramatically reduces path explosion for straight-line code with many branches. Most useful for code with many conditionals but few loops. Enabled with simgr.use_technique(angr.exploration_techniques.Veritesting()).

Books That Will Help

Topic Book Chapter/Section Why It Matters
Symbolic Execution Fundamentals “Practical Binary Analysis” by Dennis Andriesse Ch. 11.4: Symbolic Execution Introduction to symbolic execution concepts
Binary Analysis Foundation “Practical Binary Analysis” Ch. 6: Disassembly and Binary Analysis Fundamentals Understand what angr is analyzing
Dynamic Binary Instrumentation “Practical Binary Analysis” Ch. 11: Principles of Dynamic Binary Instrumentation Related techniques (Pin, DynamoRIO)
Control Flow Graph Recovery “Practical Binary Analysis” Ch. 6.3: Control Flow Graphs How angr discovers program structure
Assembly and Instruction Sets “Low-Level Programming” by Igor Zhirkov Ch. 3-5: Assembly Language Understanding what VEX IR represents
Computer Architecture “Computer Systems: A Programmer’s Perspective” Ch. 3: Machine-Level Representation Foundation for understanding execution
Integer Representations “Computer Systems: A Programmer’s Perspective” Ch. 2: Representing and Manipulating Information Understand bitvector logic in Z3
Memory and Addressing “Computer Systems: A Programmer’s Perspective” Ch. 9: Virtual Memory How angr models memory
Optimization Techniques “Computer Systems: A Programmer’s Perspective” Ch. 5: Optimizing Program Performance Understanding why some code paths are expensive
Linking and Loading “Computer Systems: A Programmer’s Perspective” Ch. 7: Linking How angr loads binaries
Dynamic Analysis “Practical Malware Analysis” by Sikorski & Honig Ch. 3: Basic Dynamic Analysis Complementary dynamic analysis techniques
Control Flow Analysis “Practical Malware Analysis” Ch. 4: A Crash Course in x86 Disassembly Reading assembly to understand paths
Anti-Analysis Bypass “Practical Malware Analysis” Ch. 16: Anti-Debugging Using angr to bypass protections
Constraint Solving Basics Z3 Tutorial Documentation Entire tutorial Understanding the solver angr uses
Academic Foundation Academic Paper: “A Survey of Symbolic Execution Techniques” (Baldoni et al., 2018) Full paper Deep dive into symbolic execution research
Veritesting Technique Paper: “Enhancing Symbolic Execution with Veritesting” (Avgerinos et al., 2014) Full paper Advanced technique for path merging
angr Framework angr Official Documentation Core Concepts, Examples, Advanced Topics Comprehensive guide to angr usage

Common Pitfalls and Debugging

Problem 1: “Your interpretation does not match runtime behavior”

  • Why: Static analysis can hide runtime-resolved addresses, lazy binding, and input-dependent branches.
  • Fix: Reproduce the path with debugger or tracer, then compare static assumptions against live register/memory state.
  • Quick test: Run the same sample through both your static workflow and a debugger transcript, and confirm control-flow decisions align.

Problem 2: “Tool output is inconsistent across machines”

  • Why: ASLR, tool version drift, and different binary build flags (PIE, RELRO, symbols stripped) change observed addresses and metadata.
  • Fix: Pin tool versions, capture checksec/metadata, and document environment assumptions in your report.
  • Quick test: Re-run analysis in a container or VM with pinned tools and compare hashes of generated outputs.

Problem 3: “Analysis accidentally executes unsafe code”

  • Why: Dynamic workflows run binaries in host context without sufficient isolation.
  • Fix: Use disposable snapshots, no-network execution, and non-privileged users for all unknown samples.
  • Quick test: Validate isolation controls first (network disabled, snapshot active, unprivileged user), then execute sample.

Definition of Done

  • Core functionality works on reference inputs
  • Edge cases are tested and documented
  • Results are reproducible (same binary, same tools, same report output)
  • Analysis notes clearly separate observations, assumptions, and conclusions
  • Lab safety controls were applied for any dynamic execution

4. Solution Architecture

Input Artifact -> Parse/Decode -> Analysis Engine -> Validation Layer -> Report

Design each stage so intermediate artifacts are inspectable (JSON/text/notes), which makes debugging and peer review much easier.

5. Implementation Phases

Phase 1: Foundation

  • Define input assumptions and format checks.
  • Produce a minimal golden output on one known sample.

Phase 2: Core Functionality

  • Implement full analysis pass for normal cases.
  • Add validation against an external ground-truth tool.

Phase 3: Hard Cases and Reporting

  • Add malformed/edge-case handling.
  • Finalize report template and reproducibility notes.

6. Testing Strategy

  • Unit-level checks for parser/decoder helpers.
  • Integration checks against known binaries/challenges.
  • Regression tests for previously failing cases.

7. Extensions & Challenges

  • Add automation for batch analysis and comparative reports.
  • Add confidence scoring for each major finding.
  • Add export formats suitable for CI/security pipelines.

8. Production Reflection

Map your project output to a production analogue: what reliability, observability, and security controls would be required to run this continuously in an engineering organization?