x86_64: Phase 2

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.

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 right after parsing of six numbers taken as input.
addr_start = 0x400F0A

# The address of the return of phase_2.
# We end it there so as to dump the stack and retrieve values before the stack frame is discarded.
addr_target = 0x400F3C

# 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 [4]:
state = project.factory.blank_state(addr=addr_start)

Push the symbolic values to be input on the stack.

In [5]:
# From the stack trace show in the picture in the blog,
# we know that the function allocates 4bytes per value and merges two in memory.
# => For values entered to be 1, 2, 4 and 8,
# Stack representation: 0x200000001
#                       0x800000004
# Thus, for 4 input values, two values appear on the stack.

# Therefore, 
# Thus, we push three symbolic values which will appear on the stack for six values as input.
for i in range(3):
    state.stack_push(claripy.BVS("num_{}".format(i), 32))

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

In [6]:
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 [7]:
simgr.explore(find=addr_target, avoid=addr_bomb, enable_veritesting=True)

WARNING | 2020-06-16 00:19:09,048 | 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 00:19:09,049 | 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 00:19:09,052 | angr.state_plugins.symbolic_memory | 1) setting a value to the initial state
WARNING | 2020-06-16 00:19:09,052 | 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 00:19:09,053 | angr.state_plugins.symbolic_memory | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY_REGISTERS}, to suppress these messages.
WARNING | 2020-06-16 00:19:09,054 | angr.state_plugins.symbolic_memory | Filling memory at 0x7fffffffffeffe4 with 4 unconstrained bytes referenced from 0x400f1c (phase_2+0x20 in bomb64 (0x400f1c))
WARNING | 2020-06-16 00:19:09,262 | angr.state_plugins.symbolic_memory | Filling memory at 0x7fffffffffeffec with 4 unconstrained bytes referenced from 0x400f1c (phase_2+0x20 in bomb64 (0x400f1c))
WARNING | 2020-06-16 00:19:09,458 | angr.state_plugins.symbolic_memory | Filling memory at 0x7fffffffffefff4 with 4 unconstrained bytes referenced from 0x400f1c (phase_2+0x20 in bomb64 (0x400f1c))
Out[7]:
<SimulationManager with 1 found, 6 avoid>

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

In [8]:
found = simgr.found[0]
In [9]:
answer = []

# Only 3 iterations since when we pushed the input,
# the values were merged in a way that two numbers were in the same block,
# at the end and the beginning.
# This can be seen when each popped value is printed.
for i in range(3):
    curr = found.solver.eval(found.stack_pop())
    print("Popped value: {0}".format(hex(curr)))
    
    # Masking is done using bit-wise operators to split the values merged in the block.
    lower_end = curr & 0xffffffff
    print("Decimal number on the lower end: {0}".format(lower_end))
    answer.append(str(lower_end))
    higher_end = curr>>32 & 0xffffffff
    answer.append(' ')
    print("Decimal number on the higher end: {0}\n".format(higher_end))
    answer.append(str(higher_end))
    answer.append(' ')

# Removes the space in the end.
''.join(answer[:-1])

Popped value: 0x200000001
Decimal number on the lower end: 1
Decimal number on the higher end: 2

Popped value: 0x800000004
Decimal number on the lower end: 4
Decimal number on the higher end: 8

Popped value: 0x2000000010
Decimal number on the lower end: 16
Decimal number on the higher end: 32
Out[9]:
'1 2 4 8 16 32'

That's the number sequence to be input to pass the second phase.

Since the output we got was correct, we don't need to add that constraint on the first value.