转载：All Right
符号执行概述
在学习这个框架之前首先要知道符号执行。
符号执行技术使用符号值代替数字值执行程序，得到的变量的值是由输入变 量的符号值和常量组成的表达式。符号执行技术首先由King在1976年提出 ，经过三十多年的发展，现在仍然被广泛研究，它在软件测试和程序验证中发挥着重 要作用。符号执行是一种重要的形式化方法和静态分析技术，它使用数学和逻辑 首先定义一些基本概念。程序的路径（path）是程序的一个语句序列，这个 语句序列包括程序的一些顺序的代码片段，代码片段之间的连接是由于分支语句 导致的控制转移。一个路径是可行的（feasible），是指存在程序输入变量的至少一组值，如果以这组值作为输入，程序将沿着这条路径执行。否则，路径就是不 可行的（infeasible）。路径条件（path condition,PC）是针对一个路径的，它是一 个关于程序输入变量的符号值的约束，一组输入值使得程序沿着这条路径执行当 且仅当这组输入值满足这条路径的路径条件。具体看这里，链接
angr框架介绍
在二进制代码中寻找并且利用漏洞是一项非常具有挑战性的工作，它的挑战性主要在于人工很难直观的看出二进制代码中的数据结构、控制流信息等。angr是一个基于python的二进制漏洞分析框架，它将以前多种分析技术集成进来，方便后续的安全研究人员的开发。它能够进行动态的符号执行分析（如，KLEE和Mayhem），也能够进行多种静态分析。
当然这款工具在CTF中的运用还是比较火的，在一些国际比赛中经常会看到它所带来的神奇之处，比如下面我们将要讲的的DEFCON CTF Qualifier 2016 baby-re这道题它仅仅用了10min就完成看了自动化分析拿到了flag。angr的github地址为，链接
angr的安装
理论上来说angr目前支持linux、windows、MAC多个平台。但是支持的最好的还是linux平台。Windows平台下由于相关的依赖库文件较难安装，因此不太建议在windows上安装。
接下来我们介绍一下ubuntu上的安装。
- 安装独立python虚拟环境，virtualenvwrapper是一个python的虚拟环境，使用这个的主要原因是angr会对于libz3 or libVEX产生修改，为了防止对已经安装的库的修改而影响到到之后其他程序的使用，使用一个python的虚拟机环境是一个不错的选择。
1sudo apt-get install python-dev libffi-dev build-essential virtualenvwrapper
此时virtualenvwrapper就可以使用了,常用命令如下：
- 列出虚拟环境列表:workon，也可以使用：lsvirtualenv
- 新建虚拟环境:mkvirtualenv [虚拟环境名称]
- 启动/切换虚拟环境:workon [虚拟环境名称]
- 删除虚拟环境:rmvirtualenv [虚拟环境名称]
- 离开虚拟环境:deactivate
- 接着angr安装
|
1
|
pip install angr
|
安装好以后我们启动虚拟环境，进入虚拟的python库后就可以载入angr库了
|
1
2
3
4
5
6
|
longlong@ubuntu:~/examples/defcon2016quals_baby-re_0$ workon angr
(angr) longlong@ubuntu:~/examples/defcon2016quals_baby-re_0$ python
Python 2.7.6 (default, Oct 26 2016, 20:30:19)
[GCC 4.8.4] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> import angr
|
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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
#include <stdio.h>
#include <string.h>
#include <unistd.h>
#include <fcntl.h>
#include <stdlib.h>
char *sneaky = "SOSNEAKY";
int authenticate(char *username, char *password)
{
char stored_pw[9];
stored_pw[8] = 0;
int pwfile;
// evil back d00r
if (strcmp(password, sneaky) == 0) return 1;
pwfile = open(username, O_RDONLY);
read(pwfile, stored_pw, 8);
if (strcmp(password, stored_pw) == 0) return 1;
return 0;
}
int accepted()
{
printf("Welcome to the admin console, trusted user!\n");
}
int rejected()
{
printf("Go away!");
exit(1);
}
int main(int argc, char **argv)
{
char username[9];
char password[9];
int authed;
username[8] = 0;
password[8] = 0;
printf("Username: \n");
read(0, username, 8);
read(0, &authed, 1);
printf("Password: \n");
read(0, password, 8);
read(0, &authed, 1);
authed = authenticate(username, password);
if (authed) accepted();
else rejected();
}
|
这个程序的逻辑很简单，样例程序的功能就是让你输入用户名和密码，然后authenticate函数会进行检验，如果失败就显示Go away，反之就显示认证成功。
接下来我们用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
|
#!/usr/bin/env python
#_*_ coding:utf-8 _*_
import angr
def basic_symbolic_execution():
p = angr.Project('fauxware') #新建一个angr的工程，括号中是目标二进制程序的路径
state = p.factory.entry_state() #接着新建一个SimState的对象
path = p.factory.path(state) #使用factory.path这个容器获取state的起点path对象
pathgroup = p.factory.path_group(path) #根据前面获取的函数入口点的path对象，利用path_group容器获取沿着path开端下面将会执行的path列表
pathgroup.step(until=lambda lpg: len(lpg.active) > 1)#接下来就让pathgroup对象一直执行下去，直到执行到可选择的路径个数大于一个，即产生选择分支的时候，再停止。
#对应在上述的简单程序中authenticate函数的 if (strcmp(password, sneaky) == 0)这个条件判断语句
input_0 = pathgroup.active[0].state.posix.dumps(0) #dump出所有分支的内容，看看哪个答案应该是最可能的
input_1 = pathgroup.active[1].state.posix.dumps(0)
if 'SOSNEAKY' in input_0:
return input_0
else:
return input_1
def test():
pass
if __name__ == '__main__':
print basic_symbolic_execution()
|
结果如下：
|
1
2
3
|
(angr) longlong@ubuntu:~/examples/fauxware$ python solve.py
SOSNEAKY
(angr) longlong@ubuntu:~/examples/fauxware$
|
angr的使用之简单例子二（CTF题）
这道题是DEFCON CTF Qualifier 2016 baby-re0，在打开二进制可执行文件后，我们向下移动到主要的底部，看到0x4028e7有两条非常明显的路径，一条路径是0x402941，打印出错误。另一条是0x4028e9，将会打印出flag。但是这个程序的中间有大量的繁琐的指令，看的人眼花缭乱，接下来我们用angr解决这个问题。
脚本如下：
|
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
#!/usr/bin/env python2
#_*_ coding:UTF-8 _*_
import angr
def main():
proj = angr.Project('./baby-re', load_options={'auto_load_libs': False})
path_group = proj.factory.path_group(threads=4) # 设置了四个线程，对于这个程序线程再多了没意义
# 如果是0x40294b就执行，如果是0x402941就不去执行
path_group.explore(find=0x40294b, avoid=0x402941)
# flag在0x40292c的位置
print path_group.found[0].state.posix.dumps(0)
return path_group.found[0].state.posix.dumps(1) # dumps出flag
if __name__ == '__main__':
print(repr(main()))
|
结果如下：
|
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(angr) longlong@ubuntu:~/examples/defcon2016quals_baby-re_0$ python solve.py
WARNING | 2017-04-09 16:34:11,976 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:34:14,865 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:34:19,274 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:34:26,447 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:34:38,414 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:34:58,141 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:35:24,905 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:36:00,673 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:36:45,998 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:37:48,193 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:39:20,551 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:41:20,080 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
WARNING | 2017-04-09 16:44:18,468 | simuvex.plugins.symbolic_memory | Concretizing symbolic length. Much sad; think about implementing.
+000000077+000000097+000000116+000000104+000000032+000000105+000000115+000000032+000000104+000000097+000000114+000000100+000000033B
'Var[0]: Var[1]: Var[2]: Var[3]: Var[4]: Var[5]: Var[6]: Var[7]: Var[8]: Var[9]: Var[10]: Var[11]: Var[12]: The flag is: Math is hard!\n'
(angr) longlong@ubuntu:~/examples/defcon2016quals_baby-re_0$
|
大概10min后我们得到的flag 是Math is hard!