Back
Featured image of post angr ctf writeup
Labs

angr ctf writeup

开始学angr

就是在抄solution

find

from angr import *

proj = Project('./00_angr_find', load_options={'auto_load_libs': False}, main_opts={'base_addr':0x8048000})
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
find_addr = 0x8048675
simgr.explore(find = find_addr)

if simgr.found:
    simulations = simgr.found[0]
    print (simulations.posix.dumps(0))
else:
    print ('no result')

先用 Project 导入二进制文件

然后 state 为开始模拟时的状态，entry_state 为从入口点开始模拟

simgr 是为 simulation_manager 导入这个状态，进行模拟执行

explore 为模拟器设定了一个执行的目标，遇到avoid将停止执行，遇到find则会添加到found状态中，这里填写的是输出 Success 字符串的地址

最后从found中dumps出标准输入的值，就可以拿到flag

avoid

from angr import *

base_addr = 0x8048000
find_addr = 0x80485E0
avoid_addr = [0x80485A8, 0x80485F2]
proj = Project('./01_angr_avoid', main_opts={'base_addr': base_addr})

state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)

simgr.explore(find = find_addr, avoid = avoid_addr)

if simgr.found:
    simulation = simgr.found[0]
    print (simulation.posix.dumps(0))
else:
    print ("no result")

没什么区别，就是增加了一个avoid参数

find condition

from angr import *

proj = Project('./02_angr_find_condition', main_opts={'base_addr': 0x8048000})
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)

def find_condition(cur_state):
    output = cur_state.posix.dumps(1)
    return b'Good Job.' in output

def avoid_condition(cur_state):
    output = cur_state.posix.dumps(1)
    return b'Try again.' in output

simgr.explore(find=find_condition, avoid=avoid_condition)

if simgr.found:
    print (simgr.found[0].posix.dumps(0))
else:
    print ("no result")

explore 中，可以将find和avoid的参数设置为函数，当各种输出太多的时候，这种方法比较省事，而且可拓展性很强

dumps(1) 则是从状态中获取标准输出

symbolic registers

symbolic的几个实验就是往初始状态里注入符号了

from angr import *
import claripy

proj = Project('./03_angr_symbolic_registers', main_opts={'base_addr':0x8048000})
after_input_addr = 0x8048980
state = proj.factory.blank_state(addr = after_input_addr)

user_input = [claripy.BVS('user_input_%d' % i, 32) for i in range(3)]

state.regs.eax = user_input[0]
state.regs.ebx = user_input[1]
state.regs.edx = user_input[2]

find_addr = 0x80489E9
avoid_addr = 0x80489D7

simgr = proj.factory.simgr(state)
simgr.explore(find = find_addr, avoid = avoid_addr)

if simgr.found:
    for a in user_input:
        print ('%x' % simgr.found[0].se.eval(a), end = ' ')
    print ()
else:
    print ("no result")

claripy 是 angr 中的约束求解器，z3 好像就是fork出来的

主要使用 state.regs.eax 之类的将符号注入到寄存器中

这里用寄存器是因为输入被存储到了寄存器中

main 函数

.text:0804897B                 call    get_user_input
.text:08048980                 mov     [ebp+var_14], eax    ; state starts here
.text:08048983                 mov     [ebp+var_10], ebx
.text:08048986                 mov     [ebp+var_C], edx

get_user_input 内部实现

.text:0804892F                 call    ___isoc99_scanf
.text:08048934                 add     esp, 10h
.text:08048937                 mov     ecx, [ebp+var_18]
.text:0804893A                 mov     eax, ecx
.text:0804893C                 mov     ecx, [ebp+var_14]
.text:0804893F                 mov     ebx, ecx
.text:08048941                 mov     ecx, [ebp+var_10]
.text:08048944                 mov     edx, ecx

写这题的时候，不小心把 blank_state 打成了 entry_state，但还是可以得到正确结果，不知道为啥

symbolic stack

这题的输入直接存到了 stack 中，因此需要把符号注入到 stack

.text:08048682                 lea     eax, [ebp+var_10]     ; 2nd input stores here
.text:08048685                 push    eax
.text:08048686                 lea     eax, [ebp+var_C]      ; 1st input stores here
.text:08048689                 push    eax
.text:0804868A                 push    offset aUU      ; "%u %u"
.text:0804868F                 call    ___isoc99_scanf
.text:08048694                 add     esp, 10h
.text:08048697                 mov     eax, [ebp+var_C]      ; state starts here
.text:0804869A                 sub     esp, 0Ch

from angr import *
import claripy

proj = Project('./04_angr_symbolic_stack', main_opts={'base_addr':0x8048000})
after_input_addr = 0x8048697
state = proj.factory.entry_state(addr=after_input_addr)

user_input = [claripy.BVS('input_%d' % i, 32) for i in range(2)]

# state.regs.ebp = state.regs.esp
state.regs.esp = state.regs.ebp - 8
state.stack_push(user_input[0])
state.stack_push(user_input[1])

simgr = proj.factory.simgr(state)

find_addr = 0x80486E4
avoid_addr = 0x80486D2

simgr.explore(find=find_addr, avoid=avoid_addr)

if simgr.found:
    for a in user_input:
        print (simgr.found[0].se.eval(a), end = ' ')
    print ()
else:
    print ("no result")

用的方法是 stack_push，所以需要先把 esp 设置好

剩下的应该没什么变化

symbolic memory

这题是输入存到了 .bss 段中

.text:080485E0                 push    offset unk_A1BA1D8
.text:080485E5                 push    offset unk_A1BA1D0
.text:080485EA                 push    offset unk_A1BA1C8
.text:080485EF                 push    offset user_input
.text:080485F4                 push    offset a8s8s8s8s ; "%8s %8s %8s %8s"
.text:080485F9                 call    ___isoc99_scanf
.text:080485FE                 add     esp, 20h
.text:08048601                 mov     [ebp+var_C], 0       ; state starts here
.text:08048608                 jmp     short loc_8048637

from angr import *
import claripy

proj = Project('./05_angr_symbolic_memory', main_opts={"base_addr":0x8048000})

start_addr = 0x8048601
state = proj.factory.blank_state(addr = start_addr)

user_input = [claripy.BVS('input_%d' % i, 8) for i in range(32)]

for u in user_input:
    state.solver.add(u >= 0x20)
    state.solver.add(u <= 0x7f)

mem_addr = 0xA1BA1C0
for i in range(32):
    state.memory.store(mem_addr + i, user_input[i])

simgr = proj.factory.simgr(state)

find_addr = 0x8048672
avoid_addr = 0x804865B

simgr.explore(find=find_addr, avoid=avoid_addr)

if simgr.found:
    for i in range(32):
        if i % 8 == 0 and i != 0:
            print (' ', end = '')
        print (chr(simgr.found[0].se.eval(user_input[i])), end = '')
    print ()
else:
    print ("no result")

用的是 memory.store(store_addr, store_symbolic) 方法

symbolic dynamic memory

  buffer0 = (char *)malloc(9u);
  buffer1 = (char *)malloc(9u);
  memset(buffer0, 0, 9u);
  memset(buffer1, 0, 9u);
  printf("Enter the password: ");
  __isoc99_scanf("%8s %8s", buffer0, buffer1, v6);

这题的输入存储到了 malloc 中，这个地址动态的，如果仅仅使用 memory.store() 无法确定存储的地址

因此先将 buffer 的地址修改为一个自定义的虚假地址（因为 buffer 在 .bss 段上，地址是固定的），然后往这个地址中写入数据，后续程序的模拟执行会使用这个虚假地址

from angr import *
import claripy

proj = Project('./06_angr_symbolic_dynamic_memory', main_opts={'base_addr':0x8048000})

state_addr = 0x8048699
state = proj.factory.blank_state(addr = state_addr)

buffer0_addr = 0xABCC8A4
buffer1_addr = 0xABCC8AC

fake_heap_addr0 = 0xDEADBE00
fake_heap_addr1 = 0xDEADBF00

state.memory.store(buffer0_addr, fake_heap_addr0, endness=proj.arch.memory_endness)
state.memory.store(buffer1_addr, fake_heap_addr1, endness=proj.arch.memory_endness)

user_input = [claripy.BVS('input_%d' % i, 8 * 8) for i in range(2)]
state.memory.store(fake_heap_addr0, user_input[0])
state.memory.store(fake_heap_addr1, user_input[1])

simgr = proj.factory.simgr(state)

find_addr = 0x8048759
avoid_addr = 0x8048747

simgr.explore(find=find_addr, avoid=avoid_addr)

if simgr.found:
    print (simgr.found[0].se.eval(user_input[0], cast_to=bytes).decode(), simgr.found[0].se.eval(user_input[1], cast_to=bytes).decode())
else:
    print ("no result")

symbolic file

这题没有用预期做法来做

  fp = fopen("OJKSQYDP.txt", "rb");
  fread(buffer, 1u, 0x40u, fp);
  fclose(fp);
  unlink("OJKSQYDP.txt");

既然这里有个从文件读取，那么可以直接把初始状态设置到文件读取后面，那么这道题就和之前做过的 symbolic memory 一样了

from angr import *
import claripy

proj = Project('./07_angr_symbolic_file', main_opts={'base_addr':0x8048000})

init_addr = 0x804893C
state = proj.factory.blank_state(addr=init_addr)

user_input = claripy.BVS('user_input', 8 * 8)
mem_addr = 0x804A0A0
state.memory.store(mem_addr, user_input)

simgr = proj.factory.simgr(state)

find_addr = 0x80489B0
avoid_addr = 0x8048996

simgr.explore(find=find_addr, avoid=avoid_addr)

if simgr.found:
    print (simgr.found[0].se.eval(user_input))
else:
    print ('no result')

constraints

这题的解法是对运算结果手动做约束，不知道为什么用之前的方法做不出来

from angr import *
import claripy

proj = Project('./08_angr_constraints', load_options={'auto_load_libs':False}, main_opts={'base_addr':0x8048000})

start_addr = 0x8048625
start_state = proj.factory.blank_state(addr = start_addr)

flag = claripy.BVS('flag', 8 * 16)
buffer_addr = 0x804A050

start_state.memory.store(buffer_addr, flag)

end_addr = 0x804866E
simgr = proj.factory.simgr(start_state)

simgr.explore(find = end_addr)

if simgr.found:
    end_state = simgr.found[0]
    calc_res = end_state.memory.load(buffer_addr, 16)
    cipher = b"AUPDNNPROEZRJWKB"
    end_state.add_constraints(calc_res == cipher)
    print (end_state.se.eval(flag, cast_to=bytes))
else:
    print ('fail')

仅模拟了for循环（加密部分），运行结束后直接使用 add_constraints 手动添加约束条件

hook

又来了次非预期

  printf("Enter the password: ");
  __isoc99_scanf("%16s", buffer);
  for ( i = 0; i <= 15; ++i )
    *(_BYTE *)(i + 134520916) = complex_function(*(char *)(i + 0x804A054), 18 - i);
  equals = check_equals_XYMKBKUHNIQYNQXE(buffer, 16);
  for ( j = 0; j <= 15; ++j )
    *(_BYTE *)(j + 0x804A044) = complex_function(*(char *)(j + 134520900), j + 9);
  __isoc99_scanf("%16s", buffer);
  v3 = equals && !strncmp(buffer, password, 0x10u);

显然，这道题可以拆成两部分来做，第一部分使用 constraints 求解第一次输入；第二部分直接获取 password 的运算结果

于是相当于写了两次 angr（感觉完全可以合并起来，但稳妥起见，后面再试试）

from angr import *
import claripy

proj = Project('./09_angr_hooks')

start_state = 0x8048665
user_input = claripy.BVS('user_input', 8 * 16)

init_state = proj.factory.blank_state(addr = start_state)
buffer_addr = 0x804A054
init_state.memory.store(buffer_addr, user_input)

simgr = proj.factory.simgr(init_state)

end_addr = 0x80486AC
simgr.explore(find = end_addr)

if simgr.found:
    solution_state = simgr.found[0]
    result = solution_state.memory.load(buffer_addr, 16)
    solution_state.add_constraints(b"XYMKBKUHNIQYNQXE" == result)
    print (solution_state.solver.eval(user_input, cast_to=bytes).decode())
else:
    print ("fail")

second_start = 0x80486C0
second_state = proj.factory.blank_state(addr = second_start)

second_state.memory.store(0x804A044, b"XYMKBKUHNIQYNQXE")

second_simgr = proj.factory.simgr(second_state)

second_simgr.explore(find = 0x8048700)

if second_simgr.found:
    result = second_simgr.found[0].memory.load(0x804A044, 16)
    print (second_simgr.found[0].solver.eval(result, cast_to=bytes).decode())
else:
    print ("no result")

运行结果

Enter the password: ZXIDRXEORJOTFFJN
WUFAOUBLOGLQCCGK
Good Job.

补上用hook写的，用了两种hook的写法（看到simprocedures那题才发现第二个是下一题的写法）

from angr import *
import claripy

proj = Project('./09_angr_hooks')

start_state = proj.factory.entry_state()

check_addr = 0x80486B3
instraction_len = 5

choose_hook = 1

if choose_hook == 1:
	@proj.hook(check_addr, length = instraction_len)
	def replace_check_equal(state):
		target = b'XYMKBKUHNIQYNQXE' # claripy will convert it to bytes if it is str.
		input_addr = 0x804A054
		cipher = state.memory.load(input_addr, 0x10)
		state.regs.eax = claripy.If(cipher == target, claripy.BVV(1, 32), claripy.BVV(0, 32))

if choose_hook == 2:
	class replace_check_equal(SimProcedure):
		def run(self):
			target = b'XYMKBKUHNIQYNQXE'
			input_addr = 0x804A054
			cipher = self.state.memory.load(input_addr, 0x10)
			return claripy.If(cipher == target, claripy.BVV(1, 32), claripy.BVV(0, 32))

	check_equal_symbol = 'check_equals_XYMKBKUHNIQYNQXE'
	proj.hook_symbol(check_equal_symbol, replace_check_equal())

simgr = proj.factory.simgr(start_state)

def is_success(state):
	output = state.posix.dumps(1)
	return b'Good Job.' in output
def should_avoid(state):
	output = state.posix.dumps(1)
	return b'Try again.' in output

simgr.explore(find = is_success, avoid = should_avoid)

if simgr.found:
	print (simgr.found[0].posix.dumps(0))
else:
	print ('no solution')

simprocedures

同样先用之前的方法写了一遍

from angr import *
import claripy

proj = Project('./10_angr_simprocedures')

start_addr = 0x80486C3
init_state = proj.factory.blank_state(addr = start_addr)

init_state.regs.esp = init_state.regs.ebp - 0xD

user_input1 = claripy.BVS('user_input1', 8 * 4)
user_input2 = claripy.BVS('user_input2', 8 * 4)
user_input3 = claripy.BVS('user_input3', 8 * 4)
user_input4 = claripy.BVS('user_input4', 8 * 4)
init_state.stack_push(user_input4)
init_state.stack_push(user_input3)
init_state.stack_push(user_input2)
init_state.stack_push(user_input1)

init_state.regs.esp = init_state.regs.ebp - 0x28

simgr = proj.factory.simgr(init_state)

check_addr = 0x80499F1
simgr.explore(find = check_addr)

ans = b"ORSDDWXHZURJRBDH"

if simgr.found:
    solution_state = simgr.found[0]
    input_addr = solution_state.regs.ebp - 0x1D
    result1 = solution_state.memory.load(input_addr, 4)
    result2 = solution_state.memory.load(input_addr + 4, 4)
    result3 = solution_state.memory.load(input_addr + 8, 4)
    result4 = solution_state.memory.load(input_addr + 12, 4)
    solution_state.add_constraints(ans[:4] == result1)
    solution_state.add_constraints(ans[4:8] == result2)
    solution_state.add_constraints(ans[8:12] == result3)
    solution_state.add_constraints(ans[12:] == result4)
    print (solution_state.solver.eval(user_input1, cast_to=bytes).decode()[::-1], end = '')
    print (solution_state.solver.eval(user_input2, cast_to=bytes).decode()[::-1], end = '')
    print (solution_state.solver.eval(user_input3, cast_to=bytes).decode()[::-1], end = '')
    print (solution_state.solver.eval(user_input4, cast_to=bytes).decode()[::-1])
else:
    print ("no result")

然后用 hook_symbol 试试

from angr import *
import claripy

proj = Project('./10_angr_simprocedures')

start_state = proj.factory.entry_state()

class replace_check_equals(SimProcedure):
    def run(self, to_check, length):
        target = b'ORSDDWXHZURJRBDH'
        result = self.state.memory.load(to_check, length)
        return claripy.If(result == target, claripy.BVV(1, 32), claripy.BVV(0, 32))

check_equals_sym = 'check_equals_ORSDDWXHZURJRBDH'
proj.hook_symbol(check_equals_sym, replace_check_equals())

simgr = proj.factory.simgr(start_state)

def is_successful(state):
    output = state.posix.dumps(1)
    return b'Good Job.' in output
def should_abort(state):
    output = state.posix.dumps(1)
    return b'Try again.' in output

simgr.explore(find = is_successful, avoid = should_abort)

if simgr.found:
    print (simgr.found[0].posix.dumps(0))
else:
    print ('no result')

sim_scanf

simProcedure 其实是 angr 用于缓解路径爆炸的一个策略，将一些有可能导致路径爆炸的库函数进行了重写，然而 angr 提供的重写可能存在不完善的地方，例如 scanf 无法支持多个参数，因此这道题目中，需要自己重写 scanf 的 SimProcedure，实现接收两个参数

这道题主要学到的就是利用 globals 存储注入的符号

from angr import *
import claripy

proj = Project('./11_angr_sim_scanf')

start_state = proj.factory.entry_state()

start_state.globals['inputs'] = []
class replace_scanf(SimProcedure):
    def run(self, fmt, input1, input2):
        user_input1 = claripy.BVS('user_input1', 32)
        user_input2 = claripy.BVS('user_input2', 32)
        self.state.memory.store(input1, user_input1, endness = proj.arch.memory_endness)
        self.state.memory.store(input2, user_input2, endness = proj.arch.memory_endness)
        self.state.globals['inputs'].append((user_input1, user_input2))

scanf_sym = "__isoc99_scanf"
proj.hook_symbol(scanf_sym, replace_scanf())

simgr = proj.factory.simgr(start_state)

def is_success(state):
    output = state.posix.dumps(1)
    return b'Good Job.' in output
def should_avoid(state):
    output = state.posix.dumps(1)
    return b'Try again.' in output

simgr.explore(find = is_success, avoid = should_avoid)

if simgr.found:
    solution_state = simgr.found[0]
    for res in solution_state.globals['inputs']:
        print (solution_state.solver.eval(res[0]), end=' ')
        print (solution_state.solver.eval(res[1]))
else:
    print ('no result')

veritesting

设置 simulation_manager 时，启用 veritesting 可以缓解一定程度的路径爆炸

from angr import *
import claripy

proj = Project('./12_angr_veritesting')

start_state = proj.factory.entry_state()

simgr = proj.factory.simgr(start_state, veritesting=True)

def is_success(state):
    output = state.posix.dumps(1)
    return b'Good' in output
def should_avoid(state):
    output = state.posix.dumps(1)
    return b'Try' in output

simgr.explore(find = is_success, avoid = should_avoid)

if simgr.found:
    print (simgr.found[0].posix.dumps(0))
else:
    print ('No result')

简单学习了一下 veritesting 的原理，在本题目的验证环节，代码为

  for (int i=0; i<32; ++i) {
    if (buffer[i] == complex_function(${ write('\'' + letter0 + '\'' ) }$, i + ${ write(integer) }$) ) {
      counter0++;
    }
  }

如果单纯以分支图来话，总共引入了 $2^{32}$ 种可能，然而事实上只有满足和不满足两种情况

开启 veritesting 后，angr会在遇到基础代码（无系统调用，间接跳转等语句）时，从动态符号执行（为每一条路径生成一个表达式）切换到静态符号执行（将程序转换为表达式）。因此，在执行这个循环时，先动态恢复控制流图，找到静态符号执行容易分析和难以分析的语句，并推断出易分析节点到难分析节点的影响，最后切换回动态分析来处理不易处理的情况。

static binary

在 sim_scanf 中说到，angr 将部分库函数替换为自己实现的 SimProcedures 来避免路径爆炸，但当遇到静态编译的二进制文件时，由于没有调用库函数，这些静态的函数就有可能造成路径爆炸，需要我们手动替换为 SimProcedures

from angr import *

proj = Project('./13_angr_static_binary')

start_state = proj.factory.entry_state()

proj.hook(0x804ED40, SIM_PROCEDURES['libc']['printf']())
proj.hook(0x804ED80, SIM_PROCEDURES['libc']['scanf']())
proj.hook(0x804F350, SIM_PROCEDURES['libc']['puts']())
proj.hook(0x8048D10, SIM_PROCEDURES['glibc']['__libc_start_main']())

simgr = proj.factory.simgr(start_state, veritesting = True)

def is_success(state):
	output = state.posix.dumps(1)
	return b'Good Job.' in output
def should_avoid(state):
	output = state.posix.dumps(1)
	return b'Try again.' in output

simgr.explore(find = is_success, avoid = should_avoid)

if simgr.found:
	solution = simgr.found[0]
	print (solution.posix.dumps(0))
else:
	print ('No result')

shared library

这道题目将加密部分放到了 so 文件中，因此需要执行 so 文件

在执行时遇到的问题有

  • 基地址不确定：使用 base_addr 来控制程序的基地址
  • 符号注入的地址未知：使用 call_state 来控制函数调用时的参数
from angr import *
import claripy

base_addr = 0x400000
proj = Project('./lib14_angr_shared_library.so', main_opts={'base_addr':base_addr})

store_addr = 0x300000

init_state = proj.factory.call_state(base_addr + 0x6d7, store_addr, claripy.BVV(8, 32))

user_input = claripy.BVS('user_input', 8 * 8)
init_state.memory.store(store_addr, user_input, endness = proj.arch.memory_endness)

find_addr = base_addr + 0x775
simgr = proj.factory.simgr(init_state)

simgr.explore(find = find_addr)

if simgr.found:
	solution = simgr.found[0]
	solution.add_constraints(solution.regs.eax != 0)
	print (solution.solver.eval(user_input, cast_to=bytes))
else:
	print ('no result')

arbitrary read

这道题有些复杂，由于需要让输入的部分溢出，控制 puts 的输出参数

同样需要替换 scanf，同时，这道题目为了减小输入的可能性，需要手动添加一下对输入的约束，要求在可见字符范围内

from angr import *
import claripy

proj = Project('./15_angr_arbitrary_read')

init_state = proj.factory.entry_state()

class replace_scanf(SimProcedure):
	def run(self, fmt, key_addr, stack_addr):
		user_input1 = claripy.BVS('user_input1', 32)
		user_input2 = claripy.BVS('user_input2', 20 * 8)

		for i in user_input2.chop(bits = 8):
			self.state.add_constraints(i > 0x20)
			self.state.add_constraints(i < 0x80)

		self.state.memory.store(key_addr, user_input1, endness = proj.arch.memory_endness)
		self.state.memory.store(stack_addr, user_input2)
		self.state.globals['solutions'] = (user_input1, user_input2)

proj.hook_symbol('__isoc99_scanf', replace_scanf())

simgr = proj.factory.simgr(init_state)

def check_puts(state):
	output_addr = state.memory.load(state.regs.esp + 4, 4, endness = proj.arch.memory_endness)
	if not state.solver.symbolic(output_addr):
		return False
	FLAG = output_addr == 0x484F4A47
	copy_state = state.copy()
	copy_state.add_constraints(FLAG)
	if copy_state.satisfiable():
		state.add_constraints(FLAG)
		return True
	return False

def is_success(state):
	puts_addr = 0x8048370
	if state.addr == puts_addr:
		return check_puts(state)
	else:
		return False

simgr.explore(find = is_success)

if simgr.found:
	solution = simgr.found[0]
	user_input1, user_input2 = solution.globals['solutions']
	print (solution.solver.eval(user_input1), solution.solver.eval(user_input2, cast_to=bytes).decode())
else:
	print ("No result")

不是很理解的地方是，为什么要先添加判断这个 constraints 是否满足，然后再添加到 state 中

arbitrary write

思路和上一题比较接近，这次使用了 strncpy 函数的参数作为检查

遇到的一个问题是 BV 数据类型在选择部分数据上的问题

from angr import *
import claripy

proj = Project('./16_angr_arbitrary_write')

start_state = proj.factory.entry_state()

class replace_scanf(SimProcedure):
    def run(self, fmt, key_addr, s_addr):
        user_input1 = claripy.BVS('user_input1', 32)
        user_input2 = claripy.BVS('user_input2', 8 * 20)

        for c in user_input2.chop(bits = 8):
            self.state.add_constraints(c > 0x20)
            self.state.add_constraints(c < 0x7f)
        
        self.state.memory.store(key_addr, user_input1, endness = proj.arch.memory_endness)
        self.state.memory.store(s_addr, user_input2)
        self.state.globals['solutions'] = (user_input1, user_input2)
    
proj.hook_symbol('__isoc99_scanf', replace_scanf())

simgr = proj.factory.simgr(start_state)

def check_strncpy(state):
    dest_addr = state.memory.load(state.regs.esp + 4, 4, endness = proj.arch.memory_endness)
    src_addr = state.memory.load(state.regs.esp + 8, 4, endness = proj.arch.memory_endness)
    length = state.memory.load(state.regs.esp + 12, 4, endness = proj.arch.memory_endness)
    source = state.memory.load(src_addr, length)
    if not state.solver.symbolic(source) or not state.solver.symbolic(dest_addr):
        return False
    target_string = b'NDYNWEUJ'
    target_dest = 0x57584344
    if state.satisfiable(extra_constraints = (target_dest == dest_addr, target_string == source[-1:-64])):
        state.add_constraints(target_dest == dest_addr, target_string == source[-1:-64])
        return True
    return False

def is_successful(state):
    if state.addr == 0x8048410:
        return check_strncpy(state)
    else:
        return False

simgr.explore(find = is_successful)

if simgr.found:
    solution_state = simgr.found[0]
    user_input1, user_input2 = solution_state.globals['solutions']
    print (solution_state.solver.eval(user_input1), solution_state.solver.eval(user_input2, cast_to=bytes).decode())
else:
    print ("No result")
© 2024 s0uthwood's Blog
已运行 0 天    ⌨  86.36k  字    🧠  38  篇文章
Built with Hugo
Theme Stack designed by Jimmy