For this challenge I decided to try out binary ninja, which I haven’t used since the original beta back in 2016. Back then I was very impressed with the python API and used it to easily solve a challenge that required automatically reversing and exploiting 1000 binaries of a specific template. This time I’m using binaryninja cloud, which unfortunately does not have API access, but does have a very nice high level IL I’ve been wanting to play around with. Spoilers: not much reversing was had.

The challenge

Opening the binary in binary ninja and switching to high-level IL, we see that the program takes a 32 byte input

Start of the main function

and then calls a bunch of functions. A large bunch of functions:

large bunch of functions

After calling all of the functions, the code prints that we have succeeded

success

Let’s have a look at one of the functions.

example func

There’s an annoying amount of sign extensions here, but the function performs a check on an simple equation of some of the input characters. If the result is wrong, we call this bad function:

bad func

All of the other functions perform similar checks and jump to the same function when failing.

At this point we could try to solve the equations, or input them into z3 and let it do the heavy lifting. Or we could just let angr figure out everything by itself. Let’s go!

Angr

Solving with angr is really easy. We just let it know the size of our input, give it a hint as to the values of the flag (all printable), and let it run!

import angr
import claripy

proj = angr.Project("measles", load_options={"auto_load_libs": False},
                    main_opts={"base_addr": 0})

flag = [claripy.BVS(f"c_{i}", 8) for i in range(32)]
flag_ast = claripy.Concat(*flag)

state = proj.factory.entry_state(stdin=flag_ast)

for f in flag:
    state.solver.add(f >= 0x20)
    state.solver.add(f < 0x7f)

simgr = proj.factory.simulation_manager(state)
print("Start")
simgr.explore(avoid=0x1179)

found = simgr.deadended[0]
valid_flag = found.solver.eval(flag_ast, cast_to=bytes)
print(valid_flag)

After a few minutes it spits out the correct solution:

evlz{n0_al1ce_1t_h4s_m3a5l3s}ctf