07 Angr Symbolic File

Analyzing the Binary

Checking out main.

It looks like it is reading 0x40 bytes from a file named OJKSQYDP.txt.

It is interesting that the function only compares the first nine bytes of the result, and the string it compares it to is only 8 bytes. From this we know that the ninth character must be a \x00.

Based on this, we know:

• We want the script to start after the scanf
• We need to create a symbolic file
• The symbolic file should be named OJKSQYDP.txt

Lets get going.

Building the Script

The starting point. I chose to set my starting address after the call to ignore_me.

So we set the start_address the filename and the file size in bytes. Then create the project.

path_to_binary = "./07_angr_symbolic_file"

start_address = 0x80488D6
filename = "OJKSQYDP.txt"
symbolic_file_size_bytes = 64
project = angr.Project(path_to_binary)

Next we need to build the symbolic file. This took a bit of reading through the Angr API docs as the instructions will no longer work. Here is how I built the file.

password = claripy.BVS("password0", symbolic_file_size_bytes)
password_file = angr.storage.file.SimFile(
    name=filename,
    content=password,
    size=symbolic_file_size_bytes,
    has_end=True,
)

As we create the initial state of the project we will want to provide the constructor with information on the simfile we just created. In preparation for that, we put it in a dictionary.

symbolic_filesystem = {filename: password_file}

Now we can create our initial state using the start address and the simfile we defined.

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

With the hard parts done we can create the simulation manager and run it.

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

if simulation.found:
    solution_state = simulation.found[0]
    solution = solution_state.solver.eval(password, cast_to=bytes)
    run_binary(solution, path_to_binary)
else:
    raise Exception("Could not find the solution")

Final Script

import sys

import pwn
import angr
import claripy


def main():
    path_to_binary = "./07_angr_symbolic_file"

    start_address = 0x80488D6
    filename = "OJKSQYDP.txt"  # :string
    symbolic_file_size_bytes = 64

    project = angr.Project(path_to_binary)

    password = claripy.BVS("password0", symbolic_file_size_bytes)
    password_file = angr.storage.file.SimFile(
        name=filename,
        content=password,
        size=symbolic_file_size_bytes,
        has_end=True,
    )
    symbolic_filesystem = {filename: password_file}

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

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

    if simulation.found:
        solution_state = simulation.found[0]
        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}")


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()