0x00 题目分析

没啥好说的,就是VM,不过这个VM用的不是汇编,而是加减乘除,相当于整了个计算器出来

0x01 解

无壳,两个附件,一个二进制的data和一个dll

直接上IDA

分成了两部分,一个是key,一个是flag

不过看得出来就算key输错了也是能继续输flag的

先看看key

由main函数可以知道,key有16位,而且全是数字(48<ASCII<57),然后两两一组丢进v11里面去了,sub_1400011E5里面有个scanf,应该是用于格式转换的

比较重要的就是sub_1400012D5了,返回值给了v9然后用v9进行判断

一直进去可以看到很经典的vm格式

直接写解释器吧

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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
def vm(opcode, eip):
if opcode[eip] == 192:
exit()
code = {
160: [f"mov key[{opcode[eip+1]}],{opcode[eip+2]}", 3],
161: [f"mov key[{opcode[eip+1]}],key[{opcode[eip+2]}]", 3],
162: [f"add key[{opcode[eip+1]}],{opcode[eip+2]}", 3],
163: [f"add key[{opcode[eip+1]}],key[{opcode[eip+2]}]", 3],
164: [f"sub key[{opcode[eip+1]}],{opcode[eip+2]}", 3],
165: [f"sub key[{opcode[eip+1]}],key[{opcode[eip+2]}]", 3],
166: [f"mul key[{opcode[eip+1]}],{opcode[eip+2]}", 3],
167: [f"mul key[{opcode[eip+1]}],key[{opcode[eip+2]}]", 3],
176: [f"cmp key[{opcode[eip+1]}],{opcode[eip+2]}", 3],
177: [f"cmp key[{opcode[eip+1]}],key[{opcode[eip+2]}", 3],
178: [f"check cmp == 1", 1],

}
print(opcode[eip], '\t', code[opcode[eip]][0])
eip += code[opcode[eip]][1]
return eip


v9 = [192]*94
v9[0] = 162
v9[1] = 0
v9[2] = 132
v9[3] = 163
v9[4] = 8
v9[5] = 0
v9[6] = 163
v9[7] = 8
v9[8] = 1
v9[9] = 176
v9[10] = 8
v9[11] = 316
v9[12] = 178
v9[13] = 163
v9[14] = 9
v9[15] = 1
v9[16] = 163
v9[17] = 9
v9[18] = 2
v9[19] = 163
v9[20] = 9
v9[21] = 3
v9[22] = 176
v9[23] = 9
v9[24] = 158
v9[25] = 178
v9[26] = 166
v9[27] = 4
v9[28] = 22
v9[29] = 163
v9[30] = 0
v9[31] = 4
v9[32] = 176
v9[33] = 0
v9[34] = 889
v9[35] = 178
v9[36] = 164
v9[37] = 5
v9[38] = 11
v9[39] = 161
v9[40] = 8
v9[41] = 5
v9[42] = 163
v9[43] = 8
v9[44] = 6
v9[45] = 176
v9[46] = 8
v9[47] = 38
v9[48] = 178
v9[49] = 163
v9[50] = 7
v9[51] = 6
v9[52] = 176
v9[53] = 7
v9[54] = 96
v9[55] = 178
v9[56] = 161
v9[57] = 9
v9[58] = 1
v9[59] = 163
v9[60] = 9
v9[61] = 2
v9[62] = 165
v9[63] = 9
v9[64] = 5
v9[65] = 176
v9[66] = 9
v9[67] = 111
v9[68] = 178
v9[69] = 166
v9[70] = 5
v9[71] = 7
v9[72] = 161
v9[73] = 8
v9[74] = 0
v9[75] = 165
v9[76] = 8
v9[77] = 6
v9[78] = 163
v9[79] = 8
v9[80] = 5
v9[81] = 176
v9[82] = 8
v9[83] = 859
v9[84] = 178
v9[85] = 163
v9[86] = 3
v9[87] = 4
v9[88] = 176
v9[89] = 3
v9[90] = 706
v9[91] = 178
v9[92] = 192
r = 0
while 1:
r = vm(v9, r)
if r >= len(v9):
break

解出来这个

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
"""
key[9] == 0
key[8] == 0
162 add key[0],132
163 add key[8],key[0]
163 add key[8],key[1]
176 cmp key[8],316
178 check cmp == 1 (key[0]+132)+key[1] == 316; key[0] = (key[0]+132)
163 add key[9],key[1]
163 add key[9],key[2]
163 add key[9],key[3]
176 cmp key[9],158
178 check cmp == 1 key[3]+key[2]+key[1] == 158
166 mul key[4],22
163 add key[0],key[4]
176 cmp key[0],889
178 check cmp == 1 ((key[0]+132) + (key[4]*22)) == 889; key[0] = ((key[0]+132) + (key[4]*22)); key[4] = (key[4]*22)
164 sub key[5],11
161 mov key[8],key[5]
163 add key[8],key[6]
176 cmp key[8],38
178 check cmp == 1 (key[5] - 11) + key[6] == 38; key[5] = (key[5] - 11)
163 add key[7],key[6]
176 cmp key[7],96
178 check cmp == 1 key[7] + key[6] == 96; key[7] = (key[7] + key[6])
161 mov key[9],key[1]
163 add key[9],key[2]
165 sub key[9],key[5]
176 cmp key[9],111
178 check cmp == 1 key[1] + key[2] - (key[5] - 11) == 111
166 mul key[5],7
161 mov key[8],key[0]
165 sub key[8],key[6]
163 add key[8],key[5]
176 cmp key[8],859
178 check cmp == 1 ((key[0]+132) + (key[4]*22)) - key[6] + (key[5] - 11)*7 ==859
163 add key[3],key[4]
176 cmp key[3],706
178 check cmp == 1 key[3] + (key[4]*22) == 706
"""

需要注意的是比如add key[0],132这种,是会改变key[0]的,后面再调用key[0]要用变化后的,否则会出错

解出这个之后可以发现有很多个方程组,直接上Z3

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

s = Solver()
key = [BitVec(('x%s' % i), 16) for i in range(8)]
#('x%s' % i)是命名格式,意思为xi,i为1~8,16是位数,一组两个字节,即2×8=16bits
out = []
s.add((key[0]+132)+key[1] == 316)
s.add(key[3]+key[2]+key[1] == 158)
s.add(((key[0]+132) + (key[4]*22)) == 889)
s.add((key[5] - 11) + key[6] == 38)
s.add(key[7] + key[6] == 96)
s.add(key[1] + key[2] - (key[5] - 11) == 111)
s.add(((key[0]+132) + (key[4]*22)) - key[6] + (key[5] - 11)*7 == 859)
s.add(key[3] + (key[4]*22) == 706)
if s.check() == sat:
result = s.model()
print(result)
for i in range(8):
out.append(result[key[i]].as_long())
print('0x{:02x}'.format(out[i]), end=', ')

# 9787254630123759

get到了key之后有啥用呢(

去看看对于v9的判断,即sub_140001217

跟进去看看

注意一下这里的a1是上面get到的key

这个函数看来是把原来的check.dll改了个名字为check1.dll,之后读了data这个文件,将data与得到的key异或后命名为check.dll

对比一下两个dll是能看出不同的

左为原dll,右为用data异或key生成的dll

主程序的main函数会调用dll里面的check函数

所以只要分析一下check函数就好了

没什么好说的,就是一个异或,直接解就好

1
2
3
4
5
enc = [13, 8, 26, 10, 29, 15, 0x32, 0x78, 0x2a, 0x7b, 0x2a, 0x7b, 0x7c, 0x7d, 0x71, 0x64, 0x7a, 0x2c, 0x7b, 0x7d, 0x64, 0x28, 0x7d,
0x71, 0x2c, 0x64, 0x78, 0x78, 0x7d, 0x7a, 0x64, 0x28, 0x7a, 0x7d, 0x70, 127, 0x28, 0x7a, 0x2b, 0x7e, 0x7d, 0x79, 0x79, 0x34]
for i in enc:
print(chr(i ^ 0x49), end="")
# DASCTF{1c2c2548-3e24-a48e-1143-a3496a3b7400}