angr — let the solver read the check for you

Here's a crackme: it reads a key, mangles it through a few rounds of arithmetic, and prints correct or nope. You could reverse the mangling by hand and write an inverse. Or you can mark the input as an unknown, tell a symbolic execution engine "find a path that reaches correct and avoids nope," and let the constraint solver work out what bytes satisfy every comparison on the way.

mark the input unknown, name the two exits#

angr explores the binary's paths over symbolic values. You give it a symbolic input, a find address (the print of correct) and an avoid address (the failure print), and it searches for a state that reached find. Pull the addresses out of the disassembly first:

1
2
3
4
5

  4011d2: lea  rdi, [rip+0xe2a]   ; "correct"   <- find
  4011d9: call puts
  ...
  401205: lea  rdi, [rip+0xe0b]   ; "nope"      <- avoid
  40120c: call puts

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

import angr, claripy
proj  = angr.Project("./crackme", auto_load_libs=False)

flag  = claripy.BVS("flag", 8 * 16)             # 16 unknown bytes
state = proj.factory.full_init_state(stdin=flag)
for b in flag.chop(8):                           # keep it printable
    state.solver.add(b >= 0x20, b <= 0x7e)

simgr = proj.factory.simulation_manager(state)
simgr.explore(find=0x4011d2, avoid=0x401205)     # the two addresses above
print(simgr.found[0].posix.dumps(0))             # the stdin that reaches "correct"

explore walks both branches at every comparison, accumulating constraints (input[3] ^ 0x5a == 0x31, …). The moment a state reaches find, the solver has a system of equations with one satisfying assignment — your key — and posix.dumps(0) prints the exact stdin that produced it.

1
2
3

$ python3 solve.py
b'r3v_by_c0nstr4int'
correct

the part the tutorials skip: when it won't#

Symbolic execution is not magic; it's a search, and the search blows up:

• Path explosion. Every input-dependent branch forks the state. A loop over your 16 bytes with a branch inside is 2^16 paths — minutes to never. Hook the hot function with a SimProcedure, or explore toward an address past the loop, or constrain bytes up front (as above) to prune dead branches.
• Crypto and hashes. A real hash (SHA-256, AES) produces constraints the SMT solver can't invert in any human timescale — that's the point of a hash. If the check is sha256(key) == const, angr will grind forever; reverse it by hand or attack the key space instead.
• Environment. Syscalls, threading, rdtsc, and libc internals can derail the engine; auto_load_libs=False plus SimProcedure stubs for the noisy calls keeps it on the part you actually care about.

When the check is pure arithmetic over your input, angr feels like cheating — you describe the destination and it derives the path. The skill that matters is recognising the cases where the solver can't help, and not burning an afternoon watching the active-state count climb.