04 Angr Symbolic Stack

Analyzing the Binary

So the challenge is that the call to scanf expects two inputs, but unlike the last one, we can't just bypass the function all together because the logic in handle_user contains both the scanf call and the calls to complex functions.

Therefore, we need to jump in at the middle of the handle_user function. To do that, we need to figure out two things:

1. What our insertion point should be.
2. What the stack should look like at our insertion point.

Lets look at the handle_user function in assembly.

From this we can tell that the input will be two unsigned ints (four bytes each).

Insertion point

We know we want to start after the scanf call but before the call to complex_function0. That gives us four options. The add esp, 0x10 is cleaning up the stack after the scanf call. So, I think the best place would be 0x8048697.

Rebuilding the Stack

We know we want the password0 to start at 0xc (remember the stack grows up, when adding to the stack, the first byte will go on top, the second on top of the first, and so on).

We want password1 to be right below password0 on the stack starting at 0x10 (and taking up four bytes).

We need to pad the stack to align the start password1 to 0xc and then insert both passwords. Since the password is four bytes (determined above) we take its starting point and minus four and that gives us the padding (in bytes) we need to add to the ESP.

With that done, we can move onto the script.

Building the Script

We are going to start off like we did in 03 but using the address we found above as our starting point.

path_to_binary = "./04_angr_symbolic_stack"
project = angr.Project(path_to_binary)
start_address = 0x08048697
initial_state = project.factory.blank_state(addr=start_address)

Lets define our two bitvectors.

password0 = claripy.BVS("password0", 32)
password1 = claripy.BVS("password1", 32)

Now we need to configure the stack. We will start by setting the stack pointer to ebp and then add in the padding we determined, then the two passwords - being conscious of the order so that the stack is set up correctly.

initial_state.regs.ebp = initial_state.regs.esp
padding_length_in_bytes = 8
initial_state.regs.esp -= padding_length_in_bytes
initial_state.stack_push(password0)
initial_state.stack_push(password1

With that done we can create the simulation manager and let it do its thing.

simulation = project.factory.simgr(initial_state)
simulation.explore(find=is_successful, avoid=should_abort)

Final Script

import sys

import angr
import claripy
import pwn


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}")


def main():
    path_to_binary = "./04_angr_symbolic_stack"
    project = angr.Project(path_to_binary)

    start_address = 0x08048697
    initial_state = project.factory.blank_state(addr=start_address)

    password0 = claripy.BVS("password0", 32)
    password1 = claripy.BVS("password1", 32)

    initial_state.regs.ebp = initial_state.regs.esp
    padding_length_in_bytes = 8
    initial_state.regs.esp -= padding_length_in_bytes
    initial_state.stack_push(password0)
    initial_state.stack_push(password1)

    simulation = project.factory.simgr(initial_state)

    def is_successful(state):
        stdout_output = state.posix.dumps(sys.stdout.fileno())
        return b"Good Job." in stdout_output

    def should_abort(state):
        stdout_output = state.posix.dumps(sys.stdout.fileno())
        return b"Try again." in stdout_output

    simulation.explore(find=is_successful, avoid=should_abort)

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

        solution0 = solution_state.solver.eval(password0)
        solution1 = solution_state.solver.eval(password1)

        solution = " ".join(map(str, [solution0, solution1]))
        run_binary(solution, path_to_binary)
    else:
        raise Exception("Could not find the solution")


if __name__ == "__main__":
    main()