符号执行的背景

软件中存在缺陷（漏洞）十分常见，一个项目中往往存在着大量的代码。为了查找和修复二进制文件漏洞。其中利用的关键技术都是基于符号执行，可以减少分析二进制文件代码的时间。

符号执行的基本概念

符号执行的概念

符号执行的过程类似于生成代数表达式。符号执行通过尽可能探索程序的执行路径找到潜在的漏洞为止，然后尝试解出利用该漏洞的特定输入。形象的来说就是设方程，然后解出设的未知数。这个未知数就是符号输入。

1
2
3
若x^2+2x+1=0,求其中的x为多少
x^2+2x+1=0对应到符号执行中为探索到特定路径之后引擎生成的表达式
x=-1对应到符号执行中就是利用该漏洞的特定输入

约束的概念，举个例子

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
#include<stdio.h>

int main()
{
	int i=0;
	scanf("%d",&i);
	if(i > 0){
		printf("step one success!");
		if(i>1){
			printf("you win!");
		}
		else{
			printf("still fail");
		}
	}
	else
	{
		printf("fail");
	}
	
	return 0;
}

目标是执行到第8行的“you win!”,所以输入的变量i要大于1。代码中的每一个if分支语句都可称之为一个约束（简单说就是限制），符号执行的每个路径都可以看做是一个表达式，约束求解生成的路径win表达式后得到的答案就是想要的输入。

再举个例子

image-20231105195453682

  • 符号化程序的输入->探索程序的路径->发现指定的特殊路径->根据此路径约束求解->生成输入

  • 符号状态（symbolic state）：符号执行维护一个符号状态，它是一个<变量，符号表达式（symbolic expressions）>的mapping（映射）

  • 符号路径约束（symbolic path constraint）：简单说就是逻辑条件

导致符号执行引擎效率低下的原因–路径爆炸

符号执行可能会导致状态空间的爆炸，深层次的原因是路径爆炸。比如说：符号执行一个动态链接的Linux可执行文件，在引擎探索路径的过程中可能会探索到如libc的动态链接库，因为libc的路径十分复杂，因此会出现路径爆炸，然后把电脑内存挤爆，导致崩溃。

  • 符号执行引擎是通过按行读取的方式模拟执行每条机器码，并更新对应变量，最后再通过约束求解的方式去逆推输入的初值

符号执行工具–angr

angr是现在出名的基于符号执行和模拟执行的二进制框架。

安装

用python虚拟环境安装

1
2
sudo apt-get install python-dev libffi-dev build-essential virtualenvwrapper
mkvirtualenv angr && pip install angr

常用命令

导入angr模块以及加载二进制程序

1
2
import angr
proj = angr.Project('./00_angr_find')

image-20231105210422546

了解导入的二进制程序的基本信息

1
2
3
print(proj.arch)	#架构
print(proj.entry)	#程序入口点
print(proj.filename)#程序名称以及位置

image-20231105211034182

二进制程序在虚拟地址空间的表示

1
2
3
4
5
6
7
8
9
10
11
12
print(proj.loader)#通过CLE模块将二进制对象加载并映射到单个内存空间
print(proj.loader.min_addr)#proj.loader 的低地址
print(proj.loader.max_addr)#proj.loader 的高地址
print(proj.loader.all_objects)#CLE加载的对象的完整列表
print(proj.loader.shared_objects)#这是一个从共享对象名称到对象的字典映射
print(proj.loader.all_elf_objects)#这是从ELF文件中加载的所有对象
print(proj.loader.main_object)#加载main对象
print(proj.loader.execstack)#这个二进制文件是否有可执行堆栈
print(proj.loader.main_object.pic)#这个二进制位置是否独立
print(proj.loader.extern_object)#这是"extern对象",使用它来为未解析的导入和angr内部提供地址
print(proj.loader.kernel_object)#此对象用于为模拟的系统调用提供地址
print(proj.find_object_containing)#获得对给定地址的对象的饮用

image-20231105214320786

Loader 模块主要是负责记录二进制程序的一些基本信息，包括段、符号、链接等。

1
2
obj = proj.loader.main_object#加载main对象
print(obj.plt)#这是plt表

image-20231105214800075

同时也支持一些加载选项

  • auto_load_libs：是否自动加载程序的依赖
  • skip_libs：避免加载的库
  • except_missing_libs：无法解析共享库时是否抛出异常
  • force_load_libs：强制加载的库
  • ld_path：共享库的优先搜索搜寻路径

一般情况下，加载程序都会将auto_load_libs设置为False，这是为了防止连外部库一起加载从而可能会导致路径爆炸。

factory模块

block：用于从给定地址提取基本代码块，angr以基本块为单位分析代码。

1
2
3
4
5
6
7
block = proj.factory.block(proj.entry)#从程序的入口点提取一段代码
print(block)
block.pp()	#打印代码块
print(block.instructions)#该代码块共有多少条指令
print(block.instruction_addrs)#每条指令的地址
print(block.capstone)#capstone风格的反汇编
print(block.vex)

image-20231106002909540

image-20231106002931249

States：proj = angr.Project('./00_angr_find')

这是一个初始化映像，但是要执行符号执行，还需要simstate，表示模拟程序状态的特定对象

1
2
state = proj.factory.entry_state()#即就是simstate，Simstate包含程序的内存，寄存器，文件系统数据...
print(state)

image-20231106003432325

  • blank_state：构造一个“空白板”空白状态，其中大部分数据未初始化。当访问未初始化的数据时，将返回一个不受约束的符号值。
  • entry_state：造一个准备在主二进制文件的入口点执行的状态。
  • full_init_state：构造一个准备好通过任何需要在主二进制文件入口点之前运行的初始化程序执行的状态，例如，共享库构造函数或预初始化程序。完成这些后，它将跳转到入口点。
  • call_state：构造一个准备好执行给定函数的状态

这些构造函数都能够通过参数addr来指定初始时的rip/eip地址，而call_state可以用这种方式来构造传参。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
state = proj.factory.entry_state()#即就是simstate，Simstate包含程序的内存，寄存器，文件系统数据...
# print(state)

s = proj.factory.blank_state()

s.memory.store(0x4000,s.solver.BVV(0x123456789abcdef0123456789abcdef,128))

load_data = s.memory.load(0x4004,6)

print(load_data)

print(state.regs.eip)#获取当前指令指针
print(state.regs.eax)
state.regs.ebp = state.regs.ebp#将寄存器rsp的值给rbp
print(state.regs.ebp)

image-20231106103348875

这些并不是python int型，而是位向量（bitvectors），需要对其置换

1
2
3
4
5
6
7
8
bv = state.solver.BVV(0x1234,32)#创建一个32位宽，值为0x1234的位向量
y = state.solver.BVS("y",64)#创建一个名为"y"的位向量符号，长度为64位

print(bv)
print(y)

int_bv = state.solver.eval(bv)#将bit向量转为python int
print(hex(int_bv))

image-20231106104328005

eval是一种通用方法，可以将任何位向量转换成python原语。

Simulation Managers模拟管理器

1
2
3
4
5
6
simgr = proj.factory.simulation_manager(state)#首先创建将要使用的模拟管理器。构造函数可以接受状态或状态列表。
#多个state可以被组成为stash,可以进行forward(单步),filter(过滤),merge(合并),move(移动)这些操作
print(simgr)
print(simgr.active)#用于存储操作
simgr.step()#执行一个基本块的符号执行，即就是所有状态向前推进一个基本块
print(simgr.active)#更新存储

image-20231106110416617

一些存储的类型：

  • active：此存储区包含默认情况下将逐步执行的状态，除非指定了备用存储区
  • deadended：当一个状态在某些原因下无法被继续执行，则我们会将这个状态放入到deadended stash中，这个原因包括没有有效的指令去执行，所有的约束状态都不可满足，或者是非法的指针
  • pruned：牵扯到了一个LAZY_SOLVES参数，主要是用来加快angr的符号执行速度，但是这个参数要在恰当的情况下使用，否则可能求解出的答案是错误的，因为使用该参数后angr不检查每个状态对约束是否满足。
  • unconstrained：如果save_unconstrained选项被提供给SimulationManager构造函数，则会将“不受约束的状态”放入到这个stash中。
  • unsat：如果向SimulationManager构造函数中传入参数save_unsat，则会将不满足的状态放入到unsat中，比如某两个约束是互相矛盾的（输入必须同时是AAAA和BBBB）

SimProcedure

当符号执行遇到一些函数的时候，为了防止angr将外部库也一并加载分析从而导致效率低下甚至可能是路径爆炸。可以利用hook一些常用函数，从而提高效率。

它支持以下这些外部库：

1
angr.procedures
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
28
29
30
31
32
33
34
35
36
SIM_LIBRARIES
SIM_PROCEDURES
SimProcedures
__builtins__
__cached__
__doc__
__file__
__loader__
__name__
__package__
__path__
__spec__
advapi32
cgc
definitions
glibc
gnulib
java
java_io
java_jni
java_lang
java_util
libc
libstdcpp
linux_kernel
linux_loader
msvcr
ntdll
posix
procedure_dict
stubs
testing
tracer
uclibc
win32
win_user32

以Libc为例，angr支持了一部分libc中的函数：

1
angr.procedures.libc
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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
__builtins__
__cached__
__doc__
__file__
__loader__
__name__
__package__
__path__
__spec__
abort
access
atoi
atol
calloc
closelog
err
error
exit
fclose
feof
fflush
fgetc
fgets
fopen
fprintf
fputc
fputs
fread
free
fscanf
fseek
ftell
fwrite
getchar
getdelim
getegid
geteuid
getgid
gets
getuid
malloc
memcmp
memcpy
memset
openlog
perror
printf
putchar
puts
rand
realloc
rewind
scanf
setbuf
setvbuf
snprintf
sprintf
srand
sscanf
stpcpy
strcat
strchr
strcmp
strcpy
strlen
strncat
strncmp
strncpy
strnlen
strstr
strtol
strtoul
system
time
tmpnam
tolower
toupper
ungetc
vsnprintf
wchar

所以如果程序中调用了这部分函数，默认情况下就会由angr.procedures.libc中实现的函数进行接管。但是其中有一部函数实现的并不完善，需要我们自己编写函数来hook它。

hook

第一种方案是直接对地址进行 hook，通过直接使用 project.hook(addr,function()) 的方法直接钩取。

同时，Angr 对于有符号的二进制程序也运行直接对符号本身进行钩取：project.hook_symbol(name,function) 。