angr

Reversing a binary line-by-line using IDA or GDB can take hours, especially when a challenge has tons of nested if/else checks, complex bitwise logic, or custom verification equations. What if you could just tell a tool: "Hey, find me the input that prints 'Valid License' and avoids 'Invalid License'", and let it solve the whole challenge for you automatically? That is exactly what angr is for! angr is a Python framework that performs Symbolic Execution to solve binary challenges.

What is Symbolic Execution?

To understand angr, let's compare how normal program execution works versus how symbolic execution works.

When you run a binary normally on your computer, you give it concrete input (for example, input = "password123"). The CPU executes instructions step-by-step using those exact concrete characters. If your password is wrong, the binary immediately branches to the failure path and exits.

With Symbolic Execution, instead of feeding the binary actual text or numbers, angr feeds the program symbols (think of them as algebraic variables like x, y, z). As the program executes through its machine code instructions, angr translates assembly into VEX IR, tracks everything that happens to those variables, and builds a system of mathematical equations (called constraints). When the binary hits a conditional branch (like if (check_key(input) == 1)), angr splits execution into two paths and hands those equations over to an SMT Solver (Z3 under the hood). The SMT solver analyzes the constraints and determines the exact concrete bytes needed to reach the success path!

Writing an angr Script

Installing angr is straightforward using Python's package manager: pip install angr claripy. claripy is the solver engine that angr uses to handle symbolic bitvectors and equations.

Writing an angr solver script usually takes between 15 and 25 lines of Python. First, we load the binary with proj = angr.Project("./binary", auto_load_libs=False). Setting auto_load_libs=False tells angr not to load external system libraries like libc.so, which speeds up performance significantly.

Next, we create symbolic variables to represent our unknown input bytes using claripy.BVS (Bit Vector Symbolic) and combine them with claripy.Concat. We create an initial execution state starting at the entry point with proj.factory.entry_state(stdin=...). If we know our key consists of printable ASCII characters, adding domain constraints (state.solver.add(c >= 0x20) and state.solver.add(c <= 0x7E)) tells angr to drop unprintable search paths, speeding up the solver dramatically!

Finally, we create a Simulation Manager (simgr = proj.factory.simgr(state)) and call simgr.explore(find=..., avoid=...). We can pass lambda functions matching stdout text (e.g. find=lambda s: b"Valid" in s.posix.dumps(1)) or exact memory addresses (e.g. find=0x401234). If a solution is found, we extract the bytes sent to stdin from simgr.found[0].posix.dumps(0).

Here is a complete, well-commented script template that you can copy, save as solve.py, and adapt for your CTF challenges:

#!/usr/bin/env python3
import angr
import claripy
import sys

BINARY = "./license"
KEY_LEN = 16

def solve():
    # 1. Load binary (auto_load_libs=False speeds up analysis)
    proj = angr.Project(BINARY, auto_load_libs=False)

    # 2. Create symbolic input bytes and append newline (\n)
    key_chars = [claripy.BVS(f"key_{i}", 8) for i in range(KEY_LEN)]
    stdin_content = claripy.Concat(*key_chars, claripy.BVV(ord('\n'), 8))

    # 3. Create initial state starting at entry point
    state = proj.factory.entry_state(
        stdin=angr.SimFileStream(name="stdin", content=stdin_content, has_end=True)
    )

    # 4. Add domain constraints (printable ASCII range)
    for c in key_chars:
        state.solver.add(c >= 0x20)
        state.solver.add(c <= 0x7E)

    # 5. Explore execution paths
    simgr = proj.factory.simgr(state)
    simgr.explore(
        find=lambda s: b"Valid" in s.posix.dumps(1),
        avoid=lambda s: b"Invalid" in s.posix.dumps(1)
    )

    # 6. Extract concrete solution
    if simgr.found:
        found_state = simgr.found[0]
        solution = found_state.posix.dumps(0)[:KEY_LEN]
        print(f"[+] Solution Found: {solution.decode()}")
        return solution
    else:
        print("[-] No valid path found.")
        sys.exit(1)

if __name__ == "__main__":
    solve()

Strengths and Limitations

angr feels like pure magic when it solves a challenge in seconds, but it has important limitations every reverse engineer should understand.

It is great for license checkers with complex mathematical conditions or bitwise transforms, binary mazes or crackmes with dozens of nested if/else checks, and obfuscated condition checks where manual reversing would take hours.

However, you should avoid angr when dealing with Cryptographic Hash Functions (like MD5, SHA256, or AES) because mathematical SMT solvers cannot efficiently invert cryptographic hashes. Trying to run angr through a hash function causes Path Explosion, where angr consumes gigabytes of RAM and runs indefinitely without finding a solution. You should also avoid angr on binaries with huge loops that run thousands of times.