逆向小工具

Posted by nop on 2019-09-29
Words 1.2k In Total

拿到binary时的步骤:

  • file
  • strings
  • ltrace/strace
  • gdb/OD
  • IDA

angr

符号执行

符号执行 (Symbolic Execution)是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时,该程序会使用符号值作为输入,而非一般执行程序时使用的具体值。在达到目标代码时,分析器可以得到相应的路径约束,然后通过约束求解器来得到可以触发目标代码的具体值。
符号模拟技术(symbolic simulation)则把类似的思想用于硬件分析。符号计算(Symbolic computation)则用于数学表达式分析。

angr简介

angr是一个多架构的二进制分析平台,具备对二进制文件的动态符号执行能力和多种静态分析能力。
angr的简要过程:

  • 将二进制程序载入angr分析系统
  • 将二进制程序转换成中间件语言(intermediate representation, IR)
  • 将IR语言转换成语义较强的表达形式,比如,这个程序做了什么,而不是它是什么。
  • 执行进一步的分析,比如,完整的或者部分的静态分析(依赖关系分析,程序分块)、程序空间的符号执行探索(挖掘溢出漏洞)、一些对于上面方式的结合。
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
# 不需要命令行参数的情况

import angr # 导入angr库

proj = angr.Project('./binary',auto_load_libs=False) # 参数auto_load_libs设置是否载入动态连接库
state = proj.factory.entry_state() # 读取入口点的状态
simgr = proj.factory.simgr(state) # 载入状态

simgr.explore(find=0xaaaa,avoid=0xbbbb) # 查找路径,find参数表示要达到目的正确路径,avoid参数表示要避免的路径
# example Out: <SimulationManager with 2 active, 1 found, 12 avoid>

simgr.found[0].posix.dumps(0) # 得到的结果是列表,只有一个结果时即第一个元素:found[0]


# 需要命令行参数的情况

import angr
import claripy # angr中的一个求解器引擎

proj = angr.Project('./binary',auto_load_libs=False)
argv1 = claripy.BVS('argv1',50*8) # BVS为字节对象,其中第一个参数为参数名,第二个参数为字符个数(一般每8bit为一个英文字符,这里设置50个字符长度)整个语句用于生成程序的参数(符号集)

state = proj.factory.entry_state(args=['./binary',arvg1]) # 读取程序入口点状态,并传入构造好的参数(符号集)

simgr = proj.factory.simgr(state)

simgr.explore(find=0xaaaa,avoid=0xbbbb)
# example Out: <SimulationManager with 3 active, 1 found, 46 avoid>

print simgr.found[0].solver.eval(argv1) # 得到的结果为bit类型,利用sovler.eval转化为ascii码对应的十六进制数

print simgr.found[0].solver.eval(argv1,cast_to=str) # 通过设置参数cast_to使结果变为字符串

z3

Z3 is a theorem prover from Microsoft Research
Z3 is a Satisfaiability Modulo Thories(SMT) solver

z3 Types

  • BitVec:指特定大小的数据类型
    • BitVec(“x”,32)对应c语言中的int
    • BitVec(“x”,8)对应c语言中的char
  • Int(整型)
  • Real(实数)
  • Bool(布尔值)
  • Array
  • ……

Tips

  • z3中没有signed/unsigned类型
  • 使用<,<=,>=,/,/%,>>操作signed类型变量
  • 使用ULT,ULE,UGT,UGE,UDIV,Uremand,LShR操作unsigned类型变量
  • 将BitVec的大小设成运算过程中最大的

模板

1
2
3
4
5
6
7
8
9
10
11
12
from z3 import *
inputs = [BitVec('inputs_%d'%i,8)for i in range(32)] # char inputs[32]

s = Solver()
s.add(...)
if s.check()!=sat: # check检查是否有解,有解时返回结果sat
print 'unsat' # check检查无解时返回结果unsat
else:
m = s.modle()
print m
print repr("".join([chr(m[inputs[i]].as_long()) for i in range(32)]))
# repr方法用于返回一个string格式

例子:

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
// Soup Meat Tea (SMT) (TM)
//
// We welcome you to our delicious kitchen featuring many dishes from all
// around the world. With so many choices we really don't know the perfect
// combination. Fortunately our previous chef left the best set of dishes for
// a table of 8 people. Can you reconstruct the set of dishes?
//
// The service provided by our last chef can be found at.. find the ip/port
// as if it's a stego001 challenge :-)
//
// Compile with: gcc -std=c99 soup_meat_tea.c -o soup_meat_tea
// Test with: echo -n $'... payload ...'|./soup_meat_tea

#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>
#include <unistd.h>

uint32_t state = 42;

typedef enum {
D_SOUP_CHICKEN,
D_SOUP_MEAT,
D_SOUP_NAZI,
D_CHICKEN_RAW,
D_CHICKEN_BLACK,
D_MEAT_BLACKANGUS,
D_MEAT_WAGYU,
D_MEAT_HORSE,
D_TIRAMISU,
D_ICE_BANANA,
D_ICE_STRAWBERRY,
D_OVERFLOW,
} dish_t;

const char *dishes[] = {
"soup-chicken", "soup-meat", "soup-nazi", "chicken-raw", "chicken-black",
"meat-blackangus", "meat-wagyu", "meat-horse", "tiramisu", "ice-banana",
"ice-strawberry",
};

void dish(uint8_t d)
{
state = ((state + d) * 3294782) ^ 3159238819;
}

int main()
{
uint8_t input[32];
read(0, input, 32);

for (uint32_t idx = 0; idx < 32; idx++) {
dish(input[idx]);
}

printf("That's some delicious.. ");
for (uint32_t idx = 0; idx < 32; idx++) {
if(input[idx] < D_OVERFLOW) {
printf("%s ", dishes[input[idx]]);
}
else {
printf("%s ", "<YUEATTHIS>");
}
}

if(state == 0xde11c105) {
system("/bin/cat flag.txt");
}
return 0;
}

z3求解:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
from z3 import *

state = 42
def dish(d):
global state
state = ((state + d) * 3294782) ^ 3159238819
inputs = [BitVec('inputs_%d'%i,8) for i in range(32)]
for idx in range(32):
dish(inputs[idx])
s = Solver()
for i in range(32):
s.add(inputs[i]>=0,inputs[i]<=0xff>)
s.add(state == 0xde11c105)
if s.check() == sat:
m = s.model()
print m
print repr("".join([chr(m[inputs[i]].as_long()) for i in range(32)]))

You are welcome to share this blog, so that more people can participate in it. If the images used in the blog infringe your copyright, please contact the author to delete them.