diff options
Diffstat (limited to 'example/symbol_exec/dse_crackme.py')
| -rw-r--r-- | example/symbol_exec/dse_crackme.py | 73 |
1 files changed, 36 insertions, 37 deletions
diff --git a/example/symbol_exec/dse_crackme.py b/example/symbol_exec/dse_crackme.py index 34c39138..9ac4d6d1 100644 --- a/example/symbol_exec/dse_crackme.py +++ b/example/symbol_exec/dse_crackme.py @@ -10,6 +10,7 @@ import os import subprocess from collections import namedtuple from pdb import pm +from tempfile import NamedTemporaryFile from miasm2.jitter.csts import PAGE_READ, PAGE_WRITE from miasm2.analysis.sandbox import Sandbox_Linux_x86_64 @@ -19,6 +20,8 @@ from miasm2.expression.expression import * my_FILE_ptr = 0x11223344 FInfo = namedtuple("FInfo", ["path", "fdesc"]) FILE_to_info = {} +TEMP_FILE = NamedTemporaryFile() + def xxx_fopen(jitter): ''' #include <stdio.h> @@ -57,8 +60,13 @@ def xxx_fclose(jitter): # Create sandbox parser = Sandbox_Linux_x86_64.parser(description="ELF sandboxer") parser.add_argument("filename", help="ELF Filename") +parser.add_argument("--strategy", + choices=["code-cov", "branch-cov", "path-cov"], + help="Strategy to use for solution creation", + default="code-cov") options = parser.parse_args() options.mimic_env = True +options.command_line = ["%s" % TEMP_FILE.name] sb = Sandbox_Linux_x86_64(options.filename, options, globals()) # Init segment @@ -209,44 +217,17 @@ def xxx_puts_symb(dse): raise FinishOn(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 - - 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) +# Convert strategy to the correct value +strategy = { + "code-cov": DSEPathConstraint.PRODUCE_SOLUTION_CODE_COV, + "branch-cov": DSEPathConstraint.PRODUCE_SOLUTION_BRANCH_COV, + "path-cov": DSEPathConstraint.PRODUCE_SOLUTION_PATH_COV, +}[options.strategy] +dse = DSEPathConstraint(machine, produce_solution=strategy) # Attach to the jitter dse.attach(sb.jitter) @@ -279,8 +260,8 @@ 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) + open(TEMP_FILE.name, "w").write(file_content) + dse.restore_snapshot(snapshot, keep_known_solutions=True) FILE_to_info.clear() FILE_to_info_symb.clear() @@ -294,13 +275,31 @@ while todo: found = True break + finfo = FILE_to_info_symb[FILE_stream] + for sol_ident, model in dse.new_solutions.iteritems(): + # Build the file corresponding to solution in 'model' + + out = "" + fsize = max(model.eval(dse.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(dse.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) + # 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, +crackme = subprocess.Popen([options.filename, TEMP_FILE.name], + stdout=subprocess.PIPE, stderr=subprocess.PIPE) stdout, stderr = crackme.communicate() assert not stderr |