Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
130 lines (103 sloc) 3.92 KB
"""Example of DynamicSymbolicExecution engine use
This example highlights how coverage can be obtained on a binary
Expected target: 'simple_test.bin'
Global overview:
- Prepare a 'jitter' instance with the targeted function
- Attach a DSE instance
- Make the function argument symbolic, to track constraints on it
- Take a snapshot
- Initialize the argument candidate list with an arbitrary value, 0
- Main loop:
- Restore the snapshot (initial state, before running the function)
- Take an argument candidate and set it in the jitter
- Run the function
- Ask the DSE for new candidates, according to its strategy, ie. finding new
block / branch / path
from argparse import ArgumentParser
from miasm2.analysis.machine import Machine
from miasm2.jitter.csts import PAGE_READ, PAGE_WRITE
from miasm2.analysis.dse import DSEPathConstraint
from miasm2.expression.expression import ExprMem, ExprId, ExprInt, ExprAssign
# Argument handling
parser = ArgumentParser("DSE Example")
parser.add_argument("filename", help="Target x86 shellcode")
parser.add_argument("strategy", choices=["code-cov", "branch-cov", "path-cov"],
help="Strategy to use for solution creation")
args = parser.parse_args()
# 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,
# Map the shellcode
run_addr = 0x40000
machine = Machine("x86_32")
jitter = machine.jitter("python")
with open(args.filename) as fdesc:
jitter.vm.add_memory_page(run_addr, PAGE_READ | PAGE_WRITE,,
# Expect a binary with one argument on the stack
# Argument
# Handle return
def code_sentinelle(jitter): = False
return False
ret_addr = 0x1337beef
jitter.add_breakpoint(ret_addr, code_sentinelle)
# Init the jitter
# Init a DSE instance with a given strategy
dse = DSEPathConstraint(machine, produce_solution=strategy)
# Concretize everything except the argument
regs = jitter.ir_arch.arch.regs
arg = ExprId("ARG", 32)
arg_addr = ExprMem(ExprInt(jitter.cpu.ESP + 4, regs.ESP.size), arg.size)
# @[ESP + 4] = ARG
arg_addr: arg
# Explore solutions
todo = set([ExprInt(0, arg.size)])
done = set()
snapshot = dse.take_snapshot()
# Only needed for the final output
reachs = set()
while todo:
# Get the next candidate
arg_value = todo.pop()
# Avoid using twice the same input
if arg_value in done:
print "Run with ARG = %s" % arg_value
# Restore state, while keeping already found solutions
dse.restore_snapshot(snapshot, keep_known_solutions=True)
# Reinit jitter (reset, etc.)
# Set the argument value in the jitter context
jitter.eval_expr(ExprAssign(arg_addr, arg_value))
# Launch
# Obtained solutions are in dse.new_solutions: identifier -> solution model
# The identifier depends on the strategy:
# - block address for code coverage
# - last edge for branch coverage
# - execution path for path coverage
for sol_ident, model in dse.new_solutions.iteritems():
print "Found a solution to reach: %s" % str(sol_ident)
# Get the argument to use as a Miasm Expr
sol_value = model.eval(dse.z3_trans.from_expr(arg)).as_long()
sol_expr = ExprInt(sol_value, arg.size)
# Display info and update storages
print "\tARG = %s" % sol_expr
print "Found %d input, to reach %d element of coverage" % (len(done),