angr符号执行用例解析——0ctf_momo_3

45 阅读 0 评论 30 点赞

我是靠谱客的博主结实钢铁侠，最近开发中收集的这篇文章主要介绍angr符号执行用例解析——0ctf_momo_3，觉得挺不错的，现在分享给大家，希望可以做个参考。

概述

源码及二进制文件链接：https://github.com/angr/angr-doc/tree/master/examples/0ctf_momo_3

该题目来自于2016年0ctf比赛的被混淆过的二进制文件。在使用angr进行分析前，作者通过调试工具确定了flag的生成方式。flag获取代码为：.text:0804ABAC mov edx, dword_81FE260[edx*4]。随后，我们对输入进行了变换，并寻找与Qira的不同点。我们发现0x81fe6e0和0x81fe6e4内容一样时即可。因为movfuscator混淆后 “vm”访问内存总是一样的，所以我们可以通过寻找相同指令（相同顺序）来确定angr执行的目标。

程序首先将momo文件加载进来；
然后计算了要分析的起始地址和大小；
通过loader.memory.read_bytes方法将要分析的数据读取出来；
使用capstone框架对这段数据反汇编；
初始化一个capstoneblock；
在这段block中通过指令的字符串与顺序匹配来寻找分析的目标地址targets；
指令的顺序为：
edx, dword ptr [edx*4 + 0x81fe260]
al, byte ptr [0x81fe6e0]
dl, byte ptr [0x81fe6e4]
发现一个记录一个targets；
打印出发现的targets地址数目；
对于每一个target进行分析，分析内容如下：
初始化一个flag_arr=“0ctf{”
然后从string工具类中取出一个char，与刚刚的flag_arr拼接得到flag；
获取程序入口状态entry_state；
entry_state的输入为flag；
从这个状态起explore，寻找所有包含target地址的路径（按照顺序来说，找到一个就返回了，所以满足的路径应该只有一个）；
以这个路径第一个状态为起始，执行到target，比较寄存器ax和dx的值，如果相等则说明这个trychar是对的，则在flag_arr后面添加这个字符；
直到所有的target都遍历完成，就得到了正确的flag。

个人总结：
这个程序分析的过程仅利用了angr中反汇编，寄存器访问，路径探索explore过滤，模拟执行successors等功能。没有用到符号执行，与约束求解器。而且抓取flag的思路实在是暴力，相当于依次暴力破解每个字符，找到满足要求的字符后，再去遍历下一位。
分析起来是真的慢。

#!/usr/bin/env python
# This is a movfuscated binary from 0ctf 2016, debugging we can see
# that every byte from the flag gets moved this way:
# .text:0804ABAC
mov
edx, dword_81FE260[edx*4]
# after, varying a few times the input and looking for differences
# with Qira we can see that it is expected for the content of
# 0x81fe6e0 and 0x81fe6e4 to be the same
# since the way the movfuscator "vm" access memory is always the same
# we can search for the same instructions (in the same order) to
# establish the targets for angr execution
import sys
import string
import angr
from angr.block import CapstoneInsn, CapstoneBlock
ins_char = 0x81fe6e0
flag_char = 0x81fe6e4
after_fgets = 0x08049653
mov_congrats = 0x0805356E
def main():
p = angr.Project('./momo', load_options={'auto_load_libs': False}) #load the binary files
addr = after_fgets
size = mov_congrats - after_fgets
# let's disasm with capstone to search targets
insn_bytes = ''.join(
p.loader.memory.read_bytes(addr, size))
insns = []
for cs_insn in p.arch.capstone.disasm(insn_bytes, addr):
insns.append(CapstoneInsn(cs_insn))
block = CapstoneBlock(addr, insns, 0, p.arch)
targets = []
# let's keep track of the state
state = 0
for ins in block.insns:
if state == 0:
if ins.op_str == 'edx, dword ptr [edx*4 + 0x81fe260]':
state += 1
continue
if state == 1:
if ins.op_str == 'al, byte ptr [0x81fe6e0]':
state += 1
continue
if state == 2:
if ins.op_str == 'dl, byte ptr [0x81fe6e4]':
targets.append(ins.address + ins.size) #targets are addrs
state = 0
print "found {:d} targets".format(len(targets))
assert len(targets) == 28
flag_arr = ['0', 'c', 't', 'f', '{']
for target in targets[5:]:
print "nexamining target {:#x}:".format(target)
for trychar in string.printable:
print trychar,
sys.stdout.flush()
flag = ''.join(flag_arr)+trychar
state = p.factory.entry_state()
state.posix.files[0].content.store(0, flag + "n") #have no idea about posix.files
e = p.surveyors.Explorer(start=state, find=(target,))#find target states from entry state
e.run()
assert len(e.found) == 1
np = e.found[0] #find the first state with target
while(True):
nb_size = target - np.addr
if nb_size <= 0:
break
np = p.factory.successors(np, size=nb_size).flat_successors[0]
assert nb_size == 0
al = np.regs.eax[7:0]
dl = np.regs.edx[7:0]
al_val = al._model_concrete.value
dl_val = dl._model_concrete.value
if al_val == dl_val:
flag_arr.append(trychar)
break
return ''.join(flag_arr)
def test():
assert main() == '0ctf{m0V_I5_tUr1N9_c0P1Et3!}'
if __name__ == '__main__':
print main()