x86_64: Secret Phase

In [1]:
# Imports

import angr
import claripy

We push the input values to the stack and then pop them right before the function exits. Since no value is pushed onto the stack during the execution of the function, we can safely manipulate the stack in the way we planned.

Discover the key to the Secret Phase.

Load the binary.

In [2]:
project = angr.Project('bomb64')

Define the address for the start of the execution path.

In [3]:
# The address where the symbolic execution shall begin. It is the beginning of the middle block where the key phrase is verified.
addr_start = 0x401604

# The address where the hook will be established.
# It is right before the string comparison function.
# Dumps it's arguments and finds out the reference string.
addr_hook = 0x40160E

addr_avoid = 0x401635

addr_target = 0x40162B

Define a blank state for the simulation, a state with most of it's data uninitialized. Pass the address where the state is initialized, along with the user input to be given via standard input.

In [4]:
state = project.factory.blank_state(addr=addr_start)

We define and add the hook to the function.

In [5]:
# Takes the state as initialiser.
class HookClass(angr.SimProcedure):
    def run(self):
        # Dumps the address of the argument to "strings_not_equal" function from the register.
        addr = self.state.regs.esi
        # Dereferences the address of the string and prints it.
        print(self.state.mem[addr].string.concrete)
        return 0

# Adds the hook to the execution flow.
project.hook(addr_hook, HookClass())

Create a simulation manager with this blank state that would help us manage the symbolic execution.

In [6]:
simgr = project.factory.simulation_manager(state)

Run the simulation manager so as to walk over various states.

In [7]:
simgr.explore(find=addr_target, avoid=addr_avoid)

WARNING | 2020-06-16 14:50:04,071 | angr.state_plugins.symbolic_memory | The program is accessing memory or registers with an unspecified value. This could indicate unwanted behavior.
WARNING | 2020-06-16 14:50:04,072 | angr.state_plugins.symbolic_memory | angr will cope with this by generating an unconstrained symbolic variable and continuing. You can resolve this by:
WARNING | 2020-06-16 14:50:04,072 | angr.state_plugins.symbolic_memory | 1) setting a value to the initial state
WARNING | 2020-06-16 14:50:04,072 | angr.state_plugins.symbolic_memory | 2) adding the state option ZERO_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to make unknown regions hold null
WARNING | 2020-06-16 14:50:04,073 | angr.state_plugins.symbolic_memory | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY_REGISTERS}, to suppress these messages.
WARNING | 2020-06-16 14:50:04,074 | angr.state_plugins.symbolic_memory | Filling memory at 0x7fffffffffefff8 with 8 unconstrained bytes referenced from 0x40160e (phase_defused+0x4a in bomb64 (0x40160e))

b'DrEvil'

WARNING | 2020-06-16 14:50:04,408 | angr.engines.successors | Exit state has over 256 possible solutions. Likely unconstrained; skipping. <BV64 mem_7fffffffffefff8_39_64{UNINITIALIZED}>
Out[7]:
<SimulationManager with 1 unconstrained>

There's the string we need to append to the input we provide to the input for phase_4.

Solving the Secret Phase.

Load the binary.

In [8]:
project = angr.Project('bomb64')

Define the address for the start of the execution path.

In [9]:
# The address where the symbolic execution shall begin. It is the actual verification part of the function.
addr_start = 0x40126C

# The address of the return block of phase_7.
addr_target = 0x401282

# The address of the first instruction of the explode_bomb function, which is to be avoided.
addr_bomb = 0x40143A

Define a blank state for the simulation, a state with most of it's data uninitialized. Pass the address where the state is initialized, along with the user input to be given via standard input.

In [10]:
state = project.factory.blank_state(addr=addr_start)

Move a symbolic value into the relevant register.

In [11]:
# A BitVectorSymbol is declared.
user_input = claripy.BVS('user_input', 32)

Add the constraint as observed at the end of the first block.

In [12]:
state.solver.add(user_input<1001)
Out[12]:
[<Bool user_input_79_32 < 0x3e9>]

Store the symbolic value in the register and set others as required to prepare it for further execution of the binary.

In [13]:
state.regs.rax = user_input
state.regs.rbx = state.regs.rax

Create a simulation manager with this blank state that would help us manage the symbolic execution.

In [14]:
simgr = project.factory.simulation_manager(state)

We call the explore method of the simulation manager, tasked with finding an execution path that reaches the target address and avoids the address which explodes the bomb.

In [15]:
simgr.explore(find=addr_target, avoid=addr_bomb, enable_veritesting=True)
Out[15]:
<SimulationManager with 21 active, 1 found, 4 avoid>

We dereference the execution path "found" by the simulation manager and dump the stack.

In [16]:
found = simgr.found[0]
In [17]:
found.solver.eval(user_input, cast_to=int)
Out[17]:
22

And that's the string we have to give as input to pass the secret phase.