diff options
Diffstat (limited to 'example/symbol_exec')
| -rw-r--r-- | example/symbol_exec/dse_crackme.py | 310 |
1 files changed, 310 insertions, 0 deletions
diff --git a/example/symbol_exec/dse_crackme.py b/example/symbol_exec/dse_crackme.py new file mode 100644 index 00000000..e08536f9 --- /dev/null +++ b/example/symbol_exec/dse_crackme.py @@ -0,0 +1,310 @@ +"""Example of DynamicSymbolicExecution engine use + +This example should run on the compiled ELF x86 64bits version of +"dse_crackme.c" + +""" + +#### This part is only related to the run of the sample, without DSE #### +import os +import subprocess +from collections import namedtuple +from pdb import pm + +from miasm2.jitter.csts import PAGE_READ, PAGE_WRITE +from miasm2.analysis.sandbox import Sandbox_Linux_x86_64 +from miasm2.expression.expression import * + +# File "management" +my_FILE_ptr = 0x11223344 +FInfo = namedtuple("FInfo", ["path", "fdesc"]) +FILE_to_info = {} +def xxx_fopen(jitter): + ''' + #include <stdio.h> + + FILE *fopen(const char *path, const char *mode); + ''' + global my_FILE_ptr + ret_addr, args = jitter.func_args_systemv(['path', 'mode']) + fname = jitter.get_str_ansi(args.path) + FILE_to_info[my_FILE_ptr] = FInfo(fname, open(fname)) + my_FILE_ptr += 1 + return jitter.func_ret_stdcall(ret_addr, my_FILE_ptr - 1) + +def xxx_fread(jitter): + ''' + #include <stdio.h> + + size_t fread(void *ptr, size_t size, size_t nmemb, FILE *stream); + ''' + ret_addr, args = jitter.func_args_systemv(['ptr', 'size', 'nmemb', 'stream']) + info = FILE_to_info[args.stream] + data = info.fdesc.read(args.size * args.nmemb) + jitter.vm.set_mem(args.ptr, data) + return jitter.func_ret_stdcall(ret_addr, len(data)) + +def xxx_fclose(jitter): + ''' + #include <stdio.h> + + int fclose(FILE *stream); + ''' + ret_addr, args = jitter.func_args_systemv(['stream']) + del FILE_to_info[args.stream] + return jitter.func_ret_stdcall(ret_addr, 0) + +# Create sandbox +parser = Sandbox_Linux_x86_64.parser(description="ELF sandboxer") +parser.add_argument("filename", help="ELF Filename") +options = parser.parse_args() +options.mimic_env = True +sb = Sandbox_Linux_x86_64(options.filename, options, globals()) + +# Init segment +sb.jitter.ir_arch.do_stk_segm = True +sb.jitter.ir_arch.do_ds_segm = True +sb.jitter.ir_arch.do_str_segm = True +sb.jitter.ir_arch.do_all_segm = True +FS_0_ADDR = 0x7ff70000 +sb.jitter.cpu.FS = 0x4 +sb.jitter.cpu.set_segm_base(sb.jitter.cpu.FS, FS_0_ADDR) +sb.jitter.vm.add_memory_page( + FS_0_ADDR + 0x28, PAGE_READ, "\x42\x42\x42\x42\x42\x42\x42\x42", + "Stack canary FS[0x28]") + +# Prepare the execution +sb.jitter.init_run(sb.entry_point) + + +#### This part handle the DSE #### +from miasm2.analysis.dse import DSEPathConstraint +from miasm2.analysis.machine import Machine + + +# File "management" + +class SymbolicFile(object): + """Symbolic file with read operation, returning symbolic bytes""" + + def __init__(self, fname): + self.fname = fname + self.position = 0 + self.max_size = os.stat(fname).st_size + self.gen_bytes = {} + self.state = "OPEN" + + def read(self, length): + assert self.state == "OPEN" + out = [] + for i in xrange(self.position, min(self.position + length, + self.max_size)): + if i not in self.gen_bytes: + ret = ExprId("SF_%08x_%d" % (id(self), i), 8) + self.gen_bytes[i] = ret + out.append(self.gen_bytes[i]) + self.position += 1 + + return out + + def close(self): + self.state = "CLOSE" + + +FILE_to_info_symb = {} +FILE_stream = ExprId("FILE_0", 64) +FILE_size = ExprId("FILE_0_size", 64) + +def xxx_fopen_symb(dse): + regs = dse.ir_arch.arch.regs + fname_addr = dse.eval_expr(regs.RDI) + mode = dse.eval_expr(regs.RSI) + assert fname_addr.is_int() + assert mode.is_int() + fname = dse.jitter.get_str_ansi(int(fname_addr)) + ret_addr = ExprInt(dse.jitter.get_stack_arg(0), regs.RIP.size) + + assert len(FILE_to_info_symb) == 0 + ret_value = FILE_stream + FILE_to_info_symb[ret_value] = SymbolicFile(fname) + + dse.update_state({ + regs.RSP: dse.eval_expr(regs.RSP + ExprInt(8, regs.RSP.size)), + dse.ir_arch.IRDst: ret_addr, + regs.RIP: ret_addr, + regs.RAX: ret_value, + }) + +def xxx_fread_symb(dse): + regs = dse.ir_arch.arch.regs + ptr = dse.eval_expr(regs.RDI) + size = dse.eval_expr(regs.RSI) + nmemb = dse.eval_expr(regs.RDX) + stream = dse.eval_expr(regs.RCX) + + assert size.is_int() + assert nmemb.is_int() + + # Fill the buffer with symbolic bytes + update = {} + sf = FILE_to_info_symb[stream] + data = sf.read(int(size) * int(nmemb)) + for i, content in enumerate(data): + addr = dse.symb.expr_simp(ptr + ExprInt(i, ptr.size)) + update[ExprMem(addr, 8)] = content + + ret_addr = ExprInt(dse.jitter.get_stack_arg(0), regs.RIP.size) + ret_value = FILE_size + + update.update({ + regs.RSP: dse.symb.eval_expr(regs.RSP + ExprInt(8, regs.RSP.size)), + dse.ir_arch.IRDst: ret_addr, + regs.RIP: ret_addr, + regs.RAX: ret_value, + }) + dse.update_state(update) + +def xxx_fclose_symb(dse): + regs = dse.ir_arch.arch.regs + stream = dse.eval_expr(regs.RDI) + FILE_to_info_symb[stream].close() + + ret_addr = ExprInt(dse.jitter.get_stack_arg(0), regs.RIP.size) + dse.update_state({ + regs.RSP: dse.symb.eval_expr(regs.RSP + ExprInt(8, regs.RSP.size)), + dse.ir_arch.IRDst: ret_addr, + regs.RIP: ret_addr, + regs.RAX: ExprInt(0, regs.RAX.size), + }) + +# Symbolic naive version of _libc_start_main + +def xxx___libc_start_main_symb(dse): + # ['RDI', 'RSI', 'RDX', 'RCX', 'R8', 'R9'] + # main, argc, argv, ... + regs = dse.ir_arch.arch.regs + top_stack = dse.eval_expr(regs.RSP) + main_addr = dse.eval_expr(regs.RDI) + argc = dse.eval_expr(regs.RSI) + argv = dse.eval_expr(regs.RDX) + hlt_addr = ExprInt(0x1337beef, 64) + + dse.update_state({ + ExprMem(top_stack, 64): hlt_addr, + regs.RDI: argc, + regs.RSI: argv, + dse.ir_arch.IRDst: main_addr, + dse.ir_arch.pc: main_addr, + }) + +# Stop the execution on puts and get back the corresponding string +class FinnishOn(Exception): + + def __init__(self, string): + self.string = string + super(FinnishOn, self).__init__() + +def xxx_puts_symb(dse): + string = dse.jitter.get_str_ansi(dse.jitter.cpu.RDI) + raise FinnishOn(string) + + +done = set([]) # Set of jump address already handled +todo = set([""]) # Set of file content to test + +class DSEGenFile(DSEPathConstraint): + """DSE with a specific solution creation: + The solution is the content of the FILE to be read + + The politics of exploration is the branch coverage: create a solution only + if the target address has never been seen + """ + + def handle_solution(self, model, destination): + global todo, done + assert destination.is_int() + + if destination in done: + # Skip this path, already treated + return + + finfo = FILE_to_info_symb[FILE_stream] + + # Build corresponding file + out = "" + fsize = max(model.eval(self.z3_trans.from_expr(FILE_size)).as_long(), + len(finfo.gen_bytes)) + for index in xrange(fsize): + try: + byteid = finfo.gen_bytes[index] + out += chr(model.eval(self.z3_trans.from_expr(byteid)).as_long()) + except (KeyError, AttributeError) as _: + # Default value if there is no constraint on current byte + out += "\x00" + + todo.add(out) + done.add(destination) + +# Instanciate the DSE engine +machine = Machine("x86_64") +dse = DSEGenFile(machine) + +# Attach to the jitter +dse.attach(sb.jitter) + +# Update the jitter state: df is read, but never set +# Approachs: specific or generic +# - Specific: +# df_value = ExprInt(sb.jitter.cpu.df, dse.ir_arch.arch.regs.df.size) +# dse.update_state({ +# dse.ir_arch.arch.regs.df: df_value +# }) +# - Generic: +dse.update_state_from_concrete() + +# Add constraint on file size, we don't want to generate too big FILE +z3_file_size = dse.z3_trans.from_expr(FILE_size) +dse.cur_solver.add(0 < z3_file_size) +dse.cur_solver.add(z3_file_size < 0x10) + +# Register symbolic stubs for extern functions (xxx_puts_symb, ...) +dse.add_lib_handler(sb.libs, globals()) + +# Automatic exploration of solution + +## Save the current clean state, before any computation of the FILE content +snapshot = dse.take_snapshot() +found = False + +while todo: + # Prepare a solution to try, based on the clean state + file_content = todo.pop() + print "CUR: %r" % file_content + open("test.txt", "w").write(file_content) + dse.restore_snapshot(snapshot) + FILE_to_info.clear() + FILE_to_info_symb.clear() + + # Play the current file + try: + sb.run() + except FinnishOn as finnish_info: + print finnish_info.string + if finnish_info.string == "OK": + # Stop if the expected result is found + found = True + break + +# Assert that the result has been found +assert found == True +print "FOUND !" + +# Replay for real +print "Trying to launch the binary without Miasm" +crackme = subprocess.Popen([options.filename], stdout=subprocess.PIPE, + stderr=subprocess.PIPE) +stdout, stderr = crackme.communicate() +assert not stderr +stdout = stdout.strip() +print stdout +assert stdout == "OK" |