dse_strategies Namespace Reference

Functions
def	code_sentinelle (jitter)

Variables
	parser = ArgumentParser("DSE Example")
	help
	choices
	args = parser.parse_args()
dictionary	strategy
	loc_db = LocationDB()
int	run_addr = 0x40000
	machine = Machine("x86_32")
	jitter = machine.jitter(loc_db, "python")
int	ret_addr = 0x1337beef
	dse = DSEPathConstraint(machine, loc_db, produce_solution=strategy)
	regs = jitter.ir_arch.arch.regs
	arg = ExprId("ARG", 32)
	arg_addr = ExprMem(ExprInt(jitter.cpu.ESP + 4, regs.ESP.size), arg.size)
	todo = set([ExprInt(0, arg.size)])
	done = set()
	snapshot = dse.take_snapshot()
	reaches = set()
	arg_value = todo.pop()
	keep_known_solutions
	sol_value = model.eval(dse.z3_trans.from_expr(arg)).as_long()
	sol_expr = ExprInt(sol_value, arg.size)

Detailed Description

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

Function Documentation

code_sentinelle()

def dse_strategies.code_sentinelle

(

jitter

)

Variable Documentation

arg

dse_strategies.arg = ExprId("ARG", 32)

arg_addr

dse_strategies.arg_addr = ExprMem(ExprInt(jitter.cpu.ESP + 4, regs.ESP.size), arg.size)

arg_value

dse_strategies.arg_value = todo.pop()

args

dse_strategies.args = parser.parse_args()

choices

dse_strategies.choices

done

dse_strategies.done = set()

dse

dse_strategies.dse = DSEPathConstraint(machine, loc_db, produce_solution=strategy)

help

dse_strategies.help

jitter

dse_strategies.jitter = machine.jitter(loc_db, "python")

keep_known_solutions

dse_strategies.keep_known_solutions

loc_db

dse_strategies.loc_db = LocationDB()

machine

dse_strategies.machine = Machine("x86_32")

parser

dse_strategies.parser = ArgumentParser("DSE Example")

reaches

dse_strategies.reaches = set()

regs

dse_strategies.regs = jitter.ir_arch.arch.regs

ret_addr

int dse_strategies.ret_addr = 0x1337beef

run_addr

int dse_strategies.run_addr = 0x40000

snapshot

dse_strategies.snapshot = dse.take_snapshot()

sol_expr

dse_strategies.sol_expr = ExprInt(sol_value, arg.size)

sol_value

dse_strategies.sol_value = model.eval(dse.z3_trans.from_expr(arg)).as_long()

strategy

dictionary dse_strategies.strategy

Initial value:

=  {
    "code-cov": DSEPathConstraint.PRODUCE_SOLUTION_CODE_COV,
    "branch-cov": DSEPathConstraint.PRODUCE_SOLUTION_BRANCH_COV,
    "path-cov": DSEPathConstraint.PRODUCE_SOLUTION_PATH_COV,
}[args.strategy]

todo

dse_strategies.todo = set([ExprInt(0, arg.size)])