TMCTF Final 2020 Challenge 4 writeup
本文为之前参加过的ctf比赛的writeup，迁移到这个博客来吧
RE
Challenge 4（保底分）
- 这题不难,应该是最快打到低保分数的题了;
- 题目给了一个python文件和一个so文件,运行python文件,共有999个迷宫,每个迷宫是有一个32位输入的密钥拿去解密,每个迷宫对应一个函数,这个函数会对密钥的前16位进行约束,一看就感觉可以用z3来解;
- 提示指出迷宫1是第一扇门,输入1并把z3解出来的密钥和提示的后16位密钥拼起来得到了下一扇门的后16位密钥;
- 做到这里以为稳了,只要把剩下的门的前16位密钥都给解出来,然后拼起来一个一个去试把门给试出来就行;
- 然后就开始写代码,分成下面步骤:
- 首先考虑把IDA反编译的每个函数的代码给提取出来,问了A博代码的提取方法,虽然一开始乱找找到了,但是没想到C文件太大导致导出慢,还以为搞错了;
IDA提取C代码:File -> Produce File -> Create C file (ctrl+F5)
- 接下来写正则表达式把约束提取出来,转化成z3的python表示,这一步没什么好说,写的很快,后面再上和整理代码;
- 值得学习和记录的地方是打印下匹配的个数来确认下有没有cover到所有的case,然后就是局部测试;
- 解析成python代码这一块,注意下*a1这种替换成a1[0],然后不等号换等于号,没有等于号的加个等于号;
- 然后自动拼成个python,跑完一个开个文件写结果防止跑到半路出问题,当然中间为了防止出问题判断了下sat是否满足,不满足直接跳过了;
- 十年nt的我放在笔记本跑,所以为啥不用闲置的主机跑呢嘻嘻,然后挂了半天跑完了,一看结果感觉心都凉了,因为除了第一个其他的咋一看都不是题目说的大小写+数字的组合,还以为哪里搞错了,问了龙哥龙哥没看过题也不造哪里出了问题;
- 想了想既然限制了大小写+数字组合,那何不加个约束呢,说不定原来的约束非满秩有多解,但是这个美好的想法被我试了第二个之后发现无解给打破了,看来这个约束还是严谨的;
- 这里也怀疑过可能是搞错了或者提取错了,但是对比了一个感觉没有出错,这种自动化都能出错我是不信的,那就死马当活马医,加个约束放到主机上再跑一次;
- 跑完看到结果又成了,因为只有刚好10个结果…还以为全部都有结果要一个一个试呢,因为我模仿python文件轮流尝试的脚本都写好了;
- 接下来最后一步就是轮流尝试拼接密钥了,因为密钥空间被压缩到了只有10个,所以这一步是秒出结果;
这题给的教训:还是要多看看高手的z3是怎么写的,现在的太初级了,爆破空间的约束还是龙哥给写的,因为自己不确定要怎么写有效orz;
给个答案:
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
31python3 intest.py
>> 1 Msg: Open this door successfully. 9 rooms remain. The next key is {****************Q9ZAq73LPOYfGMHN}. <<<
Q9ZAq73LPOYfGMHN
>> 78 Msg: Open this door successfully. 8 rooms remain. The next key is {****************IQCfdbiwjYA4T9V0}. <<<
IQCfdbiwjYA4T9V0
>> 708 Msg: Open this door successfully. 7 rooms remain. The next key is {****************9PzNd8OIxq6Ejlwm}. <<<
9PzNd8OIxq6Ejlwm
>> 35 Msg: Open this door successfully. 6 rooms remain. The next key is {****************e9gOFilbwKWUhdIc}. <<<
e9gOFilbwKWUhdIc
>> 648 Msg: Open this door successfully. 5 rooms remain. The next key is {****************brSuV6Ys4zXkKMmO}. <<<
brSuV6Ys4zXkKMmO
>> 468 Msg: Open this door successfully. 4 rooms remain. The next key is {****************cqxFB8M3TpRUZAug}. <<<
cqxFB8M3TpRUZAug
>> 759 Msg: Open this door successfully. 3 rooms remain. The next key is {****************3nAwFOUNZl6mB0Jy}. <<<
3nAwFOUNZl6mB0Jy
>> 382 Msg: Open this door successfully. 2 rooms remain. The next key is {****************IXgjUQKHcmMAn0L3}. <<<
IXgjUQKHcmMAn0L3
>> 802 Msg: Open this door successfully. 1 room remains. The next key is {****************CduYaXnmPk6Hcxjb}. <<<
CduYaXnmPk6Hcxjb
>> 265 Msg: You have completed all challenges. The final flag is TMCTF{IsThisTheBeginningOfTheMazeOrTheEnd}. <<<
ed all challenge脚本
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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212from z3 import *
import re
import json
static_header='''def maze{}():
s=Solver()
a1=[BitVec('a[\%\d]'%(i),8) for i in range(32)]\n\n'''
static_end='''\ts.check()
g=s.model()
with open('mazeres','a') as f:
f.write('{}\\t'+str(g)+'\\n\\n')\n\n\n'''
def anayall(ccfile):
with open(ccfile,'r') as f:
rawstr=f.read()
rawstr=re.findall(r'(?<=4h\] \[rbp-1Ch\]\n\n if \( )[^\)]*(?=\)\n \{)',rawstr)
for i in range(1,1001):
solrawtoz3(rawstr[i-1],i)
savefile='ddd.py'
newheader='''
s=Solver()
a1=[BitVec('a[%d]'%(i),8) for i in range(32)]
s.add(Or(And(a1[0] <= ord('z'), a1[0] >= ord('a')), (And(a1[0] <= ord('Z'), a1[0] >= ord('A'))), (And(a1[0] <= ord('9'), a1[0] >= ord('0')))))
s.add(Or(And(a1[1] <= ord('z'), a1[1] >= ord('a')), (And(a1[1] <= ord('Z'), a1[1] >= ord('A'))), (And(a1[1] <= ord('9'), a1[1] >= ord('0')))))
s.add(Or(And(a1[2] <= ord('z'), a1[2] >= ord('a')), (And(a1[2] <= ord('Z'), a1[2] >= ord('A'))), (And(a1[2] <= ord('9'), a1[2] >= ord('0')))))
s.add(Or(And(a1[3] <= ord('z'), a1[3] >= ord('a')), (And(a1[3] <= ord('Z'), a1[3] >= ord('A'))), (And(a1[3] <= ord('9'), a1[3] >= ord('0')))))
s.add(Or(And(a1[4] <= ord('z'), a1[4] >= ord('a')), (And(a1[4] <= ord('Z'), a1[4] >= ord('A'))), (And(a1[4] <= ord('9'), a1[4] >= ord('0')))))
s.add(Or(And(a1[5] <= ord('z'), a1[5] >= ord('a')), (And(a1[5] <= ord('Z'), a1[5] >= ord('A'))), (And(a1[5] <= ord('9'), a1[5] >= ord('0')))))
s.add(Or(And(a1[6] <= ord('z'), a1[6] >= ord('a')), (And(a1[6] <= ord('Z'), a1[6] >= ord('A'))), (And(a1[6] <= ord('9'), a1[6] >= ord('0')))))
s.add(Or(And(a1[7] <= ord('z'), a1[7] >= ord('a')), (And(a1[7] <= ord('Z'), a1[7] >= ord('A'))), (And(a1[7] <= ord('9'), a1[7] >= ord('0')))))
s.add(Or(And(a1[8] <= ord('z'), a1[8] >= ord('a')), (And(a1[8] <= ord('Z'), a1[8] >= ord('A'))), (And(a1[8] <= ord('9'), a1[8] >= ord('0')))))
s.add(Or(And(a1[9] <= ord('z'), a1[9] >= ord('a')), (And(a1[9] <= ord('Z'), a1[9] >= ord('A'))), (And(a1[9] <= ord('9'), a1[9] >= ord('0')))))
s.add(Or(And(a1[10] <= ord('z'), a1[10] >= ord('a')), (And(a1[10] <= ord('Z'), a1[10] >= ord('A'))), (And(a1[10] <= ord('9'), a1[10] >= ord('0')))))
s.add(Or(And(a1[11] <= ord('z'), a1[11] >= ord('a')), (And(a1[11] <= ord('Z'), a1[11] >= ord('A'))), (And(a1[11] <= ord('9'), a1[11] >= ord('0')))))
s.add(Or(And(a1[12] <= ord('z'), a1[12] >= ord('a')), (And(a1[12] <= ord('Z'), a1[12] >= ord('A'))), (And(a1[12] <= ord('9'), a1[12] >= ord('0')))))
s.add(Or(And(a1[13] <= ord('z'), a1[13] >= ord('a')), (And(a1[13] <= ord('Z'), a1[13] >= ord('A'))), (And(a1[13] <= ord('9'), a1[13] >= ord('0')))))
s.add(Or(And(a1[14] <= ord('z'), a1[14] >= ord('a')), (And(a1[14] <= ord('Z'), a1[14] >= ord('A'))), (And(a1[14] <= ord('9'), a1[14] >= ord('0')))))
s.add(Or(And(a1[15] <= ord('z'), a1[15] >= ord('a')), (And(a1[15] <= ord('Z'), a1[15] >= ord('A'))), (And(a1[15] <= ord('9'), a1[15] >= ord('0')))))\n\n'''
newend='''
if s.check()==sat:
g=s.model()
with open('mazeres','a') as f:
f.write('{}\\t'+str(g)+'\\n\\n')\n\n\n'''
def solrawtoz3(rawstr,doornum):
global savefile
eqlist=rawstr.replace('*a1','a1[0]').replace('!=','==').split('\n ||')
with open(savefile,'a') as f:
f.write(newheader.format(doornum))
for eqstr in eqlist:
if '==' not in eqstr:
eqstr+='==0'
eqstr=eqstr.replace('\n ','')
with open(savefile,'a') as f:
f.write('s.add('+eqstr+')\n')
with open(savefile,'a') as f:
f.write(newend.format(doornum))
def anares(keyfile):
with open(keyfile,'r') as f:
b=f.read()
mazres=b.split('\n\n')
print(len(mazres))
mazkeydict=dict()
for eachmaz in mazres:
if not len(eachmaz):
break
numlist=eachmaz.split('\n')
maznum=numlist[0].split('\t')[0]
mazkey=[0]*16
for num in numlist:
print(num)
charnum=int(re.findall(r'(?<=a\[)\d*',num)[0])
val=int(re.findall(r'(?<= \= )\d*',num)[0])
mazkey[charnum]=val
keystr=''
for i in mazkey:
keystr+=chr(i)
mazkeydict[maznum]=keystr
with open('mazkeystr','w') as f:
json.dump(mazkeydict,f)
def testz322():
s=Solver()
a1=[BitVec('a[%d]'%(i),8) for i in range(32)]
s.add(Or(And(a1[2] <= ord('z'), a1[2] >= ord('a')), (And(a1[2] <= ord('Z'), a1[2] >= ord('A'))), (And(a1[2] <= ord('9'), a1[2] >= ord('0')))))
s.check()
print(s.model())
def testmaze():
s=Solver()
a1=[BitVec('a[%d]'%(i),8) for i in range(32)]
# cccset=set([48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 97, 65, 98, 66, 99, 67, 100, 68, 101, 69, 102, 70, 103, 71, 104, 72, 105, 73, 106, 74, 107, 75, 108, 76, 109, 77, 110, 78, 111, 79, 112, 80, 113, 81, 114, 82, 115, 83, 116, 84, 117, 85, 118, 86, 119, 87, 120, 88, 121, 89, 122, 90])
# s.add(a1[13] in cccset)
# s.add(Or(And(a1 <= ord('z'), a1 >= ord('a')), (And(a1 <= ord('Z'), a1 >= ord('A')))))
s.add(Or(And(a1[15] <= ord('z'), a1[15] >= ord('a')), (And(a1[15] <= ord('Z'), a1[15] >= ord('A'))), (And(a1[15] <= ord('9'), a1[15] >= ord('0')))))
s.add(a1[11]+ a1[4]+ a1[14]+ a1[4]+ a1[12]+ a1[11]+ a1[13]+ a1[0]+ a1[9]+ a1[8]+ a1[10]+ 85- a1[6]- a1[6]- 23- a1[2]+ 203+ a1[1]+ 236+ a1[4]- 24- a1[3]- a1[0]- a1[7]+ 57- a1[5]- 176+ a1[15]- 98- a1[3]- a1[7]- a1[12] == 630)
s.add( a1[7]+ a1[4]+ a1[10]+ a1[5]+ a1[15]+ a1[12]+ a1[13]+ a1[1]+ 142- a1[14]+ a1[4]- 133+ a1[15]- 198- a1[9]- a1[8]- a1[11]- 246+ a1[3]+ 130- a1[2]+ 248- a1[6]- a1[0]- a1[13]+ 225- a1[0]- a1[8]- 24+ a1[0]- 222- a1[0] == 121)
s.add( a1[13]+ a1[15]+ a1[8]+ a1[2]+ a1[10]+ a1[2]- 14+ a1[4]- 226- a1[5]- 122- a1[7]+ 65- a1[3]- a1[5]- a1[12]- a1[11]- a1[0]+ a1[1]- a1[0]+ 212+ a1[15]- a1[12]- a1[15]- a1[6]+ 115- a1[9]- a1[14]- 84- a1[11] == -499)
s.add( a1[14]+ a1[9]+ a1[9]+ a1[6]+ a1[4]+ a1[4]- 98+ a1[5]- 218+ a1[10]+ 50- a1[12]- a1[0]- a1[12]- a1[1]- a1[0]- a1[12]- a1[3]- 67+ a1[7]- 58- a1[12]+ a1[8]- 146- a1[15]+ 64+ a1[2]+ 11- a1[13]- a1[12] == -622)
s.add( a1[10]+ a1[3]+ a1[4]+ a1[4]+ a1[6]+ a1[3]+ a1[13]+ a1[2]+ a1[4]+ a1[7]+ 23- a1[8]+ 140- a1[12]- 190+ a1[1]+ 75- a1[5]- a1[15]- a1[11]- 48+ a1[2]- 250- a1[11]+ a1[9]- 177- a1[14]- a1[15]- a1[1]+ a1[14] == -176)
s.add( a1[13]+ a1[14]+ a1[11]+ a1[0]+ a1[4]+ a1[11]+ a1[7]+ a1[3]+ a1[2]+ 169- a1[10]- 86- a1[14]- a1[6]+ a1[12]+ 34- a1[0]- a1[6]- a1[6]- 213+ a1[5]+ 131- a1[11]+ 174- a1[15]+ a1[8]+ 10- a1[1]+ 41+ a1[9]+ 18+ a1[14] == 861)
s.add( a1[7]+ a1[10]+ a1[0]+ a1[6]+ a1[6]+ a1[14]+ a1[4]- a1[13]+ 17- a1[5]- a1[14]- 102+ a1[9]- 73- a1[4]+ a1[2]- 203+ a1[10]+ 118+ a1[1]- 181+ a1[15]- 4- a1[3]+ 233- a1[8]- a1[12]- a1[12]- 114+ a1[11]+ 64- a1[6] == -34)
s.add( a1[15]+ a1[1]+ a1[0]+ a1[6]+ a1[14]+ a1[12]+ a1[2]+ 68+ a1[1]- 136- a1[8]+ 90+ a1[3]+ 141+ a1[4]- 55- a1[14]- a1[13]- a1[15]- a1[5]+ 155- a1[9]- 193+ a1[13]- 255- a1[7]- 9- a1[10]- 51+ a1[6] == 91)
s.add( a1[13]+ a1[15]+ a1[8]+ a1[6]+ a1[4]+ a1[2]+ a1[0]+ a1[10]+ a1[15]+ a1[6]- a1[10]- a1[10]- a1[13]+ a1[12]+ 89- a1[13]+ a1[7]+ 133- a1[5]- a1[14]- a1[13]+ a1[1]- 64+ a1[11]+ 110- a1[3]- a1[12]- a1[9]- a1[4]- a1[10]- a1[4]+ a1[0] == 489)
s.add( a1[8]+ a1[12]+ a1[2]+ a1[6]+ a1[3]+ a1[0]+ a1[4]+ a1[6]+ a1[5]+ a1[13]+ 143+ a1[0]- 29- a1[9]- a1[10]- a1[13]- a1[2]- a1[1]- a1[6]- a1[15]+ 68- a1[12]- a1[2]+ a1[11]- 137- a1[10]+ 50- a1[14]+ 38+ a1[7]- 205- a1[0] == -3)
s.add( a1[11]+ a1[12]+ a1[3]+ a1[14]+ a1[15]+ a1[14]+ a1[1]+ 5- a1[15]- 54- a1[5]- a1[7]- a1[2]+ 88- a1[12]+ 224- a1[8]- 93- a1[0]- a1[13]- 211- a1[6]+ 71+ a1[10]- 82+ a1[7]+ 145- a1[12]+ a1[9]+ 233- a1[4]+ a1[7] == 354)
s.add( a1[11]+ a1[3]+ a1[7]+ a1[0]+ a1[2]+ a1[13]+ a1[6]- 80- a1[12]- a1[9]- a1[10]- 234- a1[7]- a1[1]+ 44+ a1[15]- 20- a1[2]+ 212+ a1[8]- 216- a1[12]- a1[7]+ 98+ a1[11]- 234- a1[5]- 168+ a1[14]- 17- a1[4]+ a1[1] == -513)
s.add( a1[15]+ a1[6]+ a1[8]+ a1[13]+ a1[15]+ a1[9]+ a1[7]+ a1[12]+ a1[7]+ a1[12]+ a1[1]+ a1[3]- 123+ a1[7]+ 80+ a1[13]+ 140- a1[0]- 91- a1[14]- a1[4]- a1[3]+ a1[2]+ 10- a1[10]- 161- a1[6]- a1[11]+ 13+ a1[5]- 86- a1[2] == 673)
s.add( a1[10]+ a1[4]+ a1[0]+ a1[15]+ a1[15]+ a1[0]+ a1[1]+ a1[0]+ a1[7]+ a1[10]+ a1[2]+ a1[9]- 147- a1[8]- a1[5]- a1[2]+ a1[11]+ 171- a1[3]- a1[14]- a1[14]+ 213- a1[7]- a1[1]- a1[6]- a1[3]- a1[5]+ a1[13]- 66- a1[12]+ 12- a1[5] == 96)
s.add( a1[2]+ a1[11]+ a1[10]+ a1[10]+ a1[3]+ a1[0]+ a1[8]+ a1[4]- a1[1]- a1[11]- a1[5]+ 243- a1[3]+ 142- a1[13]- a1[5]- a1[12]- a1[1]- a1[1]- a1[3]- a1[6]- a1[12]- a1[9]- a1[9]- a1[15]+ 196- a1[7]- 22+ a1[14]- 133- a1[1]+ a1[0] == -536)
s.add( a1[14]+ a1[3]+ a1[14]+ a1[13]+ a1[15]+ a1[7]+ a1[11]+ a1[3]+ a1[14]+ a1[2]+ a1[8]+ a1[6]+ a1[10]+ a1[9]- 162- a1[7]- a1[2]+ 86- a1[0]- a1[5]- a1[2]- a1[1]- a1[4]+ a1[12]- 140- a1[5]- a1[8]- a1[13]- a1[6]- a1[1]- a1[3]+ a1[4] ==0)
s.check()
g=s.model()
print(g)
def genheader():
a='''
s.add(Or(And(a1[{}] <= ord('z'), a1[{}] >= ord('a')), (And(a1[{}] <= ord('Z'), a1[{}] >= ord('A'))), (And(a1[{}] <= ord('9'), a1[{}] >= ord('0')))))
'''
header2=''
for i in range(16):
header2+=a.format(i,i,i,i,i,i)
print(header2)
def aaa():
dd=[]
for i in range(10):
dd.append(i+ord('0'))
for i in range(26):
dd.append(i+ord('a'))
dd.append(i+ord('A'))
print(dd)
dd=set(dd)
print(dd)
if __name__=='__main__':
# solrawtoz3('re\\challenge4\\raw2','ddd.py')
# maze2()
# anayall('re\\challenge4\\tmmaze.c')
anares('mazeres')
# testmaze()
# genheader()
# aaa()
# testz322()
- 最后的踹门脚本
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#encoding=utf-8
import os, ctypes
import json
import re
mazinfo=dict()
with open('mazkeystr','r') as f:
mazinfo=json.load(f)
roomlist=mazinfo.keys()
def alltest():
global mazinfo
fname_tmmaze = "./tmmaze.so"
if os.path.exists(fname_tmmaze):
tmmaze = ctypes.cdll.LoadLibrary(fname_tmmaze)
lastkey='Ln7Vm2RgHMQei0WZ'
for i in range(12):
for curroom in roomlist:
curkey=mazinfo[curroom]+lastkey
room = "Room" + "{:03d}".format(int(curroom))
decryptedtext = ctypes.create_string_buffer(128)
if tmmaze[room](curkey.encode("utf-8"), decryptedtext) == 1:
room_msg = decryptedtext.value
print("\n >>> " + curroom + " Msg: " + room_msg.decode("utf-8") + " <<<")
room_msg=room_msg.decode('utf-8')
lastkey=room_msg[room_msg.find('{****************')+len('{****************'):room_msg.find('{****************')+len('{****************')+16]
print(lastkey)
if __name__=='__main__':
alltest()
本博客所有文章除特别声明外，均采用 CC BY-NC-SA 4.0 许可协议。转载请注明来自 Exp！