angr符号执行工具

关于angr
其实angr是我在hgame week4的时候偶然发现滴
//因为那个vm的题目一开始没整出来。。。
//然后随便套了个脚本就跑出来了。。。
不得不说angr是ctf里的一个神器

happyVM

直接上题
hgame 2019 week4的vm题目

可以看到程序主要是根据输入进行encrypt
经过比较后然后判断对错
直接上代码

from angr import *
p = Project("./happyVM",auto_load_libs=False)     # file name
s = p.factory.entry_state()
sm = p.factory.simulation_manager(s)
r = sm.explore(find = 0x400786,avoid = 0x40078D)        # address
print r.found[0].posix.dumps(0)
# hgame{3Z_VM_W0NT_5T0P_UR_PR0GR355}

这是我第一次使用angr，并轻松完成一道题
跑的时间有点久
10分钟左右吧
但是我完全不怎么懂angr，只是套个脚本
包括后续的做题，导致有很多能用angr的题没有整出来，因为一旦这个“万能模板”报错
我就不会使用angr来分析它了//毕竟我完全不了解他，只知道能轻松写题
所以写了下这篇文章想来熟悉一下并能进阶使用angr
//大部分借鉴了今天偶然间看到的一篇国外dalao的blog
//因为写的挺好滴~关于选取入口还有对输入的限制都有讲
具体可点击
下面是作者提供的模板，我自己稍微加了些注释

import angr 

p = angr.Project('prodkey')         #初始化文件

good = (0x400deb)
bad = (0x400df2)

verify_function = 0x00400c99
fget_function = 0x00400e20
main = 0x00400dfc

state = p.factory.blank_state(addr=main) # 入口地址

simgr = p.factory.simulation_manager(state) # 符号执行初始化

simgr.explore(find=good, avoid=bad) # 寻找路径

result = simgr.found[0]

for i in range(3):
    print (result.posix.dumps(i))

这是tamuctf中的题
那题wp在我上一篇blog中，因为z3写不出，求解答案的方式很繁琐
然而这脚本几秒钟就跑出来了
虽然说字符串有些不可打印，但确实是正确答案
作者在后面还提供了关于angr加上限制的方法
主要是用claripy来实现的
angr里面一些约束是用z3来实现，有些用法和z3也很像
看约束代码

import claripy

def AND1(c):    #自定义约束函数
    '''constrain 1: printable'''
    return claripy.And(33 <= c , c <= 126)

length = 29     #限制输入的长度

flag = claripy.BVS('flag', length*8)

for i in range(length):
    state.solver.add( AND1(flag.get_byte(i)) ) 

后面还有
看一下整体的脚本

import angr 
import claripy


def AND1(c):
    '''constrain 1: printable'''
    return claripy.And(33 <= c , c <= 126)

def AND2(c):
    '''returns constraints s.t. c is printable'''
    return claripy.And(65 <= c , c <= 90)

def AND3(c):
    '''returns constraints s.t. c is printable'''
    return claripy.And(97 <= c , c <= 122)

p = angr.Project('prodkey')    

verify_function = 0x00400c99
state = p.factory.blank_state(addr=verify_function)

length = 29
flag = claripy.BVS('flag', length*8)

for i in range(length):
    state.solver.add( AND1(flag.get_byte(i)) )
    # state.solver.add( AND2(flag.get_byte(i)) )
    # state.solver.add( AND3(flag.get_byte(i)) )

my_buf = 0x12345678         #瞎写的地址
state.memory.store(addr=my_buf, data=flag)# 吧约束的字符串放入该地址
state.regs.rdi = my_buf# rdi指向该地址

@p.hook(0x00400ca9) #勾取
def debug_func(state):
    rdi_value = state.regs.rdi 
    print ( 'rdi is point to {}'.format(rdi_value) )
    

simgr = p.factory.simulation_manager(state)

good = (0x00400deb)
bad  = (0x00400df2)

simgr.explore(find=good, avoid=bad)

result = simgr.found[0]

# Always print this 
for i in range(3):
    print (result.posix.dumps(i))

print (result.solver.eval(flag, cast_to=bytes))

这就是解决tamuctf那题的完美解决方式了
答案也都是可打印字符
我本来想用这脚本稍作修改来解决一下hgame那题
但是跑的时间也要6分钟。。。

import angr
import claripy


def AND1(c):
    '''constrain 1: printable'''
    claripy.And(65 <= c, c <= 90)
    claripy.And(95 <= c, c <= 125)
    return claripy.And(48 <= c, c <= 57)


p = angr.Project('happyVM')

mainaddr = 0x0040070E
state = p.factory.blank_state(addr=mainaddr)

length = 34
flag = claripy.BVS('flag', length * 8)

for i in range(length):
    state.solver.add(AND1(flag.get_byte(i)))
    # state.solver.add( AND2(flag.get_byte(i)) )
    # state.solver.add( AND3(flag.get_byte(i)) )


my_buf = 0x12345678
state.memory.store(addr=my_buf, data=flag)
state.regs.rsi = my_buf



@p.hook(0x0040082B)
def debug_func(state):
    rsi_value = state.regs.rsi
    print ('rsi is point to {}'.format(rsi_value))


simgr = p.factory.simulation_manager(state)

good = (0x00400786)
bad = (0x0040078d)

simgr.explore(find=good, avoid=bad)

result = simgr.found[0]

# Always print this
for i in range(3):
    print (result.posix.dumps(i))

print (result.solver.eval(flag, cast_to=bytes))

现在起码了解到怎么使用angr对条件进行约束了
本来想约束输入前6字符为hgame{
但是不知道怎么弄。。。
没办法了，先写这么一点
等到以后遇到题型了再继续总结
包括这里面涉及的hook，我也没怎么了解过
还是太菜了啊