Simple usage

import angr
import claripy

When you’re playing with angr, inevitably at the beginning you’ll have to load a binary of some form, you can do this the following way:

project_name = angr.Project("./<binary_name>")

Now angr works by using a lot of states which it steps through and investigates. To load our initial state we use the following command:

state = proj.factory.entry_state()

There are a few ways to load binaries, as one would imagine. We can add these as arguments to the state.

# To start execution from specific address (reduce runtime)
state = proj.factory.entry_state(addr=0xdeadbeef)

# Specify which architecture to use
state = proj.factory.entry_state(arch="amd64")

# Specify what to send with stdin
state = proj.factory.entry_state(stdin="test_stdin_string\n")

# How to send data with argv
state = proj.factory.entry_state(args=["./<binary_name>", argv1])

# Use unicorn engine! This is often a good way to go abouts
state = proj.factory.entry_state(add_options=angr.options.unicorn)

To actually change the state, or use it in anyway, a simulation manager is needed:

simgr = project_name.factory.simulation_manager(state)

Now to ACTUALLY change the state ( :D ), you need to use the simgr. You can do a few things:

# Step one instruction at a time
simgr.step()

# Find specific address, avoid another
simgr.explore(find=0xdeadbabe, avoid=0xcafebeef)

Solving and bitvectors

Python integers don’t have the same semantics as words on a CPU, e.g. wrapping on overflow, so we work with bitvectors.

.BVV = concrete BIT VECTOR VALUE

.BVS = BIT VALUE SYMBOLIC

db = state.solver.BVV(0xdeadbeef, 64) # Bitvector which angr uses 
state.solver.eval(db) # Python int representative of said bit vector

# Solving equation for an integer
x = state.solver.BVS("x", 64)

state.solver.add(x > 4)
state.solver.add(x <= 5)
print(f"\n[+] Trying to solve for x, satisfiable? {state.satisfiable()}\nAnswer is {state.solver.eval(x)}")

# Solving for a character (one byte)
n = state.solver.BVS("n", 8)

state.solver.add(n >= 0x41)
state.solver.add(n < 0x7f)
state.solver.add(n ^ 0x10 == 0x76)
solution = state.solver.eval(n)
print(f"\n[+] Trying to find the character that xored with 10 is 0x76.\nFound: {hex(solution)}")

Flag?

Using angr for CTF style challenges, a bit of reverse engineering knowledge is a must. For example you can try to find out the length of the flag, and use this, to setup a symbolic bit vector array of flag characters. Imagine the following pseudocode:

int flag(){
    if (strlen(flag) != 25)
        {
            return -1;
        }
    else
        {
        ...
        win();
        }
}

We know that the flag is 25 bytes. So we can set this as a constraint:

flag_chars = [claripy.BVS("flag_%d" % i, 8) for i in range(25)]
flag = claripy.Concat(*flag_chars)

Firstly we make the array of flag_chars, we set each flag_%d to have a size of 8 bits, which is a byte, which is a character. We can use this as an input to stdin in state:

_state(stdin=flag)

Now running we can explore for a success string:

simgr.explore(find=lambda s: b"Success string" in s.posix.dumps(1))
if "found" in str(simgr):
    s = simgr.found[0]
    print(s.posix.dumps(0)) #Flag
    print(s.posix.dumps(1)) #Input

Assuming we know that the flag’s last character is “q” we can also set this as a constraint:

state.solver.add(flag_chars[24] == ord("q"))

Appendix - Further reading

[¹] - Cheatsheet: https://github.com/bordig-f/angr-strategies/blob/master/angr_strategies.md

[²] - Constraint Solving and Symbolic Execution: https://flagbot.ch/lesson5.pdf

[³] - Documentation: https://angr.io/

[⁴] - Video by John Hammond: https://www.youtube.com/watch?v=RCgEIBfnTEI