Skip to main content

19. A Taste of Symbolic Execution with angr

In reverse engineering, symbolic execution is a technique that finds valid solutions by treating input conditions as variables and tracing execution paths. It is especially powerful for CTF crackmes and obfuscated branches.

Core Flow​

  • Load the binary: angr.Project("./target")
  • Model the input: claripy.BVS("stdin", 8*LEN)
  • Explore paths: simgr.explore(find=good, avoid=bad)
  • Extract the solution: found.posix.dumps(0)

Practical Tips​

  • Aggressive use of avoid can greatly reduce state explosion
  • Hooking library calls simplifies them and improves performance
  • Start with a short input length, identify the pattern, and then expand the search

angr is a tool for solving problems with mathematics when brute force is impractical. It becomes more effective as branching grows more complex.