Symbolic execution with angr

Angr is in Python 3, create a virtualenv and `pip install` it. Best is to combine with static analysis, i.e. find things in Ghidra.

Create a project:

proj = angr.Project("./Stone")

Get the base address of the binary:

base = proj.loader.main_object.mapped_base

Create states from which to start symbex

# Use the entry state
# starts from main entry point unless addr is specified
s = proj.factory.entry_state()

# Use a blank state
# have to set regs etc. yourself
s = proj.factory.blank_state(addr=addr)

Create buffers with constraints:

buf_size = 80 # bytes
buf = claripy.BVS("buf", buf_size*8) # symbolic, not actual value

# Add constraints for buffer values to be ascii
for byte in buf.chop(8):
    state.add_constraints(byte >= 0)
    state.add_constraints(byte <= 127)

buf_addr = 0xB00B5 # some unused address

Set up args for a function:

# Prepare for a function call computing one buffer from another
# e.g. calculate_buffer(char *dst, char *src)

state.memory.store(dst_buf_addr, dst_buf_bvs)
state.memory.store(src_buf_addr, src_buf_bvs)
# assuming arguments are passed in rdi,rsi,rdx...
state.regs.rdi = dst_buf_addr
state.regs.rsi = src_buf_addr

Run a simulation:

sim = proj.factory.simgr(state, veritesting=True) # veritesting speeds it up
sim.explore(find=GOOD_ADDR, avoid=BAD_ADDR)
# find and avoid can also be functions evaluating to a bool, or arrays

# to continue after a found state:
sim.unstash(from_stash="found", to_stash="active")
# and run explore again

Find solutions:

# This loop will raise angr.errors.SimUnsatError when no more solutions
while True:
    buf_in_memory = sim.found[0].memory.load(buf_addr, buf_size)

    # Get a solution, this will be an integer
    # You can add cast_to=bytes to get a bstring
    one_solution = sim.found[0].solver.eval(buf_in_memory)

    # Print it
    print(one_solution)

    # Add a constraint to avoid recomputing that solution
    sim.found[0].solver.add(buf_in_memory != one_solution)

Useful websites: