Back

DragonCTF Runofthemill Writeup

应该是,第一次在做题的时候用Angr吧,发现一个奇怪的问题,记录一下

题目分析

获取输入

v1 = sys_read(0, byte_412000, 0x40uLL);

中间计算

  byte_412000[42] = __ROR1__(byte_412000[42], 4);
  *(_DWORD *)&byte_412000[44] ^= 0x4EC10FC6u;
  *(_WORD *)&byte_412000[15] ^= 0xEBFFu;
  *(_DWORD *)&byte_412000[38] -= 1698263770;
  // 以下省略

最后的验证

  v9 = byte_412000;
  v10 = byte_412050;
  v11 = 64LL;
  v12 = 0;
  do
  {
    v12 |= *v10++ ^ *v9++;
    --v11;
  }
  while ( v11 );

Angr求解

还是很容易看懂的,主要是如何求解

一种思路是把汇编反过来,pizza爷用的是这种做法,于是就写了个Angr喝茶去了

Angr用的是手动往全局变量注入符号,然后在验证前停止,手动添加约束,wp中的写法是直接用程序中的验证,并添加了 LAZY_SOLVES 参数,学到了

之前用自己脚本跑的适合发现一直是 unsat,以为Angr会有问题,但后来发现有个wp就是用的Angr

于是掏出了之前写的脚本做了一些尝试

from angr import *
import claripy
import binascii

input_length = 56

base_addr = 0x400000
proj = Project('runofthemill', main_opts={"base_addr": base_addr})

start_addr = 0x401054
state = proj.factory.blank_state(addr = start_addr, add_options={options.LAZY_SOLVES})
# state.regs.rdi = 0x412000
user_input = [claripy.BVS('input_%d' % i, 8) for i in range(input_length)]

mem_addr = 0x412000
for i in range(input_length):
    state.memory.store(mem_addr + i, user_input[i])
state.add_constraints(state.memory.load(mem_addr, 6) == int(binascii.hexlify(b"DrgnS{"), 16))
simgr = proj.factory.simgr(state)

find_addr = 0x4117FF

simgr.explore(find = find_addr)

ans = [
    0xB5, 0x9C, 0x9A, 0x08, 0x68, 0x91, 0x29, 0x0F, 0xBD, 0x1E, 
    0xFB, 0x71, 0xF4, 0x93, 0x5C, 0xDA, 0x0D, 0x94, 0x10, 0x77, 
    0x6C, 0x41, 0x8D, 0xE2, 0x5E, 0x26, 0xA5, 0x0A, 0x95, 0xE1, 
    0x14, 0xDB, 0x25, 0x0B, 0x09, 0xE4, 0x7B, 0xE7, 0x07, 0x71, 
    0x4E, 0xD3, 0xF2, 0xC1, 0x5C, 0xB2, 0xB4, 0x17, 0x30, 0xAA, 
    0x3D, 0x35, 0x1E, 0x98, 0xC4, 0x92, 0xF4, 0x33, 0x69, 0xCC, 
    0x11, 0xB0, 0xCE, 0xCC
]

if simgr.found:
    print ("end state found")
    end_state = simgr.found[0]
    for i in range(64):
        end_state.add_constraints(end_state.memory.load(mem_addr + i, 1) == ans[i])
    for i in range(input_length):
        print (end_state.solver.eval(user_input[i], cast_to=bytes).decode(), end='')
    print ()
else:
    print ("No result")

最后发现只要把 input_length 设置为56及以下就可以,其他的都是 unsat

capstone学习

TODO

后续学习一下再来补

Built with Hugo
Theme Stack designed by Jimmy