assemblyreverse-engineeringctfsymbolic-executionangr

"Not enough data for store" while solving Angr CTF example


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

  1. Set rbp = rsp
  2. Initialise 32-bit bitvectors representing inputs given in format string of scanf
  3. Decrement rsp by 16
  4. Push bitvectors on the stack

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?


Solution

  • 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')