08 Angr Constraints

Analyzing the Binary

Looking at main we can see that it is looking for a 16 character password.

It runs each character through a complex function that checks if the value is between 0x40 and 0x5a before running some compilations.

Then it runs the results through a check equals function that looks like it returns a boolean.

Based on the check equals we get a success or fail message.

The check equals function will create a lot of branches. With that in mind the goal will be to stop processing before hitting that function, but then put constraints on the solution so that it equals the string.

Using gdb I printed out the text used in the check equals function.

Our tasks for this script are:

1. Figure out the starting address
2. Figure out where we will store the bitvector
3. Stop before we process the string compare
4. Add constraints to the solver so that the string compare will return true

Building the Script

I chose to start the script the same place as usual, right after the call to scanf.

path_to_binary = "./08_angr_constraints"
project = angr.Project(path_to_binary)

start_address = 0x8048625
initial_state = project.factory.entry_state(
    addr=start_address,
    add_options={
        angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
        angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS,
    },
)

Now we store the bitvector in memory

password = claripy.BVS("password", 16 * 8)
password_address = 0x804A050
initial_state.memory.store(password_address, password)

We create the simulation manager and tell it the address to find. This time though we stop before the print "Good Job." statement. I chose the first sub preparing the stack for the call to the check equals function. We then tell the simulation manager to explore.

simulation = project.factory.simgr(initial_state)
address_to_check_constraint = 0x8048669
simulation.explore(find=address_to_check_constraint)

Now we move onto the solution section. We start out as normal.

if simulation.found:
    solution_state = simulation.found[0]

We want to constrain the parameter sent to the to_check function. The goal is to constrain it to the exact string it is being compared against. We can do that by setting a constraint on that specific portion of memory.

constrained_parameter_address = 0x804A050
constrained_parameter_size_bytes = 16
constrained_parameter_bitvector = solution_state.memory.load(
    constrained_parameter_address, constrained_parameter_size_bytes
)
constrained_parameter_desired_value = "AUPDNNPROEZRJWKB".encode()
solution_state.add_constraints(
    constrained_parameter_bitvector == constrained_parameter_desired_value
)

That is it. Once we have told angr to only solve give us solutions that meet our constraints we can print the solution.

solution = solution_state.solver.eval(password, cast_to=bytes)
print(solution)

Final Script

import angr
import claripy
import pwn


def main():
    path_to_binary = "./08_angr_constraints"
    project = angr.Project(path_to_binary)

    start_address = 0x8048625
    initial_state = project.factory.entry_state(
        addr=start_address,
        add_options={
            angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
            angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS,
        },
    )

    password = claripy.BVS("password", 16 * 8)

    password_address = 0x804A050
    initial_state.memory.store(password_address, password)

    simulation = project.factory.simgr(initial_state)

    address_to_check_constraint = 0x8048669
    simulation.explore(find=address_to_check_constraint)

    if simulation.found:
        solution_state = simulation.found[0]

        constrained_parameter_address = 0x804A050
        constrained_parameter_size_bytes = 16
        constrained_parameter_bitvector = solution_state.memory.load(
            constrained_parameter_address, constrained_parameter_size_bytes
        )

        constrained_parameter_desired_value = "AUPDNNPROEZRJWKB".encode()

        solution_state.add_constraints(
            constrained_parameter_bitvector == constrained_parameter_desired_value
        )

        solution = solution_state.solver.eval(password, cast_to=bytes)
        run_binary(solution, path_to_binary)
    else:
        raise Exception("Could not find the solution")


def run_binary(solution, path_to_binary):
    if type(solution) == str:
        solution = bytes(solution, "utf-8")
    print(f"[+] Solution found: {solution.decode()}")
    print("    [|] Running binary")
    elf = pwn.ELF(path_to_binary, checksec=False)
    pty = pwn.process.PTY
    io = elf.process(stdin=pty, stdout=pty, level="warn")
    io.recvuntil(b":")
    io.sendline(solution)
    output = io.recvline().decode().splitlines()[0].strip()
    print(f"    [+] Output: {output}")


if __name__ == "__main__":
    main()