Symbolic Execution with angr

Dynamic Taint Analysis answered questions about one real run: you gave the program a concrete input, let it execute once, and watched which bytes of that single run reached a sink. That is precise and cheap, but it only ever tells you about the path the program happened to take. If the question is "is there any input that reaches this line", or "what exact string does this comparison want", running the program with guesses is not analysis, it is luck.

Symbolic execution answers that question directly. Instead of a concrete value, an input is represented by a symbol — a name with no fixed value yet. As the symbol flows through the program, every branch that depends on it adds a constraint, and an SMT solver can tell you whether some concrete value would satisfy all the constraints collected on a given path, and what that value is. Done exhaustively, this explores every path at once instead of one run at a time. This lesson covers the model, the practical problem that model runs into on real binaries, and angr, the framework that has become the default way analysts reach for it.

Symbols, constraints and a solver

Take a routine that checks eight bytes of input one at a time:

int check(char *buf) {
    if (buf[0] != 0x13) return 0;
    if (buf[1] != 0x37) return 0;
    /* ... six more comparisons ... */
    return 1;   /* only reached if every byte matched */
}

Concretely running this with a guessed input almost always returns 0 after the first comparison, and tells you nothing about the seven you never reached. Symbolically, buf is eight symbols, b0 through b7, each free to be any byte. Executing the routine still walks the code exactly like before, but each branch is now a fork:

• Taking the != branch at the first if adds the constraint b0 ≠ 0x13 to that path, and execution continues down the "return 0" path.
• Taking the other branch adds b0 = 0x13 instead, and continues into the second comparison, which forks again.

By the time execution reaches return 1, that single path carries the conjunction of all eight equality constraints — the path constraint — and only one path in the whole tree reaches it. Asking a solver "give me values for b0..b7 that satisfy this path's constraint" is the same kind of question a solver answers about a Sudoku puzzle: is this system satisfiable, and if so, what is a solution? The tool that does this, an SMT solver (Satisfiability Modulo Theories — Z3 is the one angr uses), is the engine underneath every angr result in this lesson. Symbolic execution's job is producing the constraints; the solver's job is producing an answer.

Note: The glossary defines symbolic execution the same way and names the same failure mode you are about to meet — read the symbolic execution entry if you have not already.

Path explosion

The routine above has eight sequential branches and one interesting path. Real code rarely cooperates. A loop that runs up to n times forks at every iteration; a routine with twenty independent if statements has up to 2²⁰ paths; a call into a parsing library multiplies that by however many paths it contains. The number of paths grows exponentially with the number of branches on the way, a problem with a name: path explosion. Explore naively and you run out of memory maintaining thousands of divergent states, long before you reach the one path you wanted.

Nothing about the theory fixes this — it is a property of branching code, not a flaw in an implementation — so every practical symbolic execution tool is really a set of strategies for not exploring paths you do not need.

Staying practical: concolic execution and targeted search

The first strategy is to stop being purely symbolic. Concolic execution ("concrete + symbolic") runs the program on a real concrete input, and tracks symbolic constraints alongside that one concrete run, the same way a taint tracker rides alongside execution. At each branch, the concrete run only ever goes one way, but the tool records the constraint it could have negated, and can later ask the solver for an input that flips exactly that branch to reach a new path on the next concrete run. This is how tools like Driller combine fuzzing (fast, concrete, finds most of a program's shallow paths for free) with symbolic execution (spent only on the few deep branches a fuzzer gets stuck on, such as a magic-value comparison it will never guess by mutation). Neither technique alone would find that path efficiently; the combination targets symbolic reasoning at exactly the branches that need it.

The second strategy, which matters most for how you will actually drive angr, is not exploring blindly at all. Rather than symbolically executing every instruction from a program's start to its end, you choose a starting address, a target address, and one or more addresses to give up on. The engine then only keeps states that are still making progress toward the target, discarding — or never forking down — the rest. This does not remove path explosion in general, but for a single, well-scoped question ("what reaches this line") it keeps the search small enough to answer.

angr basics

angr loads a binary with its own loader (CLE), builds an intermediate representation of the code with VEX (the same IR Valgrind uses), and runs symbolic execution over that IR rather than raw x86 bytes, so the same analysis code works across architectures. Four pieces matter for everyday use.

Loading and the CFG. angr.Project("sample.exe") loads a binary and its imports. proj.analyses.CFGFast() recovers a control-flow graph by static analysis — fast, but it can miss or misplace blocks behind indirect jumps, which is exactly what control-flow flattening and opaque predicates are built to cause. The CFG is useful for orientation (where are the functions, what calls what) even when it is incomplete; it is not what finds your answer.

Simulation state. A SimState is one point in the exploration: register values, memory contents, and the accumulated path constraint, where any of those can be concrete or symbolic. proj.factory.blank_state(addr=X) creates a mostly-empty one starting execution at X; entry_state() starts at the binary's real entry point with a modelled environment (argv, a fake stack, initialised libc state) for when you want a normal run instead of a bare function.

Exploration. A SimulationManager steps one or many states forward together. simgr.explore(find=A, avoid=B) steps every active state, splitting it at each branch, and sorts the results into simgr.found (a state that reached A), simgr.deadended, and states dropped because they reached B. This is the "targeted search" strategy from the previous section, expressed as one line.

SimProcedures. Stepping symbolically through strcmp's actual assembly — every byte compared, every loop iteration — wastes an enormous amount of the search for a function whose effect you already know. angr ships SimProcedures: Python models of common library functions (strcmp, memcpy, malloc, and hundreds of others) that angr calls instead of entering the real code. strcmp becomes a handful of solver constraints comparing two buffers, computed instantly, rather than thousands of symbolically-executed instructions. Custom hooks work the same way: point proj.hook(address, procedure) at any address you would rather summarise than step through — a licence-server call you know always returns 1 in your lab, for instance — and exploration skips straight past it.

Analyst use cases

Recovering a hidden comparison. The classic case, and the one the lab below builds: a sample compares input against a constant, a hash, or a derived value before doing something interesting, and you want the value without reverse-engineering the comparison by hand. Point explore at the address just past the comparison's success branch, avoid the failure branch, and read the solution back off the symbolic input.

Working out which branches in a flattened or predicated dispatcher are real. Control-flow flattening and opaque predicates are designed to make a disassembler's static view show far more possible transitions than the code actually takes at runtime. Symbolically executing the dispatcher and asking, for each candidate successor, "is there a path constraint that reaches it" — or simply observing which successors CFGFast treats as live once you seed exploration from a real entry state — separates the predicates that are always true or always false from the ones that genuinely depend on input, which is most of the work of seeing through the obfuscation.

Confirming a suspected input, cheaply. Even without solving from scratch, you can load a candidate value into a state, run it concretely-in-angr to a target address, and check whether the path constraint is satisfied — a sanity check that costs nothing next to re-running the real sample.

Honest limits

Symbolic execution is not a substitute for the rest of this curriculum, and overselling it leads to wasted afternoons. It struggles with unbounded loops (a decompression loop over attacker-controlled length forks once per iteration, with no natural place to stop), with anything that leans on real environment state (the registry, the network, the filesystem — each needs its own model or a SimProcedure before angr's answers mean anything), and with floating point and heavy SIMD, which VEX and the constraint solver support less completely than integer arithmetic. It is also not a replacement for the debugger: reading what a routine does at all is still a disassembly and control-flow job. Reach for angr when you can state the question as "is there an input that reaches here, avoiding there" about a bounded piece of code — a parser, a check, a dispatcher — not as a way to fully automate reading a sample.

Lab: recover a hidden comparison with angr

You will assemble an eight-byte comparison routine — the shape from the opening example — and use angr to recover the exact input it accepts, without reading the comparison by hand. Nothing here runs a real sample; check is a routine you are writing yourself for the exercise.

1. Create a working directory and a virtual environment:

   mkdir m11d && cd m11d
   python3 -m venv venv
   ./venv/bin/pip install angr pyelftools

   (angr pulls in claripy, its symbolic-value library, and Z3 as its solver backend automatically.)

2. Save the routine as check.s. It takes a pointer to an 8-byte buffer in rdi and returns 1 in eax only if every byte matches a fixed value, the same shape as any "does this input satisfy a hidden check" routine you will meet in real samples:

   # check.s - return 1 iff the 8 bytes at [rdi] equal a fixed key
       .intel_syntax noprefix
       .text
       .globl check
   check:
       cmp   byte ptr [rdi+0], 0x13
       jne   fail
       cmp   byte ptr [rdi+1], 0x37
       jne   fail
       cmp   byte ptr [rdi+2], 0x42
       jne   fail
       cmp   byte ptr [rdi+3], 0x69
       jne   fail
       cmp   byte ptr [rdi+4], 0x21
       jne   fail
       cmp   byte ptr [rdi+5], 0x0a
       jne   fail
       cmp   byte ptr [rdi+6], 0x55
       jne   fail
       cmp   byte ptr [rdi+7], 0x7e
       jne   fail
   success:
       mov   eax, 1
       ret
   fail:
       xor   eax, eax
       ret

   clang -target x86_64-linux-gnu -c check.s -o check.o

   As in earlier labs, Clang's integrated assembler targets x86-64 Linux from any host; you only need the object file's raw .text bytes and its symbol table, not a linked executable.

3. Save solve.py. It pulls the routine's machine code and the addresses of the success and fail labels straight from the object file, loads the code into angr as a bare blob, marks the 8 input bytes symbolic, and explores toward success while avoiding fail:

   # solve.py - recover the input `check()` accepts, without reading the comparison
   import angr
   import claripy
   from elftools.elf.elffile import ELFFile
   
   obj = ELFFile(open("check.o", "rb"))
   code = obj.get_section_by_name(".text").data()
   symtab = obj.get_section_by_name(".symtab")
   labels = {s.name: s["st_value"] for s in symtab.iter_symbols()
             if s.name in ("success", "fail")}
   
   BASE, BUF = 0x10000, 0x20000
   proj = angr.load_shellcode(code, arch="AMD64", load_address=BASE)
   
   state = proj.factory.blank_state(addr=BASE)
   state.regs.rdi = BUF
   input_bytes = [claripy.BVS(f"b{i}", 8) for i in range(8)]
   for i, b in enumerate(input_bytes):
       state.memory.store(BUF + i, b)          # one symbolic byte per address
   
   simgr = proj.factory.simgr(state)
   simgr.explore(find=BASE + labels["success"], avoid=BASE + labels["fail"])
   
   found = simgr.found[0]
   solution = bytes(found.solver.eval(b) for b in input_bytes)
   print("recovered input:", solution.hex(" "))

4. Run it:

   ./venv/bin/python solve.py

   Every one of the eight branches is a straightforward equality check with no other freedom on the path to success, so the path constraint collected by the time exploration reaches that label pins all eight symbolic bytes to exactly one value each — the solver has nothing left to choose. The script prints:

   recovered input: 13 37 42 69 21 0a 55 7e

   which is precisely the sequence check was written to require: angr never looked at the cmp immediates as "the answer", it derived them by solving the constraints your jne chain produced. Confirm it by hand — compile a small harness that calls check() with those exact bytes and with a wrong guess, and see that only the recovered value returns 1.

5. Break exploration on purpose. Comment out the avoid= argument and re-run. simgr.explore without avoid still stops as soon as it reaches find, but nothing is telling it to give up on the failing branches quickly, so on a longer or looped comparison this is where a search that looked instant starts to feel path explosion — watch simgr between steps (simgr.active, simgr.deadended) to see the state count grow.

Questions to answer: If check looped over a length byte supplied by the caller instead of a fixed 8, what would you need to bound before exploring, and why would an unbounded version never finish? If two of the eight comparisons were replaced by one call to a modelled function like memcmp, would you expect angr to explore faster or slower, and why? Where in this lab did the SMT solver actually get invoked — was it once at the end, or could explore need it at every branch along the way to decide which branch is even reachable?

Key takeaways

• Symbolic execution replaces concrete inputs with symbols, accumulates a path constraint at every branch, and asks an SMT solver (Z3, in angr's case) whether some concrete input satisfies that path.
• Path explosion — the exponential blow-up of paths with branches — is a property of the technique, not an implementation flaw; concolic execution (symbolic reasoning riding along a concrete run) and targeted find/avoid search are how tools stay practical.
• angr loads a binary with CLE, lifts it to VEX, and represents each point in a search as a SimState; simgr.explore(find=..., avoid=...) is the everyday way to ask "is there a path here, not there".
• SimProcedures summarise library calls with their effect instead of stepping through their real code, which is most of what keeps angr's search tractable on real binaries.
• Reach for it on a bounded question about a specific check or dispatcher — recovering a hidden comparison, or separating live branches from decoy ones in a flattened control-flow graph — not as a way to fully automate reading a sample; unbounded loops and real environment interaction still need modelling or a different tool.