昨天打dasctf，被第一个题暴打了，之后复现的时候感觉可以爆破，尝试一下angr，（虽然不知道行不行）

安装

因为是exe所以在win上安装

1
2
3
4
5
6
7
pip install --upgrade pip
pip install GitPython
pip install pyvex
pip install unicorn
pip install simuvex
pip install angr  
pip install "numpy<1.24.0"

最后的numpy一定要小于这个版本，不然会报错

使用

载入文件

1
2
p = Project('xxx',auto_load_libs = False)
# xxx为文件路径

执行后，视为载入了这个文件，这时才可以分析

数据类型及操作

1
2
bv = state.solver.BVV(0x1234, 32)       # create a 32-bit-wide bitvector with value 0x1234
state.solver.eval(bv)                # convert to python int

位向量和int的转换

1
2
3
4
5
6
7
state.mem[index] #指定一个内存地址
state.mem[0x1000].long = 4 #赋值为long类型的4 可以char, short, int, long, size_t, uint8_t, uint16_t等

state.mem[0x1000].long.resolved #输出为位向量
state.mem[0x1000].long.concrete #输出为int

state.regs.rsi = state.solver.BVV(3,64) #给一个寄存器赋值64位值为3，angr中寄存器的值均为位向量类型

操作寄存器和内存地址

求解器

Simulation Managers用来管理状态，执行模拟和运行。控制一组state的符号执行

1
2
simgr = proj.factory.simulation_manager(state) #创建一个SM
simgr.active #查看SM状态

不加state默认用入口点

1
2
step() # 执行一个基本块
run() #执行到结束

explore

用explore方法来探索路径

方法定义是：

1
2
3
def explore(self, stash='active', n=None, find=None, avoid=None, find_stash='found', avoid_stash='avoid', cfg=None,num_find=1, **kwargs):
# find 表示目标地点
# avoid 表示不能到的地点
1
2
simgr.explore(find=lambda s: b"Congrats" in s.posix.dumps(1))
# 求解所有可以让标准输出输出b"Congrats"的路径
1
2
s = simgr.found[0] #取解
flag = s.posix.dumps(0) #输出内容

求解引擎

state.solver

位向量：比特序列，可以是值或者符号

1
2
3
one = state.solver.BVV(1, 64)
one_hundred = state.solver.BVV(100, 64)
weird_nine = state.solver.BVV(9, 27)
1
2
3
4
>>> weird_nine.zero_extend(64 - 27)
<BV64 0x9>
>>> one + weird_nine.zero_extend(64 - 27)
<BV64 0xa>

S带符号,用extend扩展长度

创建符号变量：

1
2
x = state.solver.BVS("x", 64)
y = state.solver.BVS("y", 64)

可以直接运算得到AST抽象语法树，使用SMT求解器可以转化AST

1
2
3
4
state.solver.add(x > y)
state.solver.add(y > 2)
state.solver.add(10 > x)
state.solver.eval(x)

add用来添加约束，eval用来求解

1
state.satisfiable() #解是否可行

除了朴素的 eval ，angr 提供了多种解析方式 。

接口 描述
solver.eval(expression) 将会解出一个可行解
solver.eval_one(expression) 将会给出一个表达式的可行解，若有多个可行解，则抛出异常
solver.eval_upto(expression, n) 将会给出最多n个可行解，如果不足n个就给出所有的可行解。
solver.eval_exact(expression, n) 将会给出n个可行解，如果解的个数不等于n个，将会抛出异常。
solver.min(expression) 给出最小可行解
solver.max(expression) 给出最大可行解

同时可以设置 extra_constraints 和 cast_to参数对结果进行限制或转换。

angr 系列教程(一）核心概念及模块解读 - 先知社区 (aliyun.com)