svattt2017_jharmony.py

import angr


def char(state, n):
    """Returns a symbolic BitVector and constrains it to printable chars
       for a given state."""
    vec = state.se.BVS('c{}'.format(n), 8, explicit_name=True)
    return vec, state.se.And(vec >= ord(' '), vec <= ord('~'))

def decrypt(state):
	state.regs.ecx = 0x690000

proj = angr.Project("jharmony.exe", load_options={"auto_load_libs":False})
proj.hook(0x4011EB, decrypt, length=5)
# create a state, begin at the check func
state = proj.factory.blank_state(addr=0x401061)
# put symbolic bitvectors at the buffer address (according to the disasm,
# it is at ebp-0x30, and from argc's condition its length is 30 bytes)
chrs = []
for i in xrange(32):
    c, cond = char(state, i)
    chrs += [c]
    state.memory.store(state.regs.ebp - 0x24 + i, c)
    if (i < 30):
    	state.add_constraints(cond)
    else:
    	state.add_constraints(c == 0)
# explore for success(), avoid fail()
state.memory.store(0x690000, 'BF86E2904742C3E795A091410580E4A0A2D3474584BFB1FDCD0718C667330000'.decode('hex'))
ex = proj.surveyors.Explorer(start=state, find=(0x401221,))
ex.run()
# print solution
flag = []
f = ex._f
for c in chrs:
    flag += [f.se.eval(c, cast_to=str)]
print ''.join(flag)