2019 seccon follow-me angr

solve.py

import angr
import claripy
import json
import sys
import IPython

with open('calc.trace_15993a223f9b4a3799251447a8f8198f1ff787ed') as f:
    trace = json.loads(f.read())
    trace = trace[4:-1]

proj = angr.Project('./calc_8e4bdd821b86bebbfa6c5191bfddd40dbb120916',
                    auto_load_libs=False,
                    main_opts={'base_addr':0x55f6b4d44000},
)

sym_arg_size = 200 # Length in Bytes because we will multiply with 8 later
sym_arg = claripy.BVS('sym_arg', 8*sym_arg_size)
argv = [proj.filename]
argv.append(sym_arg)

state = proj.factory.entry_state(args=argv)
simgr = proj.factory.simulation_manager(state)

def step(simgr):
    """
    Step to the next jump, skip all calls and returns
    """
    simgr.step()
    while simgr.active[0].history.jumpkinds[-1] != 'Ijk_Boring':
        simgr.step()

for i in range(5):
    # we want to start at main
    step(simgr)

trace = trace[5:] # we want to start in main
assert int(trace[0]['inst_addr'], 16) == 0x55f6b4d44eae

trace = trace[:-4] # we skip everything after main returns
assert int(trace[-1]['inst_addr'], 16) == 0x55f6b4d44610

while len(trace) != 0:
    step(simgr)
    print(len(trace), "to go")
    el, trace = trace[0], trace[1:]
    next_address = int(el['inst_addr'], 16)

    p_addr = proj.factory.block(simgr.active[0].history.addr).capstone.insns[-1].address
    print(hex(p_addr), hex(next_address))
    assert p_addr == next_address

    bb = proj.factory.block(next_address)

    ins = bb.capstone.insns[-1]
    assert ins.address == next_address

    next_i = ins.address+ins.size

    # TODO this is technically wrong, as they could jump to the same instruction
    if el['branch_taken']:
        simgr.stash(filter_func=lambda state: state.addr == next_i, from_stash='active', to_stash='avoid')
    else:
        simgr.stash(filter_func=lambda state: state.addr != next_i, from_stash='active', to_stash='avoid')

    assert len(simgr.active) == 1
    simgr.drop(stash='avoid')

IPython.embed()
print(simgr.active[0].solver.eval(sym_arg, cast_to=bytes))