# 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.
project = angr.Project('bomb64')
Define the address for the start of the execution path.
# The address where the symbolic execution shall begin. It is the beginning of the phase_6 function.
addr_start = 0x40110B
# The address of the return of phase_6.
# We end it there so as to dump the stack and retrieve values before the stack frame is discarded.
addr_target = 0x4011F7
# 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.
state = project.factory.blank_state(addr=addr_start)
Push the symbolic values to be input on the stack.
# 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.
num = []
for i in range(3):
num.append(claripy.BVS("num_{}".format(i), 32))
for i in range(3):
state.stack_push(num[i])
Setup the registers according to the disassembly.
state.regs.r13 = state.regs.rsp
Create a simulation manager with this blank state that would help us manage the symbolic execution.
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.
simgr.explore(find=addr_target, avoid=addr_bomb, enable_veritesting=True)
We dereference the execution path "found" by the simulation manager and dump the stack.
found = simgr.found[0]
We make the necessary changes in order to yield the correct output.
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.
answer = ''.join(answer[:-1])
answer
Reversing the manipulations to get the final, correct sequence of values that we need to provide as input.
result = [7-int(i) for i in answer.split() if i.isdigit()]
final_answer = ""
for num in result:
final_answer += str(num) + ' '
final_answer[:-1]
Voilà! Yet again, there's the input we need to give to pass the sixth phase.
Do the precursors.
# Load the binary.
project = angr.Project('bomb64')
# Init the addresses.
# The address is the beginning of the phase_6 function.
addr_start = 0x4010F4
addr_target = 0x4011F7
addr_bomb = 0x40143A
# Init a blank state.
state = project.factory.blank_state(addr=addr_start)
Define a hook to successfully return the read_six_numbers function.
# The address of the function that maps the integers to their appropriate locations in memory.
read_six_numbers = 0x040145C
# Hook read_six_numbers function with a stub as we will write our numbers directly to memory.
stub_func = angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained']
project.hook(read_six_numbers, stub_func())
This time we hope to directly write to the memory instead of pushing the values to the stack.
# The address of the array of numbers in the memory.
numbers_array = 0x00007fffffffdf00
# Symbolic values instantiated and loaded in an array.
numbers = [state.solver.BVS("num" + str(i), 32) for i in range(6)]
# Symbolic values stored in the memory in the location of the numbers.
# The data type uint8_t matching the bit size of the symbolic values.
for i in range(6):
state.mem[numbers_array + 4 * i].uint32_t= numbers[i]
Executing the exploration.
# Init the simulation manager.
simgr = project.factory.simulation_manager(state)
# Let Angr explore.
simgr.explore(find=addr_target, avoid=addr_bomb, enable_veritesting=True)
# Get the answer from the found state.
found = simgr.found[0]
answer = []
# Loop to extract answers from the stack.
# Takes care of reversing the manipulations in between.
for i in range(3):
curr = found.solver.eval(found.stack_pop())
print("Popped value: {0}".format(hex(curr)))
lower_end = curr & 0xffffffff
print("Decimal number on the lower end: {0}".format(lower_end))
answer.append(str(7 - lower_end))
higher_end = curr>>32 & 0xffffffff
answer.append(' ')
print("Decimal number on the higher end: {0}\n".format(higher_end))
answer.append(str(7 - higher_end))
answer.append(' ')
# Removes the space in the end.
''.join(answer[:-1])