Create a gist now

Instantly share code, notes, and snippets.

@douggard /solve_magic.py Secret
Last active May 17, 2017

What would you like to do?
Manticore solution to the DEFCON quals challenge Magic
import sys
from manticore import Manticore
sys.path.append('/home/taxicat/work/binja/binaryninja/python/')
import binaryninja as binja
debug = True
LLIL_CALL = binja.LowLevelILOperation.LLIL_CALL
LLIL_CONST = binja.LowLevelILOperation.LLIL_CONST
def set_hooks(m, pc):
# pre branch
@m.hook(pc)
def write(state):
_pc = state.cpu.PC
_target = _pc + 0x14
if _target in m.context['values']:
if debug:
print 'Writing %s at %s...' % (chr(m.context['values'][_target]), hex(_pc))
state.cpu.write_register('RDI', m.context['values'][_target])
# print state.cpu
# negative branch
neg = pc + 0x6
@m.hook(neg)
def bail(state):
if debug:
print 'Abandoning state at %s...' % hex(neg)
state.abandon()
# target branch
target = pc + 0x14
@m.hook(target)
def solve(state):
_cpu = state.cpu
_target = _cpu.PC
_pc = _target - 0x14
# skip solver step if known
if _target in m.context['values']:
return
val = _cpu.read_register('RDI')
solution = state.solve_one(val)
values = m.context['values']
values[_target] = solution
m.context['values'] = values
target_order = m.context['target_order']
target_order.append(_target)
m.context['target_order'] = target_order
if debug:
print 'Reached target %s. Current key: ' % (hex(_target))
print "'%s'" % ''.join([chr(m.context['values'][ea]) for ea in m.context['target_order']])
def end_hook(m, end_pc):
@m.hook(end_pc)
def hook_end(state):
print 'GOAL:'
print "'%s'" % ''.join([chr(m.context['values'][ea]) for ea in m.context['target_order']])
m.terminate()
def symbolic(m, end_pc):
# hook every instruction using None as the address
@m.hook(None)
def hook_all(state):
# read an integer at the program counter
cpu = state.cpu
pc = cpu.PC
instruction = cpu.read_int(pc)
# check the instructions match
# cmp rdi, ??
# je +0xe
if (instruction & 0xFFFFFF == 0xff8348) and (instruction >> 32 & 0xFFFF == 0x0e74):
# the positive branch is 0x14 bytes from the beginning of the function
target = pc + 0x14
# if the target address is not seen yet
# add to list and declare solver hook
if target not in m.context['values']:
set_hooks(m, pc)
# set the end hook to terminate execution
end_hook(m, end_pc)
def concrete_pcs(m, pcs, end_pc):
# for each character checking function address
for pc in pcs:
@m.hook(pc)
def write(state):
# retrieve instruction bytes
_pc = state.cpu.PC
instruction = state.cpu.read_int(_pc)
# extract value from instruction
val = instruction >> 24 & 0xFF
# concretize RDI
state.cpu.write_register('RDI', val)
# store value for display at end_hook()
_target = _pc + 0x14
values = m.context['values']
values[_target] = val
m.context['values'] = values
target_order = m.context['target_order']
target_order.append(_target)
m.context['target_order'] = target_order
if debug:
print 'Reached target %s. Current key: ' % (hex(_pc))
print "'%s'" % ''.join([chr(m.context['values'][ea]) for ea in m.context['target_order']])
end_hook(m, end_pc)
def symbolic_pcs(m, pcs, end_pc):
for pc in pcs:
set_hooks(m, pc)
end_hook(m, end_pc)
def get_main(bv):
entry_fn = bv.entry_function
entry_block = entry_fn.low_level_il.basic_blocks[0]
assign_rdi_main = entry_block[11]
rdi, main_const = assign_rdi_main.operands
if rdi != 'rdi' or main_const.operation != LLIL_CONST:
raise Exception('Instruction `rdi = main` not found.')
main_addr = main_const.operands[0]
main_fn = bv.get_function_at(main_addr)
return main_fn
def get_checker(bv, main_fn):
entry_block = main_fn.low_level_il.basic_blocks[0]
call_checker = entry_block[14]
if call_checker.operation != LLIL_CALL:
raise Exception('Instruction `call(checker_fn)` not found.')
checker_const = call_checker.operands[0]
checker_addr = checker_const.operands[0]
checker_fn = bv.get_function_at(checker_addr)
return checker_fn
def get_pcs(path):
# load the final with Binary Ninja
bv = binja.BinaryViewType.get_view_of_file(path)
# retrieve the main function (shown below)
main_fn = get_main(bv)
# retrieve the checker function (shown below)
checker_fn = get_checker(bv, main_fn)
# retrieve the entry block of the checker function
entry_block = checker_fn.low_level_il.basic_blocks[0]
# if it's a call, extract the target offset
pc_addrs = [ea.operands[0].operands[0] for ea in entry_block if ea.operation == LLIL_CALL]
# add the base address to each extracted offset
pcs = [0x555555554000 + ea for ea in pc_addrs]
# iterate backward over the instructions of the last basic block
# find the instruction after the last call instruction
end_pc = entry_block[-1].address
for insn in list(entry_block)[::-1]:
if insn.operation == LLIL_CALL:
break
end_pc = insn.address
end_pc += 0x555555554000
return pcs, end_pc
def main():
path = sys.argv[1]
m = Manticore(path)
m.context['values'] = {}
m.context['target_order'] = []
pcs, end_pc = get_pcs(path)
# symbolic(m, end_pc)
concrete_pcs(m, pcs, end_pc)
# symbolic_pcs(m, pcs, end_pc)
m.run()
if __name__ == '__main__':
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment