import angr, claripy
target = angr.Project('a.out', auto_load_libs=False)
input_len = 15 # Discovered with manual analysis at a glance
inp = [claripy.BVS('flag_%d' %i, 8) for i in range(input_len)]
# Define an array of 8 bit vectors ffor each char of the flag
flag = claripy.Concat(*inp + [claripy.BVV(b'\n')])
st = target.factory.full_init_state(args=["./a.out"], stdin=flag)
# Create a simulation with our flag symbols as stdin
for k in inp:
st.solver.add(k < 0x7f)
st.solver.add(k > 0x20)
# Add constraints that the characters should be printable
sm = target.factory.simulation_manager(st)
sm.run()
y = []
for x in sm.deadended:
# Out of the simulations that exit, record
# any that output SUCCESS
if b"SUCCESS" in x.posix.dumps(1):
y.append(x)
#grab the first ouptut
valid = y[0].posix.dumps(0)
print(valid)import angr
import claripy #the solver engine
proj = angr.Project("./welcome", auto_load_libs=False)
sym_arg_size = 0x10 #Length in Bytes because we will multiply with 8 later
inp = [claripy.BVS('flag_%d' % i, 8 ) for i in range(sym_arg_size)]
flag = claripy.Concat(*inp + [claripy.BVV(b'\n')])
state = proj.factory.full_init_state(args=["./welcome"], stdin=flag)
for byte in inp:
state.solver.add(byte >= ord('0'))
state.solver.add(byte <= ord('9'))
# Input is specified to be a number
simgr = proj.factory.simulation_manager(state)
good = 0x400000 + 0x12b2
# Address of flag file being opened
bad = [0x400000 + 0x1669, 0x400000 + 0x167b]
# Addresses of failure messages being printed
simgr.use_technique(angr.exploration_techniques.DFS())
simgr.explore(find=good, avoid=bad)
# Explore input that will end at the good while avoiding the bad
found = simgr.found[0]
print(found.solver.eval(flag, cast_to=bytes))
# Cast our found input to bytes and printgoing brrrrrr