I am trying to solve the CTF example as given at 04_angr_symbolic_stack. As per the instructions, we have to setup the stack before proceeding with symbolic execution. Using binary ninja for disassembling a 64-bit binary, the code that handles the input is as follows
void var_18 {Frame offset -18}
int32_t var_10 {Frame offset -10}
int32_t var_c {Frame offset -c}
int64_t __saved_rbp {Frame offset -8}
void* const __return_addr {Frame offset 0}
00401375 handle_user:
00401375 f30f1efa endbr64
00401379 55 push rbp {__saved_rbp}
0040137a 4889e5 mov rbp, rsp {__saved_rbp}
0040137d 4883ec10 sub rsp, 0x10
00401381 488d55f8 lea rdx, [rbp-0x8 {var_10}]
00401385 488d45fc lea rax, [rbp-0x4 {var_c}]
00401389 4889c6 mov rsi, rax {var_c}
0040138c bf07204000 mov edi, 0x402007 {"%u %u"}
00401391 b800000000 mov eax, 0x0
00401396 e8e5fcffff call __isoc99_scanf
0040139b 8b45fc mov eax, dword [rbp-0x4 {var_c}]
0040139e 89c7 mov edi, eax
004013a0 e8f0fdffff call complex_function0
004013a5 8945fc mov dword [rbp-0x4 {var_c}], eax
004013a8 8b45f8 mov eax, dword [rbp-0x8 {var_10}]
004013ab 89c7 mov edi, eax
004013ad e8d3feffff call complex_function1
004013b2 8945f8 mov dword [rbp-0x8 {var_10}], eax
004013b5 8b45fc mov eax, dword [rbp-0x4 {var_c}]
004013b8 3d71e279e3 cmp eax, 0xe379e271
004013bd 750a jne 0x4013c9
TLDR; 16 bytes have been reserved on the stack for local variables. To simulate this in angr, we perform the same steps
Here is my attempt
import angr
import claripy
import sys
p = angr.Project('binaries/04_angr_symbolic_stack',
load_options={'auto_load_libs': False})
s = p.factory.blank_state(addr=0x40139b, add_options={
angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS
})
# follow the disassembly
# 0040137a 4889e5 mov rbp, rsp {__saved_rbp}
# set value of rbp = rsp
s.regs.rbp = s.regs.rsp
# create 2 bitvectors for input
# 0040138c bf07204000 mov edi, 0x402007 {"%u %u"}
s0 = claripy.BVS("s0", 32)
s1 = claripy.BVS("s1", 32)
# int32_t var_10 {Frame offset -10}
# int32_t var_c {Frame offset -c}
# setup the stack as per this, s0(1st %u of scanf) is at rsp - 12 and s1(2nd %u of scanf) is at rsp - 16
s.regs.rsp -= 16
# push the bitvectors(inputs) on tht stack, in reverse order
s.stack_push(s1)
s.stack_push(s0)
simgr = p.factory.simgr(s)
def is_successful(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Good Job.'.encode() in stdout_output
def should_abort(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Try again.'.encode() in stdout_output
simgr.explore(find=is_successful, avoid=should_abort)
if simgr.found:
solution_state = simgr.found[0]
solution0 = solution_state.solver.eval(s0)
solution1 = solution_state.solver.eval(s1)
solution = ' '.join(map(str, [ solution0, solution1 ]))
print(solution)
else:
raise Exception('Could not find the solution')
Leading me to the error angr.errors.SimMemoryError: Not enough data for store at s.stack_push(s1). What am I missing here?
Referring @Jester's comment, I modified my solution to include the 2, 32-bit bitvectors as a single 64-bit bitvector using claripy.Concat. stack_push decrements rsp. And lines
00401381 488d55f8 lea rdx, [rbp-0x8 {var_10}] # 2nd input variable
00401385 488d45fc lea rax, [rbp-0x4 {var_c}] # 1st input variable
reveal that the input variables are stored at locations rsp-0x0 and rsp-0x4. Complete solution is as follows
import angr
import claripy
import sys
p = angr.Project('binaries/04_angr_symbolic_stack',
load_options={'auto_load_libs': False})
s = p.factory.blank_state(addr=0x40139b, add_options={
angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS
})
# follow the disassembly
# 0040137a 4889e5 mov rbp, rsp {__saved_rbp}
# set value of rbp = rsp
s.regs.rbp = s.regs.rsp
# create 2 bitvectors for input
# 0040138c bf07204000 mov edi, 0x402007 {"%u %u"}
s0 = claripy.BVS("s0", 32)
s1 = claripy.BVS("s1", 32)
# On 64 bit machine, pushing 4 bytes is not allowed. Concat both bitvectors as one 64 bit wide bitvector
s64 = claripy.Concat(s0, s1)
# setup the stack as per this
# 00401381 488d55f8 lea rdx, [rbp-0x8 {var_10}] # 2nd input variable
# 00401385 488d45fc lea rax, [rbp-0x4 {var_c}] # 1st input variable
# no stack pointer manipulation needed
# push the bitvectors(inputs) on the stack, rsp = rsp - 0x8
s.stack_push(s64)
simgr = p.factory.simgr(s)
def is_successful(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Good Job.'.encode() in stdout_output
def should_abort(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Try again.'.encode() in stdout_output
simgr.explore(find=is_successful, avoid=should_abort)
if simgr.found:
solution_state = simgr.found[0]
solution0 = solution_state.solver.eval(s64)
solution = ' '.join(map(str, [s64]))
sol1 = s64[63:32]
sol2 = s64[31:0]
print(solution_state.solver.eval(sol1), solution_state.solver.eval(sol2))
else:
raise Exception('Could not find the solution')