0

recently I have been trying to solve the nobranch7e4 challenge from the HXP CTF 2020 using angr.

My success has been mixed: Even though there is no apparent state explosion I still cannot solve for the flag because for some reason I get an error: Got an unsat result

This is the script I am using (the binary is available at the link mentioned above):

import angr
import claripy
import logging

logging.getLogger("angr.sim_manager").setLevel("DEBUG")
p = angr.Project("nobranch7e4", auto_load_libs=False)

flag_size = 64
flag_addr = p.loader.find_symbol("flag").rebased_addr

s = p.factory.entry_state(add_options=angr.options.unicorn)

flag = [ claripy.BVS("flag_%d" % i, 8) for i in range(flag_size) ]
for c in flag:
    s.solver.add(c < 0x7f)
    s.solver.add(c > 0x20)

flag = claripy.Concat(*flag)
s.memory.store(flag_addr, flag)

sm = p.factory.simulation_manager(s)
sm.run()

final_state = sm.deadended[0]
final_state.solver.add(final_state.regs.dil == 0)
result = final_state.solver.eval(flag, cast_to=bytes)
print("The flag is", result)

(The goal is to make the program exit with code 0 by patching the memory at flag)

I observed that I am able to solve if I give at least the first 53 characters as known input. For some reasons the same procedure does not work if I assume the last n characters are known (it seems I cannot even solve for only the first character unknown).

I also tried hinting the flag format hxp{...} but that does not work either.

Adding/Removing the constraints (0x20 < c < 0x7f) does not seem to have an effect, too.

Any ideas?

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.