符号执行-angr

发表于 | 阅读次数:

angr基本使用

根据官网教程安装非常非常非常麻烦…

照着这篇做安装教程

例1 r100

先试着做一个例题 r100

流程很简单，就是一个玩具

1

就是要执行到0x400844，不能到0x400855

直接跑脚本，写的时候有几个奇奇怪怪的小问题

import angr 和 from angr import * 不是一回事…

用后者一直报找不到angr

还有就是proj的auto_load_libs，甚至文件名的单引号双引号都能让我这里跑不出结果…也是醉了

2

例2 ais3-cm

3

这个程序有一个命令行参数输入

先给出解题代码

4

其中BVS应该是创建一个bit向量，这里选择50*8个bit，也就是50字符

然后就是注意添加命令行参数的格式了

最后输出时用cast_to=str可以以ASCII形式输出

safari刷新网站，cmd+r

例3 hash

题目给了源码

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
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

int main(int argc, char *argv[]) {
	if (argc != 4) {
		printf("what?\n");
		exit(1);
	}

	unsigned int first = atoi(argv[1]);
	if (first != 0xcafe) {
		printf("you are wrong, sorry.\n");
		exit(2);
	}

	unsigned int second = atoi(argv[2]);
	if (second % 5 == 3 || second % 17 != 8) {
		printf("ha, you won't get it!\n");
		exit(3);
	}

	if (strcmp("h4cky0u", argv[3])) {
		printf("so close, dude!\n");
		exit(4);
	}

	printf("Brr wrrr grr\n");

	unsigned int hash = first * 31337 + (second % 17) * 11 + strlen(argv[3]) - 1615810207;

	printf("Get your key: ");
	printf("%x\n", hash);
	return 0;
}

简单编译一下，脚本比较好写

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

proj = angr.Project('./hash',auto_load_libs = False)
argv1 = claripy.BVS('argv1',10*8)
argv2 = claripy.BVS('argv2',10*8)
argv3 = claripy.BVS('argv3',10*8)

state = proj.factory.entry_state(args=["./hash",argv1,argv2,argv3])

simgr = proj.factory.simgr(state)

simgr.explore(find=0x4007f8)
print simgr.found[0].solver.eval(argv1,cast_to=str)
print simgr.found[0].solver.eval(argv2,cast_to=str)
print simgr.found[0].solver.eval(argv3,cast_to=str)

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

值得注意的是，最后程序执行到了目标地址，我们需要获得程序的输出

也就是代码中的最后一行 dumps(1)，应该就是stdout的意思

最后输出Get your key: c0ffee