angr 学习笔记

article/2025/11/8 10:36:36

附件,参考1,参考2

符号执行原理

基本概念

即初始参数用变量代替,模拟程序执行过程,维护执行到各个位置时的状态(用各个变量之间的代数关系表示)。

  • 符号状态(Symbolic State)
    当前状态所有参数的集合,用 σ σ σ 表示。集合中的每个元素用表示初始参数的变量表示。
  • 路径约束(Path Constraint)
    到达当前路径需要表示初始参数满足的关系,通常用 PC 表示。

例如下面的程序:

#include <bits/stdc++.h>using namespace std;int main() {int x, y, z;cin >> x >> y;z = 2 * y;if (x == z) {if (x > y + 10) {cout << "Path-1";} else {cout << "Path-2";}} else {cout << "Path-3";}return 0;
}

对应的程序框图如下:
在这里插入图片描述
x s i m x_{sim} xsim y s i m y_{sim} ysim 分别表示初始输入的参数 xy
如果执行到 Path-1 ,则:

  • σ = { x = x s i m , y = y s i m , z = 2 ⋅ y s i m } σ=\{x=x_{sim},y=y_{sim},z=2\cdot y_{sim}\} σ={x=xsim,y=ysim,z=2ysim}
  • PC = ( x s i m = 2 ⋅ y s i m ) ∧ ( x s i m > y s i m + 10 ) \text{PC}=(x_{sim}=2\cdot y_{sim}) \wedge ( x_{sim}>y_{sim}+10) PC=(xsim=2ysim)(xsim>ysim+10)

约束求解

即根据符号执行求得的执行到目标位置时的状态,反推出初始时假设的各个变量的值。

例如上面计算出执行到 Path-1 时的 σ σ σ 和 PC 。如果执行到 Path-1 则应当满足 PC 为真,进一步推出 x s i m = 22 , y s i m = 11 x_{sim} = 22,y_{sim}=11 xsim=22,ysim=11 为一组合法解。

为了进行约数求解,angr 内置了 z3 约束求解器。

动态符号执行

由于 angr 分析基于的是低级语言,会涉及内存、寄存器等结构,如果全部符号化会使得路径约束变得十分复杂且没有必要。因此 angr 采取动态符号执行(Dynamic Symbloic Execution)或者叫做混合执行(Concolic Execution)的方式,即将关键变量符号化,其他变量都赋一个合理的初始值。angr 在默认情况下,只有从标准输入流中读取的数据会被符号化,其他数据都是具有实际值的。

angr 入门

以下面的程序为例,介绍 angr 的基本用法

//gcc example-1.c -o example-1
#include <stdio.h>
#include <stdlib.h>
#include <string.h>void encrypt(char *flag) {for (int i = 0; i < 13; i++) {flag[i] ^= i;flag[i] += 32;}
}// flag{G00dJ0b}
int main() {char flag[100] = {};scanf("%s", flag);if (strlen(flag) != 13) {printf("Wrong length!\n");exit(0);}encrypt(flag);if (!strcmp(flag, "\x86\x8d\x83\x84\x9f\x62\x56\x57\x8c\x63\x5a\x89\x91")) {printf("Right!\n");} else {printf("Wrong!\n");}return 0;
}

加载二进制文件

首先,angr 需要加载二进制文件。

import angr
proj = angr.Project('example-1')

符号执行状态——SimStae

前面介绍的符号执行的时维护的状态在 angr 中对应为 SimStae 类。其中初始状态需要我们来创建。

state = proj.factory.entry_state()

angr 中许多类的都需要通过 factory 获得,factory 是工厂的意思,可以理解为 proj 的 factory 给用户生产了许多类的实例,这里生产的实例是 SimState ,entry_state 函数用来获取程序入口点的状态,也就是初始状态。

state 中维护这内存、寄存器以及文件结构等参数。在初始状态时,我们可以设置其中一些参数,可以是参数也可以是具体数值。

在angr中,无论是具体值还是符号量都有相同的类型——claripy.ast.bv.BV,也就是BitVector的意思,BV后面的数字表示这个比特向量的位数。

  • 创建 32bit 数值 666
    claripy.BVV(666, 32)
    
  • 创建 32bit 变量 sym_var
    claripy.BVS('sym_var', 32)
    

在本题目中,可以设置 stdin 参数。

sym_flag = claripy.BVS('flag', 60 * 8)
state = proj.factory.entry_state(stdin=sym_flag)

符号执行引擎——Simulation Managers

前面提到的符号执行在 angr 中的具体实现为 Simulation Managers 类。

simgr = proj.factory.simgr(state)

angr 符号执行的过程类似于 bfs 的过程。在到达一个条件分枝时,一个状态会分裂出多个状态分别进入各个分枝中。simgr.active 为当前存在的所有状态,simgr.step() 相当于所有状态都向下执行一步。

直接求解

我们可以直接设置需要执行到的目标位置

simgr.explore(find=0x40133D)

由于开了 PIE ,地址随机,angr 默认基址为 0x400000 ,当然也可以指定基址:

proj = angr.Project('example-1', load_options={'main_opts' : {'base_addr' : 0x400000}
})

此时的状态被保存到了 found这 个数组中,可以通过 simgr.found[0] 获取当前的状态,其中 dumps() 的参数 0,1,2 分别表示 stdinstdoutstderr 的内容,直接输出即可,不需要前面设置 stdin 参数为变量。(貌似这个得和前面 simgr.explore 配合使用)

found = simgr.found[0]
print(found.posix.dumps(0))

完整代码:

import angrproj = angr.Project('example-1')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=0x40133D)
found = simgr.found[0]
print(found.posix.dumps(0))
# b'flag{G00dJ0b}\x00\x00\x02Z\x0e\x02\xe4\x00\x19\x08\x89\x00\x00\x01\x00\x00\x1a\x00\x1a\x02\x00<\x02\x00)\x00\x19\x04\x00\x19\x89\x89\x89\x01\x01\x0e\x01*\x8a\x00\x00\x02\x00\x10\x00\x00J'

求解参数

如果是求解前面设的参数,则需要设置求解器

solver = simgr.found[0].solver

之后求解参数

print(solver.eval(sym_flag, cast_to=bytes))

当然,求解器可以添加条件限制
比如在这个地址处添加 eax = 0 的条件限制。
在这里插入图片描述

solver.add(simgr.found[0].regs.eax == 0)

完整代码:

import angr
import claripyproj = angr.Project('example-1')
sym_flag = claripy.BVS('flag', 60 * 8)
state = proj.factory.entry_state(stdin=sym_flag)
simgr = proj.factory.simgr(state)
simgr.explore(find=0x40133B)
solver = simgr.found[0].solver
solver.add(simgr.found[0].regs.eax == 0)
print(solver.eval(sym_flag, cast_to=bytes))
# b'flag{G00dJ0b}\x00\x02\x89\x01J\x01\x8a\x89\x08\x02\x00I\x89\x02\x00\x00*\x01\x00\x01\x01\x01\x00\x01\x02\x02@\x00\x00\x00\x89)\x19\x003\x00\x01J\x01\x01*\x02\x00\x00\x00\x01\x00'

手动模拟

前面 simgr.explore 的过程其实可以手动模拟
思路是每 step 后遍历所有状态,当找位于目标地址的状态后,求解参数即可。
完整代码:

import sys
import angr
import claripyproj = angr.Project('example-1')
sym_flag = claripy.BVS('flag', 60 * 8)
state = proj.factory.entry_state(stdin=sym_flag)
simgr = proj.factory.simgr(state)
while len(simgr.active):for active in simgr.active:if active.addr == 0x40133D:print(active.solver.eval(sym_flag, cast_to=bytes))sys.exit(0)simgr.step()
# b'flag{G00dJ0b}\x00*\x1a-\x08\x02\x02\x00\x00\x0c\x01\x00*\x02))\x00***\x00\x00\x01\x02I\x1b(\x08D\xc1\x01\x01J\x8d\x01\x01\x00\x19\x08\x00K\x01\x00\x00\x01\x00\x00'

angr_explore

_angr_find

主要讲解 explore 函数中 find 的用法,前面已经介绍过了。

直接定位到目标地址。
在这里插入图片描述

import angrproj = angr.Project('_angr_find')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=0x80492F0)
found = simgr.found[0]
print(found.posix.dumps(0))
# b'CYSRBXIA'

_angr_avoid

主函数复杂,ida反编译不出来,直接看判断函数
在这里插入图片描述
可以看到只有同时满足 should_succeed 为真和 s1 = s2 时才正确。
其中 should_succeed 初值为 1 且仅在 avoid_me 函数中被赋为 0 。
在这里插入图片描述
avoid_me 被多次调用
在这里插入图片描述
如果避免执行到 avoid_me 函数,则搜索空间将大大降低。

import angrproj = angr.Project('_angr_avoid')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8049300, avoid=0x80492BB)
found = simgr.found[0]
print(found.posix.dumps(0))
# b'QBQRZMMV'

_angr_find_condition

在这里插入图片描述
代码由许多相似结构组成,最终目标地址有多个。
在这里插入图片描述
explore 函数中的 findavoid 参数可以自定义功能。这里可以通过判断执行到当前位置时 stdout 的内容确定是否为目标地址。

import angrdef is_successful(state):return b'Good Job.' in state.posix.dumps(1)def should_avoid(state):return b'Try again.' in state.posix.dumps(1)proj = angr.Project('_angr_find_condition')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=is_successful, avoid=should_avoid)
print(simgr.found[0].posix.dumps(0))
# b'CNCDLYYH'

当然也参数可以简化为 lambda 表达式

import angrproj = angr.Project('_angr_find_condition')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
# b'CNCDLYYH'

angr_symbolic

前面提到创建 SimStae 类的时候可以设置某些参数为变量或值,这些参数可以是,如寄存器、某块内存甚至是某个文件。

_angr_symbolic_registers

ida 反编译不是很准确,需要分析具体汇编
在这里插入图片描述
首先 get_user_input 函数将输入结果依次放入 eaxebxedx 三个寄存器中。
在这里插入图片描述
紧接着将寄存器中的值分别作为三个函数的参数。
在这里插入图片描述
angr 中除了可以创建函数入口状态 factory.entry_state 外还可以创建空状态 blank_state
指定 blank_state 的地址以及寄存器中的值即可求解。

import angr
import claripyproj = angr.Project('_angr_symbolic_registers')
state = proj.factory.blank_state(addr=0x0804958F)
password0 = claripy.BVS('password0', 32)
password1 = claripy.BVS('password1', 32)
password2 = claripy.BVS('password2', 32)
state.regs.eax = password0
state.regs.ebx = password1
state.regs.edx = password2
simgr = proj.factory.simgr(state)
simgr.explore(find=0x080495EF)
solver = simgr.found[0].solver
print(f'password0: {hex(solver.eval(password0))}')
print(f'password1: {hex(solver.eval(password1))}')
print(f'password2: {hex(solver.eval(password2))}')
# password0: 0x729d64c2
# password1: 0x372c322
# password2: 0x189ff536

当然,直接复用前面 _angr_find_condition 的代码也可以求解。

_angr_symbolic_stack

关键函数:
在这里插入图片描述
通过 blank_state 获取初始状态, ebp 的值是未约束的。在这题中,我们之后要向栈中 push 符号值,并且通过 ebp 索引这些符号值(比如 [ebp+var_C] ),所以我们得让 ebp 有一个正确的初值了。ebp 的值是什么不重要,我们只需要保证它和esp的偏移是正确的即可。
我们将起始地址设在 scanf 函数之后的 0x80493EF 。

state = proj.factory.blank_state(addr=0x80493EF)

mov ebp, esp 开始到起始地址前,看 esp 的变化:
在这里插入图片描述
可以看到,espebp 的关系为 ebp = esp + 0x18 + 4 + 4 + 4 +4 = esp + 40

state.regs.ebp = state.regs.esp + 40

可以看到,complex_function0complex_function1 参数分别存放在 [ebp+var_C][ebp+var_10] 中。
在这里插入图片描述
其中 var_10 = -0x10var_C = -0xC
在这里插入图片描述
在栈上对于位置的值,之后就是正常求解。

state.regs.esp = state.regs.ebp - 0xC + 4
password0 = claripy.BVS('password0', 32)
password1 = claripy.BVS('password1', 32)
state.stack_push(password0)
state.stack_push(password1)
state.regs.esp = state.regs.ebp - 40

完整代码如下:

import angr
import claripyproj = angr.Project('_angr_symbolic_stack')
state = proj.factory.blank_state(addr=0x80493EF)
state.regs.ebp = state.regs.esp + 40
state.regs.esp = state.regs.ebp - 0xC + 4
password0 = claripy.BVS('password0', 32)
password1 = claripy.BVS('password1', 32)
state.stack_push(password0)
state.stack_push(password1)
state.regs.esp = state.regs.ebp - 40
simgr = proj.factory.simgr(state)
simgr.explore(find=0x804943C)
solver = simgr.found[0].solver
print(f'password0: {hex(solver.eval(password0))}')
print(f'password1: {hex(solver.eval(password1))}')
# password0: 0xef03928
# password1: 0x46731955

_angr_symbolic_memory

在这里插入图片描述
这次数据读入的位置是固定的内存地址,因此直接在对应地址处设置变量。

password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
password2 = claripy.BVS('password2', 64)
password3 = claripy.BVS('password3', 64)
state.mem[0xB53A820].uint64_t = password0
state.mem[0xB53A820 + 8].uint64_t = password1
state.mem[0xB53A820 + 16].uint64_t = password2
state.mem[0xB53A820 + 24].uint64_t = password3

如果我们要获取内存中的数据(具体值或者符号值),可以这样用

state.mem[0xA1BA1C0].uint64_t.resolved

完整代码如下:

import angr
import claripyproj = angr.Project('_angr_symbolic_memory')
state = proj.factory.blank_state(addr=0x8049315)
password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
password2 = claripy.BVS('password2', 64)
password3 = claripy.BVS('password3', 64)
state.mem[0xB53A820].uint64_t = password0
state.mem[0xB53A820 + 8].uint64_t = password1
state.mem[0xB53A820 + 16].uint64_t = password2
state.mem[0xB53A820 + 24].uint64_t = password3
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8049381)
solver = simgr.found[0].solver
print(f'password0: {solver.eval(password0, cast_to=bytes)}')
print(f'password1: {solver.eval(password1, cast_to=bytes)}')
print(f'password2: {solver.eval(password2, cast_to=bytes)}')
print(f'password3: {solver.eval(password3, cast_to=bytes)}')
# password0: b'MUPROSTX'
# password1: b'OWBBFEQD'
# password2: b'IHRUZBZU'
# password3: b'PZRKTOZX'

这里会发现直接输入求得的结果并不能通过检验,这是因为端序的问题,程序输入时输入函数自动进行端序的转换使其变为小端序存放在内存中,而内存设置的是端序转换后的结果。
实际输入应为:

XTSORPUM DQEFBBWO UZBZURHI XZOTKRZP

_angr_symbolic_dynamic_memory

在这里插入图片描述
这次采用的是动态分配内存,内存地址不确定。
但是我们可以设置内存指针的值,然后在指针指向的内存区域设置参数求解。
比如我们可以设置内存地址为bss起始位置。
在这里插入图片描述

password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
state.mem[0x804C040].uint64_t = password0
state.mem[0x804C040 + 8].uint64_t = password1

之后设置两个指针 buffer0buffer1 指向对应内存。

state.mem[0xA3FA020].uint32_t = 0x804C040
state.mem[0xA3FA028].uint32_t = 0x804C040 + 8

之后就是常规的求解过程。
完整代码如下:

import angr
import claripyproj = angr.Project('_angr_symbolic_dynamic_memory')
state = proj.factory.blank_state(addr=0x804938C)
password0 = claripy.BVS('password0', 64)
password1 = claripy.BVS('password1', 64)
state.mem[0x804C040].uint64_t = password0
state.mem[0x804C040 + 8].uint64_t = password1
state.mem[0xA3FA020].uint32_t = 0x804C040
state.mem[0xA3FA028].uint32_t = 0x804C040 + 8
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8049452)
solver = simgr.found[0].solver
print(f'password0: {solver.eval(password0, cast_to=bytes)}')
print(f'password1: {solver.eval(password1, cast_to=bytes)}')
# password0: b'KWVBCKPX'
# password1: b'GSBFNQGX'

_angr_symbolic_file

主函数逻辑如下:
在这里插入图片描述
先向 buffer 中读入数据,然后执行 ignore_me 函数后再从 XTQAFOST.txt 中读入数据到 buffer

ignore_me 函数的关键部分如下:
在这里插入图片描述
可见之后再次读入到 buffer 中的数据还是输入数据。

因此我们可以直接对文件的内容进行符号化。
要对文件内容进行符号化,首先我们要创建一个模拟的文件 SimFile ,文件名为 XTQAFOST.txt ,内容为 8 字节的符号值,大小为 0x40 字节:

password0 = claripy.BVS('password0', 0x40)
sim_file = angr.SimFile(name='XTQAFOST.txt', content=password0, size=0x40)

后插入到 state 的文件系统(FileSystem)中,state 的文件系统可以通过 state.fs 获得:

state.fs.insert('XTQAFOST.txt', sim_file)

之后就是常规求解了。

完整代码如下:

import angr
import claripyproj = angr.Project('_angr_symbolic_file')
state = proj.factory.blank_state(addr=0x8049564)
password0 = claripy.BVS('password0', 0x40)
sim_file = angr.SimFile(name='XTQAFOST.txt', content=password0, size=0x40)
state.fs.insert('XTQAFOST.txt', sim_file)
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8049635)
solver = simgr.found[0].solver
print(f'password0: {solver.eval(password0, cast_to=bytes)}')
# password0: b'XLCQLBYI'

angr_constraints

angr在符号执行的过程中,会将路径约束保存在SimState内置的约束求解器内。但是存在一些特殊的情况,使得状态数迅速增长导致 angr 无法求解。这种现象称为路径爆炸。下面举一个利用 constraints 手动添加限制解决路径爆炸的例子:
主程序十分简单。
在这里插入图片描述
然而直接求解是求不出来的,问题出在 check_equals_XCKPBIWXXTQAFOST 函数上:
在这里插入图片描述
由于这里进行了 16 次 if 判断,每次判断时一个状态会分裂出两个状态,因此经过这个函数状态数膨胀了 2 16 2^{16} 216 倍,直接导致 angr 路径爆炸。
解决这个路径爆炸的方法十分简单。因为这个函数本质上是一个比较函数,因此可以在这个函数调用之前加一条限制就可以完美解决了。

simgr.explore(find=0x80493A4)
found = simgr.found[0]
found.add_constraints(found.memory.load(buffer_addr, 16) == b'XCKPBIWXXTQAFOST')

完整代码如下:

import angr
import claripyproj = angr.Project('_angr_constraints')
state = proj.factory.blank_state(addr=0x804935D)
password = claripy.BVS('password', 16 * 8)
buffer_addr = 0x804C040
state.memory.store(buffer_addr, password)
simgr = proj.factory.simgr(state)
simgr.explore(find=0x80493A4)
found = simgr.found[0]
found.add_constraints(found.memory.load(buffer_addr, 16) == b'XCKPBIWXXTQAFOST')
print(found.solver.eval(password, cast_to=bytes))
# b'IOXDQYNPQNLWCMRT'

angr_hooks

angr hooks 即将程序中的的函数用自己实现或 angr 自带的函数替代,这种方法可以解决路径爆炸问题。

_angr_hooks

可以看出,程序分两次输入和加密,因此前面直接添加条件限制的方式不太适合。
在这里插入图片描述
考虑将 check_equals_XCKPBIWXXTQAFOST hook。
在这里插入图片描述

@proj.hook(addr=0x80493CE, length=5)
def my_check_equals(state):buffer_addr = 0x804C044buffer = state.memory.load(buffer_addr, 16)state.regs.eax = claripy.If(buffer == b'XCKPBIWXXTQAFOST', claripy.BVV(1, 32), claripy.BVV(0, 32))

这一部分可以写作如下形式:

def my_check_equals(state):buffer_addr = 0x804C044buffer = state.memory.load(buffer_addr, 16)state.regs.eax = claripy.If(buffer == b'XYMKBKUHNIQYNQXE', claripy.BVV(1, 32), claripy.BVV(0, 32))proj.hook(addr=0x80493CE, hook=my_check_equals, length=5)

length = 5 指的是指令地址跳过 5 字节。这里 hook 是将地址替换,而 call 指令本身为 E8 E5 EE FF FF 占 5 字节,需要跳过。
经过 hook 后就可以正常求解了。

import angr
import claripyproj = angr.Project('_angr_hooks')# @proj.hook(addr=0x80493CE, length=5)
# def my_check_equals(state):
#     buffer_addr = 0x804C044
#     buffer = state.memory.load(buffer_addr, 16)
#     state.regs.eax = claripy.If(buffer == b'XCKPBIWXXTQAFOST', claripy.BVV(1, 32), claripy.BVV(0, 32))def my_check_equals(state):buffer_addr = 0x804C044buffer = state.memory.load(buffer_addr, 16)state.regs.eax = claripy.If(buffer == b'XYMKBKUHNIQYNQXE', claripy.BVV(1, 32), claripy.BVV(0, 32))proj.hook(addr=0x80493CE, hook=my_check_equals, length=5)
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
# b'ZXIDRXEORJOTFFJNWYDFOSDBYRLSUABZ'

_angr_simprocedures

前面的 hook 只是替换调用函数时的函数地址,但是当一个函数被多次调用的时候就需要 hook 函数本身。

如下图所示,程序结果十分复杂。
在这里插入图片描述
并且造成路径爆炸的 check_equals_XCKPBIWXXTQAFOST 函数被多次调用。
在这里插入图片描述
考虑 hook check_equals_XCKPBIWXXTQAFOST 函数本身。angr 对函数本身进行 hook 的方法为 SimProcedures ,定义一个 SimProcedures 的代码如下:

class MyCheckEquals(angr.SimProcedure):def run(self, buffer_addr, length):buffer = self.state.memory.load(buffer_addr, length)return claripy.If(buffer == b'XCKPBIWXXTQAFOST', claripy.BVV(1, 32), claripy.BVV(0, 32))

SimProcedure 中的 run 函数由子类实现,其接收的参数与 C 语言中的参数保持一致,返回为对应原函数的返回值。
定义好了 SimProcedure 之后,我们需要调用 hook_symbol 函数对程序中名为 check_equals_XCKPBIWXXTQAFOST 的函数进行 hook :

proj.hook_symbol(symbol_name='check_equals_XCKPBIWXXTQAFOST', simproc=MyCheckEquals())

完整代码如下:

import angr
import claripyclass MyCheckEquals(angr.SimProcedure):def run(self, buffer_addr, length):buffer = self.state.memory.load(buffer_addr, length)return claripy.If(buffer == b'XCKPBIWXXTQAFOST', claripy.BVV(1, 32), claripy.BVV(0, 32))proj = angr.Project('_angr_simprocedures')
proj.hook_symbol(symbol_name='check_equals_XCKPBIWXXTQAFOST', simproc=MyCheckEquals())
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
# b'VDOWLVMQTSSFNZGK'

angr_veritesting

Veritesting 意为路径归并,出自2014年的一篇论文 Enhancing Symbolic Execution with Veritesting ,是一种解决路径爆炸的方法。
如下图,主程序中引起路径爆炸的不是单独的函数,且加密过程在循环中,前面防止路径爆炸的方法失效。
在这里插入图片描述
设置参数 veritesting=True 即可。

import angrproj = angr.Project('angr_veritesting')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state, veritesting=True)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
# b'AFKPUZEJOTYDINSXCHMRWBGLQVAFKPUZ'

这种写法与上面的写法是等价的:

simgr = proj.factory.simgr(state)
simgr.use_technique(angr.exploration_techniques.Veritesting())

另外根据官方的说法:

Note that it frequenly doesn’t play nice with other techniques due to the invasive way it implements static symbolic execution.

Versitesting 通常与其他 exploration techniques 不兼容。

angr_library

_angr_static_binary

如果程序采用静态编译,则 angr 直接求解会使得符号执行陷入库函数的代码中导致求解时间过长,这就需要前面介绍的 _angr_simprocedures 的函数 hook 技术,而库函数 angr 有提前写好的 SimProcedures ,直接用即可。

import angrproj = angr.Project('_angr_static_binary')
proj.hook_symbol('printf', angr.SIM_PROCEDURES['libc']['printf']())
proj.hook_symbol('__isoc99_scanf', angr.SIM_PROCEDURES['libc']['scanf']())
proj.hook_symbol('strcmp', angr.SIM_PROCEDURES['libc']['strcmp']())
proj.hook_symbol('puts', angr.SIM_PROCEDURES['libc']['puts']())
proj.hook_symbol('__libc_start_main', angr.SIM_PROCEDURES['glibc']['__libc_start_main']())
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))
# b'XROIJFIY'

_angr_shared_library

利用 angr 对动态链接库中单个的函数进行符号执行。

关键函数为 validate
在这里插入图片描述
该函数位于动态链接库中
在这里插入图片描述
在对应的动态链接库中找到对应的函数
在这里插入图片描述
通过 call_state 创建调用函数的状态:

state = proj.factory.call_state(validate_addr, claripy.BVV(password_addr, 32), length)

这里要注意的是,函数 validate 的参数为 password 的指针,而不是字符串本身。
因此需要在内存中选择某区域存放 password 的变量。

password = claripy.BVS('password', 8 * 8)
password_addr = 0x4024
state.memory.store(password_addr, password)

完整代码如下:

import angr
import claripyproj = angr.Project('_angr_shared_library.so')
validate_addr = 0x40129C
password = claripy.BVS('password', 8 * 8)
password_addr = 0x4024
length = claripy.BVV(8, 32)
state = proj.factory.call_state(validate_addr, claripy.BVV(password_addr, 32), length)
state.memory.store(0x4024, password)
simgr = proj.factory.simgr(state)
simgr.explore(find=0x401348)
found = simgr.found[0]
found.solver.add(found.regs.eax != 0)
print(found.solver.eval(password, cast_to=bytes))
# XNGWTLKW

angr_overflow

_angr_arbitrary_read

简单的栈溢出漏洞,v4 可以溢出覆盖 s 为 Good Job. 地址。
在这里插入图片描述
直接求解不行,因为 puts 的输出内容的由 v4 溢出覆盖的地址确定,而 angr 事先不知道 Good Job. 的地址,导致无法求解。

import angrproj = angr.Project('15_angr_arbitrary_read')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=lambda state: b'Good Job.' in state.posix.dumps(1),avoid=lambda state: b'Try again.' in state.posix.dumps(1)
)
print(simgr.found[0].posix.dumps(0))

这里可以把条件改为判断 puts 的参数是否为 Good Job. 的地址。
可以先符号执行到这里
在这里插入图片描述
然后判断 eax 是否为 Good Job. 的地址。

import angrproj = angr.Project('_angr_arbitrary_read')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=0x8049259)
found = simgr.found[0]
found.add_constraints(found.regs.eax == 0x58434B4F)
print(simgr.found[0].posix.dumps(0))
# b'0004074803 \xd9\xd9Y\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9OKCX'

当然,这个过程可以自动判断:

def check_puts(state):puts_parameter = state.memory.load(state.regs.esp + 4, 4, endness=proj.arch.memory_endness)if state.solver.symbolic(puts_parameter):good_job_string_address = 0x58434B4Fis_vulnerable_expression = puts_parameter == good_job_string_addresscopied_state = state.copy()copied_state.add_constraints(is_vulnerable_expression)if copied_state.satisfiable():state.add_constraints(is_vulnerable_expression)return Truereturn Falsedef is_successful(state):puts_address = 0x08049090if state.addr == puts_address:return check_puts(state)return Falsesimgr.explore(find=is_successful)

完整代码如下:

import angrdef check_puts(state):puts_parameter = state.memory.load(state.regs.esp + 4, 4, endness=proj.arch.memory_endness)if state.solver.symbolic(puts_parameter):good_job_string_address = 0x58434B4Fis_vulnerable_expression = puts_parameter == good_job_string_addresscopied_state = state.copy()copied_state.add_constraints(is_vulnerable_expression)if copied_state.satisfiable():state.add_constraints(is_vulnerable_expression)return Truereturn Falsedef is_successful(state):puts_address = 0x08049090if state.addr == puts_address:return check_puts(state)return Falseproj = angr.Project('_angr_arbitrary_read')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=is_successful)
print(simgr.found[0].posix.dumps(0))
# b'0004074803 \xd9\xd9\x99\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9\xd9OKCX'

_angr_arbitrary_write

这次是覆盖 *dest 指针指向 password_buffer 然后向其中写入 BIWXXTQA
在这里插入图片描述
和上道题思路一样,这次检查 strncpy 的参数。

import angr
import claripydef check_strncpy(state):dest = state.memory.load(state.regs.esp + 4, 4, endness=proj.arch.memory_endness)src = state.memory.load(state.regs.esp + 8, 4, endness=proj.arch.memory_endness)src_content = state.memory.load(src, 8)if state.solver.symbolic(src_content) and state.solver.symbolic(dest):if state.satisfiable(extra_constraints=[claripy.And(src_content == b'BIWXXTQA', dest == 0x58434B40)]):state.add_constraints(claripy.And(src_content == b'BIWXXTQA', dest == 0x58434B40))return Truereturn Falsedef is_successful(state):strncpy_address = 0x80490F0if state.addr == strncpy_address:return check_strncpy(state)return Falseproj = angr.Project('_angr_arbitrary_write')
state = proj.factory.entry_state()
simgr = proj.factory.simgr(state)
simgr.explore(find=is_successful)
print(simgr.found[0].posix.dumps(0))
# b'0061440360 BIWXXTQA\xd9\xd9\xd9\xd9\xd9\xd8\xd9\xd9@KCX'

_angr_arbitrary_jump

栈溢出
在这里插入图片描述
目标是让程序执行到这里
在这里插入图片描述
当一个指令有很多分支的可能性时,称之为不受约束(unconstrained)的状态, 比如说当用户的输入决定下一条指令的位置。angr 在遇到不受约束的状态时会将其抛出,本题将要关闭这个默认行为,转而利用此状态去求解能够跳转到 print_good 函数的payload。

import angr
import claripyproj = angr.Project('_angr_arbitrary_jump')
payload = claripy.BVS('payload', 64 * 8)
state = proj.factory.entry_state(stdin=payload)
simgr = proj.factory.simgr(state,save_unconstrained=True,stashes={'active': [state],'unconstrained': [],'found': [],})
while (len(simgr.active) or len(simgr.unconstrained)) and not len(simgr.found):for unconstrained in simgr.unconstrained:eip = unconstrained.regs.eipprint_good_addr = 0x58434B58if unconstrained.satisfiable(extra_constraints=[eip == print_good_addr]):unconstrained.add_constraints(eip == print_good_addr)simgr.move('unconstrained', 'found')breaksimgr.drop(stash="unconstrained")simgr.step()
print(simgr.found[0].posix.dumps(0))
# b'\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xd2\xdaXKCX\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\xda\x00\x00\x00\x00\x00'

http://chatgpt.dhexx.cn/article/8E0C13JZ.shtml

相关文章

利用angr获取CFG

静态二进制分析中&#xff0c;对于程序控制流图CFG的计算是很基础且重要的一步&#xff0c;很多的分析是要建立在CFG的基础上。angr作为二进制分析工具&#xff0c;当然提供了CFG功能&#xff0c;下面我们就来探索下要如何使用angr计算CFG&#xff0c;以及其中的坑。 angr中的…

Angr 内存符号化 05_angr_symbolic_memory

说明 通过查看下面的源码或IDA汇编&#xff0c;可知此例需要输入4个输入字符串&#xff0c;给每个输入字符串赋值给了user_input数组这块已经开辟的内存空间&#xff0c;我们可以监测user_input在内存中的值来获取最终的答案。 随机生成的源码 #include <stdio.h> #in…

Angr学习笔记

Angr学习笔记 前言 本文记录一下Angr的基本使用方法&#xff0c;主要是基于Github上的开源项目以及笔记AngrCTF_FITM整理&#xff0c;Angr在逆向方面确实用处比较大&#xff0c;特此记录一下。 什么是Angr angr是一个用于分析二进制文件的python框架。它专注于静态和符号分…

angr纠错和易错点

现在环境已经没有问题了。我运行了几个代码&#xff08;使用python3&#xff09;&#xff0c;都会出现不同的问题。 运行报错 解决方法&#xff1a; 添加b 运行报错&#xff1a; 解决方法&#xff1a; 删掉cast_to; 因为python2中str就是字节流 python3中不一样&#xff0c…

git本地分支管理

文章目录 一、master分支没有改变&#xff0c;合并其他分支二、master分支有改变&#xff0c;合并其他分支 作为开发人员&#xff0c;我们应该尽可能多地建立分支&#xff0c;在分支上进行开发&#xff0c;功能测试稳定后&#xff0c;再将分支上地代码合并到指定的分支 git bra…

Git 分支管理

Git 分支管理 一、主分支Master 首先&#xff0c;代码库应该有一个、且仅有一个主分支。所有提供给用户使用的正式版本&#xff0c;都在这个主分支上发布。 Git主分支的名字&#xff0c;默认叫做Master。它是自动建立的&#xff0c;版本库初始化以后&#xff0c;默认就是在主分…

git分支管理策略

git分支管理策略 1 总览 git 的分支整体预览图如下&#xff1a; 从上图可以看到主要包含下面几个分支&#xff1a; master&#xff1a;git默认主分支&#xff08;这里不作操作&#xff09;。 stable&#xff1a;稳定分支&#xff0c;替代master&#xff0c;主要用来版本发布。…

IDEA中使用Git功能和IDEA中的Git分支管理

IDEA中使用Git功能 IDEA中创建Git仓库 1、设置Git程序的路径 2、设置编译器的GitHub账号 3、新建项目 4、发布项目到GitHub IDEA向Git提交修改后的代码 1、实现git add 2、开始commit 3、实现git commit -m 4、实现git push origin master 项目成员使用IDEA的Git功…

【Git-10】Eclipse中Git分支管理

分支管理&#xff0c;是 Git 开发中的一个非常有效的团队开发策略。多个程序员并行开发&#xff0c;每个程序员可以定义各自的分支&#xff0c;在自己的分支上开发工程。再开发结束测试完毕后&#xff0c;再合并到主干工程中&#xff0c;一次性提交到远程。由其他程序员使用。 …

Git 分支管理最佳实践

Git 是目前最流行的源代码管理工具。大量的软件项目由 GitHub、Bitbucket 和 GitLab 这样的云服务平台或是私有的 Git 仓库来管理。在使用 Git 时通常会遇到的一个问题是采用何种分支管理实践&#xff0c;即如何管理仓库中作用不同的各类分支。和软件开发中的其他实践一样&…

Git分支管理办法,每个团队不一样,仅供参考!

原创不易&#xff0c;转载注明出处&#xff0c;喜欢就点个赞吧&#xff01; 网上有很多文章&#xff0c;很少有实际具体的流程图说明&#xff0c;我根据我们团队的情况&#xff0c;画了几张简图&#xff0c;仅供参考。 每个公司的代码管理方式都不一样 主要有两种 1.TrunkB…

Git分支管理与常用命令

一、分支管理 Git在创建分支仅是生成了一个指针又称快照&#xff08;有的工具则进行了物理拷贝&#xff09;&#xff0c;这样在使用起来就非常的方便。方便的同时问题随之而来&#xff0c;如果不加管理&#xff0c;那么就会到处开枝散叶&#xff0c;完全看不出主干。因此&…

复杂项目的版本管理及git分支管理建议

在复杂项目中&#xff0c;特别是多团队的快速迭代中&#xff0c;版本管理与分支管理&#xff0c;总是我们难以回避的问题&#xff0c;这里分享一下我们在团队中使用的规范&#xff0c;以及对应的每一步的步骤。 为什么需要GIT使用建议 团队开发中&#xff0c;遵循一个合理、清…

2022新版Git教程 从入门到实战(三)Git分支管理

&#x1f41f; 个人主页 &#xff1a;https://blog.csdn.net/qq_52007481⭐个人社区&#xff1a;【小鱼干爱编程】&#x1f4f0;最近专栏&#xff1a;Git教程专栏 文章目录 分支工作的工作流程Git分支管理分支的好处 前期准备查看分支分支创建分支转换在新分支中添加记录切换回…

Git 分支管理最佳实践(转载)

前言 Git 是目前最流行的源代码管理工具。大量的软件项目由 GitHub、Bitbucket 和 GitLab 这样的云服务平台或是私有的 Git 仓库来管理。在使用 Git 时通常会遇到的一个问题是采用何种分支管理实践&#xff0c;即如何管理仓库中作用不同的各类分支。和软件开发中的其他实践一样…

Git 分支管理策略汇总

原文链接&#xff1a; Git 分支管理策略 最近&#xff0c;团队新入职了一些小伙伴&#xff0c;在开发过程中&#xff0c;他们问我 Git 分支是如何管理的&#xff0c;以及应该怎么提交代码&#xff1f; 我大概说了一些规则&#xff0c;但仔细想来&#xff0c;好像也并没有形成…

Git分支管理

四、分支管理 分支的存在&#xff0c;极大的强化了不同开发者的协作管理&#xff0c;在一个功能的开发过程中&#xff0c;可以在一个单独的分支上完成&#xff0c;这样不影响主分支的开发&#xff0c;待功能完成后再将分支的内容合并到主分支。 每次提交到分支&#xff0c;Gi…

git的分支管理

这篇文章主要想讲一下git下的分支管理&#xff0c;因为分支管理是你在日常工作中必不可少的一项操作&#xff0c;觉得自己之前了解的不是很多&#xff0c;这次便决定利用一些细碎的时间好好去再次学习巩固一下&#xff0c;初衷也是为了加深自己的理解&#xff0c;便写下此文&am…

【Git】“分支” 如何管理和使用?这一篇就够了~

目录 一、什么是分支&#xff1f; 二、分支的操作 2.1、查看分支 2.2、创建分支 2.3、切换分支 和 修改分支 2.4、合并分支 2.4.1、正常合并 2.4.2、合并冲突 三、创建分支和切换分支的底层原理 一、什么是分支&#xff1f; 在版本控制中&#xff0c;我们可以针对每个任…

管理Git的分支

目录 一、本地分支&#xff08;local branches&#xff09;管理 1.1 查看和建立分支&#xff08; git branch&#xff09; 1.2 分支中提交的浏览与比较&#xff08;git log&#xff09; 1.3 切换当前分支&#xff08;git switch&#xff09;与合并分支&#xff08;git mer…