Skip to content

05 Angr Symbolic Memory

Analyzing the Binary

Lets take a look at the decompiled code.

Main

We can tell that the binary uses memset to fill 33 bytes of memory starting at 0xa1ba1c0 with 0's.

Memset

It then stores the results from the scanf call to the four addresses in memory. The scanf call requires four inputs of up to 8 characters each.

Scanf

As before we need to start the program after the call to scanf, but instead of figuring out the stack, we can just set the memory values to our bitvectors directly.

Lets figure out the starting point.

As before our starting address will be right after the scanf call and the cleanup.

Starting Address

Building the Script

We build the initial state.

path_to_binary = "./05_angr_symbolic_memory"
project = angr.Project(path_to_binary)

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

Then lets setup the four bitvectors we will need.

input_length_in_bits = 8 * 8
password0 = claripy.BVS("password0", input_length_in_bits)
password1 = claripy.BVS("password1", input_length_in_bits)
password2 = claripy.BVS("password2", input_length_in_bits)
password3 = claripy.BVS("password3", input_length_in_bits)

Now we are going to insert each bitvector into the appropriate address.

initial_state.memory.store(0x0A1BA1C0, password0)
initial_state.memory.store(0x0A1BA1C8, password1)
initial_state.memory.store(0x0A1BA1D0, password2)
initial_state.memory.store(0x0A1BA1D8, password3)

Build the simulation manager and let it go. Much easier when we don't have to mess with the stack!

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 = "./05_angr_symbolic_memory"
    project = angr.Project(path_to_binary)

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

    input_length_in_bits = 8 * 8
    password0 = claripy.BVS("password0", input_length_in_bits)
    password1 = claripy.BVS("password1", input_length_in_bits)
    password2 = claripy.BVS("password2", input_length_in_bits)
    password3 = claripy.BVS("password3", input_length_in_bits)

    initial_state.memory.store(0x0A1BA1C0, password0)
    initial_state.memory.store(0x0A1BA1C8, password1)
    initial_state.memory.store(0x0A1BA1D0, password2)
    initial_state.memory.store(0x0A1BA1D8, password3)

    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, cast_to=bytes).decode()
        solution1 = solution_state.solver.eval(password1, cast_to=bytes).decode()
        solution2 = solution_state.solver.eval(password2, cast_to=bytes).decode()
        solution3 = solution_state.solver.eval(password3, cast_to=bytes).decode()
        solution = " ".join([solution0, solution1, solution2, solution3])

        run_binary(solution, path_to_binary)
    else:
        raise Exception("Could not find the solution")


if __name__ == "__main__":
    main()
Back to top