Ash blog
0%

angr学习笔记

发表于 更新于

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)

这一步用来创建符号执行路径的管理器,用于探索并管理不同的执行路径状态.

1
sim.explore(find=)

运行,探索满足路径需要的值.通过找到某个地址的状态或者满足某个条件的状态,去除掉不能满足这个条件的状态,通过使用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():
    # angr项目对象创建
    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”的位置,我们无法确定在哪里.

image-20230919164515979

这种情况下需要找到正确的那条路径,可以对符号执行路径的标准输出判断下,可以对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-符号化寄存器

image-20230920094655614

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

image-20230920144000606

在创建符号执行的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-符号化栈上的值

image-20230920150517297

这一题与上面类似,不过将值存入了栈中,所以需要符号化栈中的值,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))

后面的一些题与之相似,符号化内存相关.就不展开了.