12 Angr Veritesting

This is an interesting problem. While looking at the code, we can see we have a similar branch explosion that we saw in 09.

This will cause the program to branch 2^32 times. Luckily angr has the Veritesting built in. Veritesting dynamically switches between Dynamic Symbolic Execution and Static Symbolic Execution depending on if the code could be reasoned about statically. You can read more about the algorithm here.

Once the branch explosion issue is out of the picture, creating a solution becomes easy. The only problem is that I am getting warnings from angr. I could not find a way to satisfy the warnings, if anyone can point me in the right direction, I would appreciate it.

Final Script

import sys

import pwn
import angr


def main():
    path_to_binary = "./12_angr_veritesting"
    project = angr.Project(path_to_binary)
    initial_state = project.factory.entry_state(
        add_options={
            angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
            angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS,
        },
    )
    simulation = project.factory.simgr(initial_state, veritesting=True)
    simulation.explore(find=is_successful, avoid=should_abort)

    if simulation.found:
        solution_state = simulation.found[0]
        solution = solution_state.posix.dumps(sys.stdin.fileno()).decode()
        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}")


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


if __name__ == "__main__":
    main()