trace_PE_verify.py

import reven

def read_symbolic(point, symbolic):
	if isinstance(symbolic, reven.SymbolicRegister):
		return point.cpu().read_register(symbolic.name)
	elif isinstance(symbolic, reven.SymbolicPhysicalMemory):
		mem = point.memory().read_physical(symbolic.address, symbolic.size)
		value = 0
		for byte in reversed(mem):
			value <<= 8
			value |= ord(byte)
		return value


def propagate_taint_once(pt, current_taint):
	taint_result = project.taint(pt, current_taint, forward=True, count=1)

	for point, diff in sorted(taint_result.diffs.iteritems()):
		print point
		print "\t taint in:  ", [s.name for s in diff.tainted]
		print "\t taint out: ", [s.name for s in diff.untainted],
		print
		current_taint += diff.tainted
		current_taint = [sym for sym in current_taint if sym not in diff.untainted]
		for sym in diff.untainted:
			current_taint = [s for s in current_taint if s.name != sym.name]
		for sym in current_taint:
			print "%s=0x%x" % (sym.name, read_symbolic(point, sym))
		print

		return current_taint



project = reven.Project('192.168.4.2', 13392)

print "\nTrace Windows PE Verification\n"
trace = project.traces()[0]
seq_count = trace.sequence_count
sym_name = "_MiVerifyImageHeader@16"
crit = reven.SymbolCriterion(sym_name, accuracy="exact")
for p in trace.search_point([crit]):
	point = p
	break

print "Beginning taint trace on PE verification at %s\n" % point.symbol.name
cpu = point.cpu()
mem = point.memory()
esp = cpu.read_register("esp")
pe_buff = mem.read_u32(esp + 4)
print "Found PE buffer at: 0x%x" % pe_buff
pe_phys_buff = mem.get_physical_address(pe_buff)
print "Physical buffer at: 0x%08x\n\n" % pe_phys_buff
taint_area = [reven.SymbolicPhysicalMemory(pe_phys_buff, 128)]
current_taint = taint_area

iterations = 10
print "Propagating taint for %d iterations .. here we go!\n\n" % iterations 
for i in range(0, iterations):
	current_taint = propagate_taint_once(point, current_taint)
	point = point.next()