前言
时间真的不多咯。这次来看看如何编写简单高效的angr脚本,如何进行设置约束条件。
题目五unbreakable
题目链接
我先贴上自己写的粗糙的脚本:
# -*-coding:utf-8-*-
from angr import *
import logging,claripy,archinfo
logging.getLogger('angr.manager').setLevel(logging.DEBUG)
START_ADDR = 0x4005bd
AVOID_ADDR = 0x400850
FIND_ADDR = 0x40083E
INPUT_LENGTH = 0xf2 - 0xc0 + 1
def main():
p = Project("unbreakable-enterprise-product-activation",auto_load_libs=False)
arg1=claripy.BVS("arg1",0x43*8)
args=[p.filename,arg1]
print('adding BitVectors and constraints')
# state = p.factory.entry_state(addr=START_ADDR, add_options={options.LAZY_SOLVES})
state = p.factory.entry_state(args=args,add_options={options.LAZY_SOLVES})
state.libc.buf_symbolic_bytes=0x43 + 1
for byte in arg1.chop(8):
state.add_constraints(byte != '\x00') # null
state.add_constraints(byte >= ' ') # '\x20'
state.add_constraints(byte <= '~') # '\x7e'
sm = p.factory.simulation_manager(state,threads=4)
res=sm.explore(find=FIND_ADDR, avoid=AVOID_ADDR)
print res
for pp in res.found:
print pp.posix.dumps(1)[:pp.posix.dumps(1).find("\x00")]
p=pp.solver.eval(arg1,cast_to=str)
print p[:pp.solver.eval(arg1,cast_to=str).find("}")]
if __name__ == '__main__':
main()
这么跑下来速度还行,不算慢,但是写得还不够好。
我在网上找到一个比较好的文档可以参考一下。
进行条件约束
我们使用了如下代码,设置了agrs参数,可以看出来flag长度为0x43,如果不对条件进行约束那么会导致无用的路径产生。
arg1=claripy.BVS("arg1",0x43*8)
我们需要对其进行约束。
类似如下代码vec
state.solver.And(vec >= ord(' '), vec <= ord('~'))
for byte in arg1.chop(8):
state.add_constraints(byte != '\x00') # null
state.add_constraints(byte >= ' ') # '\x20'
state.add_constraints(byte <= '~') # '\x7e'
这都是对输入进行约束。
这里要注意有一个选项。lazy_solves
,如果不加这个条件运行很慢,而且最终会报错。
使用angr存在explosion的问题也就是路径爆炸,会导致出错。这时候需要我们进行合理的条件约束才行。
github给出了更好的代码实现,摘抄如下;
import angr
START_ADDR = 0x4005bd # first part of program that does computation
AVOID_ADDR = 0x400850 # address of function that prints wrong
FIND_ADDR = 0x400830 # address of function that prints correct
INPUT_ADDR = 0x6042c0 # location in memory of user input
INPUT_LENGTH = 0xf2 - 0xc0 + 1 # derived from the first and last character
# reference in data
def extract_memory(state):
"""Convience method that returns the flag input memory."""
return state.solver.eval(state.memory.load(INPUT_ADDR, INPUT_LENGTH), cast_to=str)
def char(state, n):
"""Returns a symbolic BitVector and contrains it to printable chars for a given state."""
vec = state.solver.BVS('c{}'.format(n), 8, explicit_name=True)
return vec, state.solver.And(vec >= ord(' '), vec <= ord('~'))
def main():
p = angr.Project('unbreakable')
print('adding BitVectors and constraints')
state = p.factory.blank_state(addr=START_ADDR, add_options={angr.options.LAZY_SOLVES})
for i in range(INPUT_LENGTH):
c, cond = char(state, i)
# the first command line argument is copied to INPUT_ADDR in memory
# so we store the BitVectors for angr to manipulate
state.memory.store(INPUT_ADDR + i, c)
state.add_constraints(cond)
print('creating path and explorer')
ex = p.surveyors.Explorer(start=state, find=(FIND_ADDR,), avoid=(AVOID_ADDR,))
print('running explorer')
ex.run()
flag = extract_memory(ex._f) # ex._f is equiv. to ex.found[0]
print('found flag: {}'.format(flag))
return flag
def test():
assert main() == 'CTF{0The1Quick2Brown3Fox4Jumped5Over6The7Lazy8Fox9}'
if __name__ == '__main__':
main()
总结
条件约束感觉还是有点难的,首先要掌握如何编写约束条件,然后还要注意该如何去更好的约束。