记录一下入门Reverse中符号执行的利用

Angr

官方文档：http://angr.io/api-doc/angr.html

简介

Angr是一个利用python开发的二进制程序分析框架，我们可以利用这个工具尝试对一些CTF题目进行符号执行来找到正确的解答，即flag。当然，要注意的是符号执行的路径选择问题到现在依旧是一个很大的问题，换句话说也就是当我们的程序存在循环时，因为符号执行会尽量遍历所有的路径，所以每次循环之后会形成至少两个分支，当循环的次数足够多时，就会造成路径爆炸，整个机器的内存会被耗尽。

安装

ubuntu安装教程如下

1
2
3
4
5
6
7
8
9
# 安装依赖
sudo apt-get install python3-dev libffi-dev build-essential virtualenvwrapper
# 在/etc/profile中加入以下代码并进行source
export WORKON_HOME=$HOME/Python-workhome
source /usr/share/virtualenvwrapper/virtualenvwrapper.sh
# 安装angr
mkvirtualenv --python=$(which python3) angr && pip install angr
# 运行angr
workon angr

符号执行

基础实例

1
2
3
4
5
6
7
8
9
10
import angr

def main():
    p = angr.Project("r100", auto_load_libs=True)
    simgr = p.factory.simulation_manager(p.factory.full_init_state())
    simgr.explore(find=0x400844, avoid=0x400855)
    return simgr.found[0].posix.dumps(0).strip(b'\0\n')

if __name__ == '__main__':
    print(main())

加载依赖库

auto_load_libs用来设置是否自动载入依赖的库，如果设置为True会自动载入依赖的库，然后分析到库函数调用时也会进入库函数，这样会增加分析的工作量。如果为False，程序调用函数时，会直接返回一个不受约束的符号值

设置SimState

SimState表示程序的状态，包括它的内存、寄存器等等

SimState对象通常有三种：

  1. blank_state(**kwargs)
    返回一个未初始化的state，此时需要主动设置入口地址，以及自己想要设置的参数
  2. entry_state(**kwargs)
    返回程序入口地址的state，通常来说都会使用该状态
  3. full_init_state(**kwargs)
    和entry_state(**kwargs)类似，但是调用在执行到达入口点之前应该调用每个初始化函数

我们可以通过 state.regs 和 state.mem 访问寄存器和内存信息。

1
2
3
state.regs.rip
state.regs.rax
state.mem[proj.entry].int.resolved

创建Simulation Managers

p.factory.simulation_manager创建一个simulation_manager进行模拟执行，其中传入一个SimState

SimulationManager一共有三种运行方式：

  1. step()
    每次向前运行一个基本块，并返回进行分类
  2. run()
    运行完所有的基本块，然后会出现deadended的状态，此时我们通常访问最后一个状态来获取我们所需要的信息
  3. explore()
    根据find和avoid进行基本块的执行，最后会返回found和avoid状态

获取执行结果

simgr.found存储了所有符合条件的分支

help命令

可以使用help命令查看某个函数的详细说明，比如help(state)

clarioy

官方文档：http://angr.io/api-doc/claripy.html

claripy是一个符号求解引擎，和z3类似，通常用来构造输入，单位为bit

使用claripy.BVS()创建位向量符号

1
claripy.BVS("u", 8)

使用claripy.BVV()创建位向量值

1
claripy.BVV(0xab, 0x2 * 8)

CTF

这个地址是官方关于在CTF利用Angr的详细教程

这个地址是官方给出的在CTF比赛中使用Angr的例子，都是些精髓

此外还有@Badrer师傅在先知也写了很多相关的文章，大家可以学习一下

下面是一些我碰到的一些CTF例子，会不断地进行更新

funnyre

题目源于【WUSTCTF2020】

去花指令

直接用IDA打开，尝试反编译main函数发现有花指令，根据上下文逻辑nop掉图中红框部分，一共有4处

image-20210319172652670

把data强制分析为code，再把修改过的code声明为function，之后就可以正常的反汇编了

main()函数中确定了flag的长度和格式，还有一长串的异或运算

image-20210319211423984

最后与unk_4025C0的数据进行比对

image-20210319211739539

符号执行

到这里就可以有三种解决方法，第一种是直接爆破，时间会很长；第二种是把所有代码逆回去，会很麻烦；第三种，也是最简单的一种，就是使用Angr来进行符号执行约束求解

下面给出符号执行的代码

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
import angr
import claripy

# 创建project
p = angr.Project("./attachment", load_options={"auto_load_libs": False})
# 设置程序入口,此处必须是flag加载完的位置
state = p.factory.entry_state(addr=0x400601)
# 创建符号向量
flag = claripy.BVS("flag", 8*32)
# 按照程序逻辑flag存放在rdx的第6位,因为前5位是'flag{'
state.memory.store(state.regs.rdx + 5, flag)
'''
# 也可以自己手动修改rdx的位置，但是相对位置不变就行
state.memory.store(0x603056+0x300 + 5, flag)
state.regs.rdx = 0x603056+0x300
'''
# 创建Simulation Manager
sm = p.factory.simulation_manager(state)
print("[+] init ok")

# 设置探索成功的地址
sm.explore(find=0x401DAE)
if sm.found:
    print("[+] found!")
    #输出flag结果
    x = sm.found[0].solver.eval(flag, cast_to=bytes).strip(b'\0')
    print(x)

very_success

题目来源于【flareon2015_2】

符号执行

程序主要代码如下，把用户输入存储到byte_402159中，其中用户输入为37位，sub_401084()对用户输入进行加密，最后与系统的a1比较，相同则成功，其中a1可以通过动态调试得到

所以我们可以把符号执行的初始地址地位在sub_401084()的开始

image-20210322002451961

选取好了初始地址之后，我们需要给参数进行赋值，这里涉及到对内存进行操控

第1个参数来源于0x401064，即函数的返回地址

image-20210322013920422

第2个参数来源于0x4010e4，得追溯到父函数

image-20210322012614011

第3个参数来源于0x402159，直接是一个静态地址

image-20210322001900137

第4个参数就是输入字符串的长度，直接赋一个大于等于37的数值即可

所以最终脚本如下

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
import angr
import claripy

p = angr.Project("./very_success", load_options={"auto_load_libs": False})
s = p.factory.entry_state(addr=0x401084)

# 填入函数的参数
s.mem[s.regs.esp:].dword = 0x401064
s.mem[s.regs.esp+4:].dword = 0x4010E4
s.mem[s.regs.esp+8:].dword = 0x402159
s.mem[s.regs.esp+12:].dword = 37

# 在第三个参数创建一个符号向量
s.memory.store(0x402159, claripy.BVS("flag", 8*37))

sm = p.factory.simulation_manager(s)
print("[+] init ok")

sm.explore(find=0x40106B, avoid=0x401072)
if sm.found:
    print("[+] found!")
    x = sm.found[0].solver.eval(flag, cast_to=bytes).strip(b'\0')
    print(x)

参考

WUST-CTF 2020 官方 Writeup

先知社区-Badrer

angr 系列教程(一）核心概念及模块解读