angr学习笔记
1.angr介绍
angr是一个用于静态和动态二进制分析的开源工具,用于逆向,病毒分析,漏洞研究等领域.
符号执行是一种很强大的技术,它可以通过分析工具将输入变量符号化探索程序的不同执行路径,而不仅仅是用具体的输入值.符号可以不断变化,最终探索到正确的路径,通过执行路径推导出约束条件,寻找到可能的输入解,发现潜在的漏洞和问题.
angr可以通过符号执行,自动化地探索程序的路径,找到输入值和执行路径上的约束条件.
它提供了python的api用于符号执行和执行一些分析任务.
它内部通过使用z3,一个高性能的约束求解器,自动请求条件,找到满足条件的输入值或程序状态.
关于angr的路径爆炸问题
在符号执行中,程序的执行路径数量可能会迅速的增长,将内存占满,导致崩溃.这种情况可以使用一段代码为例.
以下代码将循环里面嵌套了一个if判断,在符号执行引擎执行时,每次循环判断时都会导致状态分裂,进行分支,导致路径无限的增长.
还会导致路径爆炸的代码结构还有递归调用.以及更复杂的递归循环判断等等.
1 2 3 4 5
| while(true){ if(x==y){ break; } }
|
2.angr使用
1
| project = angr.Project('path', auto_load_libs=False)
|
创建Project,加载二进制文件.auto_load_libs设置不分析引入的第三方库.
在载入二进制文件后,就可以访问文件的一些属性了.
1
| state = project.factory.entry_state()
|
这一步用来建立符号执行的起始状态,标志是分析的开始.从这个起始状态建立符号执行路径,相当于一个快照,保存者运行状态的上下文信息.
1
| sim = project.factory.simgr(state)
|
这一步用来创建符号执行路径的管理器,用于探索并管理不同的执行路径状态.
运行,探索满足路径需要的值.通过找到某个地址的状态或者满足某个条件的状态,去除掉不能满足这个条件的状态,通过使用explore方法,程序将会持续运行,直至寻找到与判断条件相匹配的状态.当满足条件时,会停止执行,并将结果放置sim.found.
3.angr练习
我使用了angr_ctf进行练习,它是一些针对angr出的ctf题,非常适合用来学习.
00_angr_find
第一题只要找到成功的基本块的位置就可以了.sol.posix.dumps(0)表示标准输入内容
1 2 3 4 5 6 7 8 9 10 11 12 13 14
| def angr_find(): project = angr.Project('./AngrCTF_FITM/00_angr_find/00_angr_find', auto_load_libs=False) state = project.factory.entry_state() sim = project.factory.simgr(state) sim.explore(find=0x8048678) if sim.found: sol = sim.found[0] print(sol) print('flag: ', sol.posix.dumps(0))
|
1 2
| <SimState @ 0x8048678> flag: b'JXWVXRKX'
|
01_angr_avoid-忽略指定位置
解的位置是080485DD.按照上面的方法,一直没有计算出结果.因为在其中构造了大量的无效路径avoid_me函数,导致出现了路径爆炸,这种情况下直接忽略掉这些路径即可.
1 2 3 4 5 6 7 8 9
| def angr_avoid(): project = angr.Project('./AngrCTF_FITM/01_angr_avoid/01_angr_avoid', auto_load_libs=False) state = project.factory.entry_state() sim = project.factory.simgr(state) sim.explore(find=0x080485DD, avoid=0x080485A8) if sim.found: sol = sim.found[0] print(sol) print('flag: ', sol.posix.dumps(0))
|
1 2
| <SimState @ 0x80485dd> flag: b'HUJOZMYS'
|
02_angr_find_condition-正确条件查找
在这个程序中,存在这大量输出”Good Job”的位置,我们无法确定在哪里.

这种情况下需要找到正确的那条路径,可以对符号执行路径的标准输出判断下,可以对find指定一个函数.sol.posix.dumps(1)表示标准输出内容,寻找到标准输出中包含’Good Job’内容的路径.
1 2 3 4 5 6 7 8 9 10 11 12
| def angr_find_condition(): def check(state): return b'Good Job' in state.posix.dumps(1)
project = angr.Project('./AngrCTF_FITM/02_angr_find_condition/02_angr_find_condition', auto_load_libs=False) state = project.factory.entry_state() sim = project.factory.simgr(state) sim.explore(find=check) if sim.found: sol = sim.found[0] print(sol) print('flag: ', sol.posix.dumps(0))
|
1 2
| <SimState @ 0x8049017> flag: b'HETOBRCU'
|
03_angr_symbolic_registers-符号化寄存器

这题是因为angr对于格式化的字符串处理有些问题,这里额字符串直接传递到了寄存器中,我们要对寄存器符号化.跳过get_user_input函数.eax,ebx,edx分别是3个字符串,进行不同的验证.

在创建符号执行的state时,不是只有entry_state.还有其他的构造函数,如下
.entry_state()
:构造从函数入口点执行的状态
.blank_state
:构造空状态,此状态,大多数数据是未初始化的,使用未初始化数据时,一个不受约束的符号值会被返回
.call_state
:构造执行某个函数的状态
.full_init_state
:构造一个已经执行过所有需要执行的初始化函数,并准备从函数入口点执行的状态.比如一些库的构造函数.
看起来挺抽象的.需要结合实践理解下.
在本题中,将在一个特定地址建立一个新状态,也就是执行完get_user_input之后.所以要使用blank_state,跳过get_user_input
关于寄存器的符号化
需要用到符号位向量bitvector,符号位向量时angr用于将符号的值注入程序的数据类型.这些值是angr约束请求的自变量, 可以理解为方式的x.
1 2 3 4
| str_size_in_bits = 32 str0 = claripy.BVS('passwd0', str_size_in_bits) str1 = claripy.BVS('passwd1', str_size_in_bits) str2 = claripy.BVS('passwd2', str_size_in_bits)
|
访问寄存器可以使用state.regs
完整代码如下
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
| def angr_symbolic_registers(): def check(state): return b'Good Job' in state.posix.dumps(1)
project = angr.Project('./AngrCTF_FITM/03_angr_symbolic_registers/03_angr_symbolic_registers', auto_load_libs=False) state = project.factory.blank_state(addr=0x08048980) str_size_in_bits = 32 str0 = claripy.BVS('str0', str_size_in_bits) str1 = claripy.BVS('str1', str_size_in_bits) str2 = claripy.BVS('str2', str_size_in_bits) state.regs.eax = str0 state.regs.ebx = str1 state.regs.edx = str2
sim = project.factory.simgr(state) sim.explore(find=check) if sim.found: sol_state = sim.found[0] sol0 = sol_state.solver.eval(str0) sol1 = sol_state.solver.eval(str1) sol2 = sol_state.solver.eval(str2) print(hex(sol0)) print(hex(sol1)) print(hex(sol2))
|
1 2 3
| 0xb9ffd04e 0xccf63fe8 0x8fd4d959
|
04_angr_symbolic_stack-符号化栈上的值

这一题与上面类似,不过将值存入了栈中,所以需要符号化栈中的值,ebp-10和ebp-c.
scanf进行了外平栈,我们将符号执行的位置放在0x8048697开始,此时栈中以及被压入了2个4字节的数据,所以想要符号化栈中的这两个数据,我们先要将栈抬高,也就是esp-8,然后再将两个符号化的栈值压入栈.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
| def angr_symbolic_stack(): def check(state): return b'Good Job' in state.posix.dumps(1)
project = angr.Project('./AngrCTF_FITM/04_angr_symbolic_stack/04_angr_symbolic_stack', auto_load_libs=False) state = project.factory.blank_state(addr=0x08048697) state.regs.ebp = state.regs.esp str_size_in_bits = 32 str0 = claripy.BVS('str0', str_size_in_bits) str1 = claripy.BVS('str1', str_size_in_bits) state.regs.esp -= 0x8 state.stack_push(str0) state.stack_push(str1) sim = project.factory.simgr(state) sim.explore(find=check) if sim.found: sol_state = sim.found[0] sol0 = sol_state.solver.eval(str0) sol1 = sol_state.solver.eval(str1) print(hex(sol0)) print(hex(sol1))
|
后面的一些题与之相似,符号化内存相关.就不展开了.