Secure your code as it's written. Use Snyk Code to scan source code in minutes - no build needed - and fix issues immediately.
def solv_concrete_engine_linux_x86(p, entry_state):
new_concrete_state = execute_concretly(p, entry_state, BINARY_DECISION_ADDRESS, [], [])
arg0 = claripy.BVS('arg0', 8*32)
symbolic_buffer_address = new_concrete_state.regs.ebp-0xa0
new_concrete_state.memory.store(symbolic_buffer_address, arg0)
# symbolic exploration
simgr = p.factory.simgr(new_concrete_state)
exploration = simgr.explore(find=DROP_STAGE2_V1, avoid=[DROP_STAGE2_V2, VENV_DETECTED, FAKE_CC])
if not exploration.stashes['found'] and exploration.errored and type(exploration.errored[0].error) is angr.errors.SimIRSBNoDecodeError:
raise nose.SkipTest()
new_symbolic_state = exploration.stashes['found'][0]
binary_configuration = new_symbolic_state.solver.eval(arg0, cast_to=int)
execute_concretly(p, new_symbolic_state, BINARY_EXECUTION_END, [(symbolic_buffer_address, arg0)], [])
correct_solution = 0xa000000f9ffffff000000000000000000000000000000000000000000000000
nose.tools.assert_true(binary_configuration == correct_solution)
def test_ppc32():
arger_ppc32 = angr.Project(os.path.join(test_location, 'ppc', 'argc_symbol'))
r_addr = [0x1000043C, 0x10000474, 0x100004B0]
sargc = claripy.BVS('argc', 32)
s = arger_ppc32.factory.entry_state(args = [claripy.BVS('arg_0', 40*8), claripy.BVS('arg_1', 40*8), claripy.BVS('arg_2', 40*8)], env ={"HOME": "/home/angr"}, argc=sargc)
pg = arger_ppc32.factory.simulation_manager(s).explore(find=r_addr, num_find=100)
_verify_results(pg, sargc)
def solv_concrete_engine_linux_arm(p, entry_state):
new_concrete_state = execute_concretly(p, entry_state, BINARY_DECISION_ADDRESS, [])
arg0 = claripy.BVS('arg0', 5 * 32)
symbolic_buffer_address = new_concrete_state.regs.r3
new_concrete_state.memory.store(symbolic_buffer_address, arg0)
simgr = p.factory.simgr(new_concrete_state)
print("Symbolically executing BINARY to find dropping of second stage [ address: " + hex(DROP_STAGE2_V1) + " ]")
exploration = simgr.explore(find=DROP_STAGE2_V2, avoid=[DROP_STAGE2_V1, VENV_DETECTED, FAKE_CC])
if not exploration.stashes['found'] and exploration.errored and type(exploration.errored[0].error) is angr.errors.SimIRSBNoDecodeError:
raise nose.SkipTest()
new_symbolic_state = exploration.stashes['found'][0]
binary_configuration = new_symbolic_state.solver.eval(arg0, cast_to=int)
print("Executing BINARY concretely with solution found until the end " + hex(BINARY_EXECUTION_END))
execute_concretly(p, new_symbolic_state, BINARY_EXECUTION_END, [(symbolic_buffer_address, arg0)])
any(v in chall_resp_info.vars_we_added for v in c.variables):
controllable_constraints.append(c)
elif any(v.startswith("output_var") for v in c.variables):
# an output like a leak
pass
else:
# uncontrollable constraints will show up as zen constraints etc
uncontrollable_constraints.append(c)
if len(controllable_constraints) > 0:
l.debug("Challenge response detected!")
file_1 = state.posix.stdout
stdout = file_1.load(0, file_1.size)
stdout_len = state.solver.eval(file_1.size)
stdout_bvs = [claripy.BVS("file_stdout_%#x" % i, 8, explicit_name=True) for i in range(stdout_len)]
stdout_bv = claripy.Concat(*stdout_bvs)
state.add_constraints(stdout == stdout_bv)
# we call simplify to separate the contraints/dependencies
state.solver.simplify()
merged_solver = state.solver._solver._merged_solver_for(lst=[self._mem] + controllable_constraints)
# todo here we can verify that there are actually stdout bytes here, otherwise we have little hope
# add the important stdout vars to mem
needed_vars = []
for bv in stdout_bvs:
if len(bv.variables & merged_solver.variables) != 0:
needed_vars.append(bv)
# add the str_to_int vars and int_to_str vars
def main():
proj = angr.Project('./unbreakable-enterprise-product-activation', load_options={"auto_load_libs": False}) # Disabling the automatic library loading saves a few milliseconds.
input_size = 0x43; # Max length from strncpy, see 0x4005ae.
argv1 = claripy.BVS("argv1", input_size * 8)
initial_state = proj.factory.entry_state(args=["./unbreakable-enterprise-product-activation", argv1], add_options={angr.options.LAZY_SOLVES})
initial_state.libc.buf_symbolic_bytes=input_size + 1 # Thanks to Christopher Salls (@salls) for pointing this out. By default there's only 60 symbolic bytes, which is too small.
# For some reason if you constrain too few bytes, the solution isn't found. To be safe, I'm constraining them all.
for byte in argv1.chop(8):
initial_state.add_constraints(byte != '\x00') # null
initial_state.add_constraints(byte >= ' ') # '\x20'
initial_state.add_constraints(byte <= '~') # '\x7e'
# Source: https://www.juniper.net/documentation/en_US/idp5.1/topics/reference/general/intrusion-detection-prevention-custom-attack-object-extended-ascii.html
# Thanks to Tom Ravenscroft (@tomravenscroft) for showing me how to restrict to printable characters.
# We're told that every flag is formatted as "CTF{...}", so we might as well use that information to save processing time.
initial_state.add_constraints(argv1.chop(8)[0] == 'C')
initial_state.add_constraints(argv1.chop(8)[1] == 'T')
initial_state.add_constraints(argv1.chop(8)[2] == 'F')
def run(self, thing, *args):
# mMark object as symbolic
if isinstance(thing, SimSootValue_ThisRef):
this_ref = thing
if args:
method_descriptor = args[-1]
else:
# if args is empty, method is static and has no params
method_descriptor = thing
# return the appropriate value based on the return type of the method
if method_descriptor is None or method_descriptor.ret is None or method_descriptor.ret == 'void':
return
elif method_descriptor.ret in ['byte', 'char', 'short', 'int', 'boolean']:
return claripy.BVS('unc_{}_{}'.format(method_descriptor.ret, method_descriptor.name), 32)
elif method_descriptor.ret == 'long':
return claripy.BVS('unc_long_{}'.format(method_descriptor.name), 64)
elif method_descriptor.ret == 'float':
return claripy.FPS('unc_float_{}'.format(method_descriptor.name), claripy.FSORT_FLOAT)
elif method_descriptor.ret == 'double':
return claripy.FPS('unc_double_{}'.format(method_descriptor.name), claripy.FSORT_DOUBLE)
elif method_descriptor.ret == 'java.lang.String':
str_ref = SimSootValue_StringRef.new_string(
self.state, claripy.StringS("unc_string_{}".format(method_descriptor.name), 1000))
return str_ref
elif method_descriptor.ret.endswith('[][]'):
raise NotImplementedError
elif method_descriptor.ret.endswith('[]'):
# TODO here array size should be symbolic
return SimSootExpr_NewArray.new_array(self.state, method_descriptor.ret[:-2], claripy.BVV(2, 32))
else:
def generate_input(p, to_find, to_avoid, byte_addresses):
print('[*] Generating input ....')
byte_map = {}
for i in range(0,len(to_find)-1):
f = to_find[i]
t = to_find[i+1]
#Set up the state for the function we want to solve
e = p.factory.blank_state(addr=f)
rdi = claripy.BVV(0, 56).concat(claripy.BVS('rdi', 8))
rsi = claripy.BVV(0, 56).concat(claripy.BVS('rsi', 8))
rdx = claripy.BVV(0, 56).concat(claripy.BVS('rdx', 8))
rcx = claripy.BVV(0, 56).concat(claripy.BVS('rcx', 8))
e.regs.rdi = rdi
e.regs.rsi = rsi
e.regs.rdx = rdx
e.regs.rcx = rcx
#Generate a SimulationManager out of this state and explore
sm = p.factory.simulation_manager(e)
sm.explore(find=t,avoid=to_avoid)
#Save the solutions
found = sm.found[0]
address_local = byte_addresses[i]
byte_map[address_local[3]] = found.solver.eval(rdi)
byte_map[address_local[2]] = found.solver.eval(rsi)
byte_map[address_local[1]] = found.solver.eval(rdx)
def main():
p = angr.Project('./issue', load_options={"auto_load_libs": False})
# By default, all symbolic write indices are concretized.
state = p.factory.entry_state(add_options={angr.options.SYMBOLIC_WRITE_ADDRESSES})
u = claripy.BVS("u", 8)
state.memory.store(0x804a021, u)
sm = p.factory.simulation_manager(state)
def correct(state):
try:
return b'win' in state.posix.dumps(1)
except:
return False
def wrong(state):
try:
return b'lose' in state.posix.dumps(1)
except:
return False
sm.explore(find=correct, avoid=wrong)
# try doubling the search len and searching again
s_new = s
while all(con.is_false() for con in c):
s_new += search_len
search_len *= 2
r, c, i = self.state.memory.find(s_new, null_seq, search_len, max_symbolic_bytes=max_symbolic_bytes, step=step, chunk_size=chunk_size)
# stop searching after some reasonable limit
if search_len > 0x10000:
raise angr.SimMemoryLimitError("strlen hit limit of 0x10000")
self.max_null_index = max(i)
self.state.add_constraints(*c)
result = r - s
if result.depth > 3:
rresult = claripy.BVS('strlen', len(result))
self.state.solver.add(result == rresult)
result = rresult
return result
state = SimState(self.project, **kwargs)
stack_end = state.arch.initial_sp
if o.ABSTRACT_MEMORY not in state.options:
state.memory.mem._preapproved_stack = IRange(stack_end - stack_size, stack_end)
if o.INITIALIZE_ZERO_REGISTERS in state.options:
highest_reg_offset, reg_size = max(state.arch.registers.values())
for i in range(0, highest_reg_offset + reg_size, state.arch.bytes):
state.registers.store(i, state.se.BVV(0, state.arch.bits))
if state.arch.sp_offset is not None:
state.regs.sp = stack_end
if initial_prefix is not None:
for reg in state.arch.default_symbolic_registers:
state.registers.store(reg, claripy.BVS(initial_prefix + "_" + reg,
state.arch.bits,
explicit_name=True))
for reg, val, is_addr, mem_region in state.arch.default_register_values:
region_base = None # so pycharm does not complain
if is_addr:
if isinstance(mem_region, tuple):
# unpack it
mem_region, region_base = mem_region
elif mem_region == 'global':
# Backward compatibility
region_base = 0
else:
raise AngrSimOSError('You must specify the base address for memory region "%s". ' % mem_region)