解决Angr CTF示例时遭遇Not enough data for store错误求助

问题描述 #

我正尝试解决GitHub上的Angr CTF 04_angr_symbolic_stack示例，需在符号执行前配置栈。通过Binary Ninja反汇编64位二进制文件后，按以下步骤模拟栈操作：

• 设置rbp = rsp；
• 初始化对应scanf格式字符串的32位符号位向量；
• 将rsp减16；
• 向栈推入位向量。

但执行s.stack_push(s1)时触发angr.errors.SimMemoryError: Not enough data for store错误。

汇编代码 #

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

我的实现代码 #

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

问题分析与解决 #

错误原因 #

1. stack_push长度不匹配：64位环境下，stack_push默认处理8字节（64位）栈元素，但你传入的是32位符号位向量，长度不匹配导致存储失败。
2. 栈帧模拟逻辑错误：从0x40139b开始执行时，前面的push rbp、mov rbp,rsp、sub rsp,0x10指令已经完成栈帧初始化，无需手动调整rsp和rbp；且汇编中变量通过rbp偏移访问，直接push会破坏栈帧布局。

修正后的代码 #

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

# 创建两个32位符号变量，对应scanf的两个输入
s0 = claripy.BVS("s0", 32)
s1 = claripy.BVS("s1", 32)

# 直接通过rbp偏移写入栈变量，匹配汇编布局：
# var_c 对应 rbp-0x4，是第一个scanf输入
# var_10 对应 rbp-0x8，是第二个scanf输入
s.mem[s.regs.rbp - 0x4].dword = s0
s.mem[s.regs.rbp - 0x8].dword = s1

simgr = p.factory.simgr(s)

def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return b'Good Job.' in stdout_output

def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    return b'Try again.' 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)
    print(f"{solution0} {solution1}")
else:
    raise Exception('Could not find the solution')

修正说明 #

• 用s.mem[...].dword直接写入32位变量，完美匹配汇编中栈变量的宽度和位置，避免stack_push的64位限制问题。
• 移除手动调整rbp和rsp的代码，从0x40139b执行时栈帧已由前置指令初始化完成，angr会自动维护正确的寄存器状态。
• 简化成功/失败判断的字符串编码，直接用字节串更高效。

内容的提问来源于stack exchange，提问作者Rinkesh P