解决 Angr CTF 示例时“没有足够的数据用于存储”

Question

我正在尝试解决04_angr_symbolic_stack中给出的CTF示例。根据说明，我们必须在继续符号执行之前设置堆栈。使用binary ninja反汇编64位二进制文件，处理输入的代码如下

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 个字节。为了在 angr 中模拟这一点，我们执行相同的步骤

1. 设置 rbp = rsp
2. 初始化表示以 scanf 格式字符串给出的输入的 32 位位向量
3. 将 rsp 减少 16
4. 将位向量压入堆栈

这是我的尝试

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

导致我在

angr.errors.SimMemoryError: Not enough data for store

处出现错误

s.stack_push(s1)

。我在这里缺少什么？

Answer 1

参考@Jester的评论，我修改了我的解决方案，使用claripy.Concat将

2个32位位向量作为单个64位位向量

包含在内。

stack_push

递减

rsp

。还有线条

00401381  488d55f8           lea     rdx, [rbp-0x8 {var_10}] # 2nd input variable
00401385  488d45fc           lea     rax, [rbp-0x4 {var_c}] # 1st input variable 

表明输入变量存储在位置

rsp-0x0

和

rsp-0x4

。完整解决方案如下

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