• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# Untitled

a guest Oct 20th, 2019 93 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. import struct
2. from z3 import *
3. import string
4.
5. def prettify(data):
6.   return ''.join([ ('\033[1;32m%s\033[0m' % c if c in string.printable[:-5] else '\033[2;32m_\033[0m' ) if c in string.printable else ('\033[2;31m?\033[0m' if c == '\x00' else '\033[2;33m?\033[0m') for c in data ]) + '\033[0m'
7.
8. s = Solver()
9. char  = [ BitVec('char_%d' % i, 8) for i in range(260) ]
10. word  = [ BitVec('word_%d' % i, 16) for i in range(260) ]
11. dword = [ BitVec('dword_%d' % i, 32) for i in range(260-4) ]
12.
13. for i in range(260): s.add(char[i] >= 0)
14.
15. # TODO: fix this
16. for i in range(130):
17.   s.add(word[i] & 0xff == ZeroExt(8, char[2*i]))
18.   s.add((word[i] >> 8) & 0xff == ZeroExt(8, char[2*i + 1]))
19.
20. for i in range(260-4):
21.   for j in range(4):
22.     s.add((dword[i] >> (8*j)) & 0xff == ZeroExt(24, char[i + j]))
23.
24. # CHARS
25.
26. # 1
27. s.add(char[0] * char[6] == -118, char[0] - char[6] == 55)
28.
29. # 2
30. s.add(char[0] + char[7] == 111, char[0] * char[7] == -82)
31.
32. # 9
33. s.add(char[16] - char[2] == -23, char[16] / char[2] == 0)
34.
35. # 10
36. s.add(char[17] + char[3] == -97, char[3] * char[17] == 10)
37.
38. # 21
39. s.add(char[36] - char[37] == -33, char[36] * char[37] == -100)
40.
41. # 22
42. s.add(char[44] - char[66] == 1, char[44] + char[66] == 91)
43.
44. # 23
45. s.add(char[1] - char[54] == -5, char[1] / char[54] == 0)
46.
47. # 24
48. s.add(char[1] / char[55] == 0, char[1] - char[55] == -6)
49.
50. # 29
51. s.add(char[45] == char[82], char[82] * char[45] == 68)
52.
53. # 33
54. s.add(char[67] - char[78] == 55, char[78] * char[67] == 38)
55.
56. # 36
57. s.add(char[84] - char[85] == -17, char[84] / char[85] == 0)
58.
59. # 37
60. s.add(char[72] + char[92] == -89, char[92] * char[72] == -66)
61.
62. # 38
63. s.add(char[72] - char[93] == -65, char[72] * char[93] == -14)
64.
65. # 41
66. s.add(char[79] + char[83] == 92, char[79] == char[83])
67.
68. # 43
69. s.add(char[84] / char[94] == 0, char[84] - char[94] == -30)
70.
71. # 44
72. s.add(char[85] + char[94] == -35, char[85] / char[94] == 0)
73.
74. # 46
75. s.add(char[90] - char[92] == -6, char[90] + char[92] == -20)
76.
77. # 49
78. s.add(char[73] * char[91] == -128, char[91] - char[73] == -84)
79.
80. # 53
81. s.add(char[95] / char[126] == 2, char[126] * char[95] == 124)
82.
83. # 54
84. s.add(char[95] - char[127] == 68, char[95] / char[127] == 2)
85.
86. # 55
87. s.add(char[93] + char[106] == -44, char[93] - char[106] == 10)
88.
89. # 63
90. s.add(char[128] / char[130] == 1, char[128] + char[130] == 92)
91.
92. # 64
93. s.add(char[130] * char[129] == 68, char[129] / char[130] == 1)
94.
95. # 65
96. s.add(char[110] - char[73] == -70, char[73] * char[110] == -40)
97.
98. # 66
99. s.add(char[111] - char[138] == -68, char[111] / char[138] == 0)
100.
101. # 67
102. s.add(char[131] / char[136] == 1, char[131] + char[136] == 78)
103.
104. # 68
105. s.add(char[131] / char[137] == 0, char[131] + char[137] == -113)
106.
107. # 75
108. s.add(char[148] - char[162] == -15, char[162] * char[148] == -60)
109.
110. # 76
111. s.add(char[149] / char[162] == 0, char[149] + char[162] == -38)
112.
113. # 78
114. s.add(char[154] / char[107] == 1, char[154] + char[107] == -90)
115.
116. # 79
117. s.add(char[160] / char[139] == 0, char[160] - char[139] == -4)
118.
119. # 80
120. s.add(char[158] * char[161] == -125, char[161] + char[158] == -60)
121.
122. # 82
123. s.add(char[159] * char[166] == 54, char[166] + char[159] == -27)
124.
125. # 83
126. s.add(char[164] - char[155] == 82, char[155] * char[164] == 64)
127.
128. # 84
129. s.add(char[164] + char[170] == -27, char[164] / char[170] == 0)
130.
131. # 90
132. s.add(char[171] + char[184] == 42, char[184] * char[171] == 64)
133.
134. # 91
135. s.add(char[165] - char[169] == 6, char[169] * char[165] == -101)
136.
137. # 93
138. s.add(char[166] + char[176] == -30, char[176] * char[166] == -35)
139.
140. # 94
141. s.add(char[167] + char[177] == -23, char[167] - char[177] == -1)
142.
143. # 95
144. s.add(char[167] - char[178] == 2, char[167] / char[178] == 1)
145.
146. # 97
147. s.add(char[184] * char[180] == 96, char[180] + char[184] == 122)
148.
149. # 98
150. s.add(char[185] * char[181] == 38, char[181] / char[185] == 2)
151.
152. # 99
153. s.add(char[185] / char[186] == 1, char[186] * char[185] == 68)
154.
155. # 103
156. s.add(char[179] - char[192] == -14, char[179] / char[192] == 0)
157.
158. # 105
159. s.add(char[187] - char[202] == -73, char[187] + char[202] == -91)
160.
161. # 109
162. s.add(char[200] * char[193] == 38, char[193] - char[200] == -55)
163.
164. # 110
165. s.add(char[200] - char[201] == -10, char[201] * char[200] == -53)
166.
167. # 112
168. s.add(char[212] - char[220] == -71, char[220] * char[212] == -60)
169.
170. # 115
171. s.add(char[203] - char[228] == -72, char[203] + char[228] == -96)
172.
173. # 116
174. s.add(char[213] + char[229] == -127, char[229] * char[213] == 32)
175.
176. # 121
177. s.add(char[201] * char[230] == -78, char[230] - char[201] == -1)
178.
179. # 122
180. s.add(char[231] / char[256] == 1, char[231] - char[256] == 15)
181.
182. # 123
183. s.add(char[240] + char[246] == -48, char[240] / char[246] == 0)
184.
185. # 124
186. s.add(char[241] + char[246] == -35, char[241] / char[246] == 0)
187.
188. # 127
189. s.add(char[242] + char[243] == -108, char[242] - char[243] == 84)
190.
191. # 133
192. s.add(char[247] / char[258] == 0, char[247] - char[258] == -19)
193.
194. # 134
195. s.add(char[247] / char[259] == 10, char[259] * char[247] == -24)
196.
197. # 135
198. s.add(char[257] - char[221] == -5, char[257] + char[221] == -29)
199.
200. # WORDS
201.
202. # 5
203. s.add(word[2] + word[6] == -23149, word[2] / word[6] == 2)
204.
205. # 8
206. s.add(word[9] * word[1] == -1004, word[9] - word[1] == -17687)
207.
208. # 11
209. s.add(word[9] / word[11] == 0, word[9] + word[11] == -26183)
210.
211. # 16
212. s.add(word[19] + word[12] == -8250, word[19] / word[12] == 0)
213.
214. # 18
215. s.add(word[14] == word[15], word[14] / word[15] == 1)
216.
217. # 25
218. s.add(word[24] - word[30] == -16461, word[24] / word[30] == 0)
219.
220. # 26
221. s.add(word[28] * word[30] == -2766, word[28] / word[30] == 1)
222.
223. # 27
224. s.add(word[29] * word[33] == -10967, word[29] - word[33] == 64)
225.
226. # 28
227. s.add(word[29] + word[38] == 28641, word[29] - word[38] == 23289)
228.
229. # 30
230. s.add(word[31] * word[32] == -3166, word[31] + word[32] == -14639)
231.
232. # 34
233. s.add(word[35] - word[40] == 15931, word[35] + word[40] == -25961)
234.
235. # 35
236. s.add(word[40] / word[41] == 1, word[40] * word[41] == -28604)
237.
238. # 39
239. s.add(word[39] - word[37] == -17719, word[39] + word[37] == -24173)
240.
241. # 40
242. s.add(word[43] * word[37] == 32069, word[43] / word[37] == 1)
243.
244. # 45
245. s.add(word[44] - word[45] == 18605, word[44] + word[45] == -30317)
246.
247. # 47
248. s.add(word[48] + word[50] == -7353, word[48] / word[50] == 1)
249.
250. # 48
251. s.add(word[49] * word[57] == 4134, word[49] - word[57] == 17975)
252.
253. # 50
254. s.add(word[52] - word[54] == 16215, word[52] + word[54] == -25749)
255.
256. # 56
257. s.add(word[51] * word[55] == -30272, word[51] - word[55] == 16370)
258.
259. # 57
260. s.add(word[54] / word[56] == 0, word[54] - word[56] == -36)
261.
262. # 58
263. s.add(word[58] * word[59] == 24574, word[58] + word[59] == -11589)
264.
265. # 59
266. s.add(word[60] - word[72] == -767, word[60] / word[72] == 0)
267.
268. # 60
269. s.add(word[61] + word[72] == -11834, word[61] - word[72] == 1788)
270.
271. # 61
272. s.add(word[62] + word[63] == 14490, word[62] - word[63] == -9154)
273.
274. # 62
275. s.add(word[62] - word[64] == -9154, word[62] + word[64] == 14490)
276.
277. # 71
278. s.add(word[68] * word[70] == -23552, word[68] + word[70] == -10944)
279.
280. # 72
281. s.add(word[69] + word[70] == -9838, word[69] - word[70] == -3758)
282.
283. # 73
284. s.add(word[73] + word[74] == -13691, word[73] / word[74] == 0)
285.
286. # 74
287. s.add(word[73] + word[75] == -11639, word[73] * word[75] == -12000)
288.
289. # 77
290. s.add(word[76] - word[71] == -1023, word[76] * word[71] == -25432)
291.
292. # 81
293. s.add(word[78] + word[71] == -9525, word[78] / word[71] == 0)
294.
295. # 85
296. s.add(word[86] - word[87] == -4785, word[86] + word[87] == -8305)
297.
298. # 86
299. s.add(word[87] / word[97] == 2, word[87] * word[97] == -31808)
300.
301. # 89
302. s.add(word[84] + word[91] == -23843, word[84] - word[91] == 9205)
303.
304. # 101
305. s.add(word[94] / word[95] == 1, word[94] == word[95])
306.
307. # 102
308. s.add(word[95] + word[102] == -27058, word[95] * word[102] == 30144)
309.
310. # 107
311. s.add(word[101] + word[109] == -25628, word[101] / word[109] == 0)
312.
313. # 108
314. s.add(word[104] + word[117] == -31330, word[104] / word[117] == 3)
315.
316. # 111
317. s.add(word[105] - word[113] == 1280, word[105] + word[113] == -5666)
318.
319. # 113
320. s.add(word[107] - word[112] == 1269, word[107] * word[112] == -9542)
321.
322. # 114
323. s.add(word[107] + word[114] == -10538, word[107] - word[114] == 5102)
324.
325. # 117
326. s.add(word[108] * word[111] == -23936, word[108] + word[111] == -30316)
327.
328. # 118
329. s.add(word[108] + word[113] == -27933, word[108] / word[113] == 0)
330.
331. # 120
332. s.add(word[115] / word[119] == 0, word[115] * word[119] == -20544)
333.
334. # 125
335. s.add(word[116] + word[121] == -26144, word[116] * word[121] == -31504)
336.
337. # 126
338. s.add(word[116] * word[124] == 17792, word[116] + word[124] == -5236)
339.
340. # 129
341. s.add(word[118] * word[122] == 32624, word[118] / word[122] == 0)
342.
343. # 130
344. s.add(word[122] + word[125] == -10545, word[122] - word[125] == 2045)
345.
346. # 131
347. s.add(word[126] * word[127] == 15616, word[126] + word[127] == -7544)
348.
349. # 132
350. s.add(word[128] + word[129] == 31196, word[128] - word[129] == 25838)
351.
352. # DWORDS
353.
354. # 7
355. s.add(dword[14] / dword[38] == 0, dword[14] * dword[38] == -696380050)
356.
357. # 12
358. s.add(dword[20] - dword[46] == 1816607519, dword[20] / dword[46] == 746)
359.
360. # 31
361. s.add(dword[62] - dword[68] == -117309447, dword[62] + dword[68] == -774585645)
362.
363. # 52
364. s.add(dword[120] - dword[170] == 99762675, dword[120] * dword[170] == 709227474)
365.
366. # 69
367. s.add(dword[132] + dword[150] == -490023232, dword[132] - dword[150] == 100137454)
368.
369. # 70
370. s.add(dword[132] * dword[210] == -1934577991, dword[132] + dword[210] == -1802641466)
371.
372. # 92
373. s.add(dword[176] + dword[218] == -1796872996, dword[176] / dword[218] == 0)
374.
375. # 100
376. s.add(dword[186] * dword[192] == 685543492, dword[186] / dword[192] == 1)
377.
378. # 104
379. # s.add(dword[196] * dword[206] == 1254425096, dword[196] / dword[206] == 1)
380.
381. # 128
382. s.add(dword[252] + dword[248] == -712382840, dword[252] * dword[248] == -829629184)
383.
384. # predict
385. for i, c in zip(range(16), 'Andrew\n.........'):
387.
388. for i, c in zip(range(16, 32), 'M-M-Miller\n.....'):
390.
391. for i, c in zip(range(32, 32+16), 'The Stammer\n....'):
393.
394. for i, c in zip(range(52+2, 52+2+30), 'stammer@fake-email.test\n......'):
396.
397. for i, c in zip(range(84, 84+13), 'What is your '): # ??
399.
400. for i, c in zip(range(116, 116+16), 'Fluffball\n......'):
402.
403. for i, c in zip(range(132, 132+64), 'What are three defining characteristics of your pet?\n...........'):
405.
406. for i, c in zip(range(196+16, 196+16+43), ', but most importantly, he want food right '):
408.
409. '''
410. # 17
411.
412. f24 = struct.unpack('f', pm[24:28])[0]
413.
414. f54 = struct.pack('f', 1.3727851e17 / f24)
415. print f54.encode('hex')
416.
417. f54 = struct.pack('f', 4.3609316e27 - f24)
418. print f54.encode('hex')
419. --> 7374616d
420. '''
421. for i, c in zip(range(54, 54 + 4), '7374616d'.decode('hex')):
423.
424. '''
425. # 20
426.
427. f104 = struct.unpack('f', pm[104:108])[0]
428.
429. f50 = struct.pack('f', 4.2070047e30 / f104)
430. print f50.encode('hex')
431.
432. f50 = struct.pack('f', 4.6942686e30 + f104)
433. print f50.encode('hex')
434. --> 00006d72
435. '''
436. for i, c in zip(range(50, 50 + 4), '00006d72'.decode('hex')):
438.
439. '''
440. # 106
441.
442. f238 = struct.unpack('f', pm[238:242])[0]
443.
444. f196 = struct.pack('f', 2.0547047e28 - f238)
445. print f196.encode('hex')
446.
447. f196 = struct.pack('f', 0.17785008 * f238)
448. print f196.encode('hex')
449. --> 6765206d
450. '''
451. for i, c in zip(range(196, 196 + 4), '6765206d'.decode('hex')):
453.
454. assert s.check() == sat
455. m = s.model()
456. pm = ''.join([ chr(m[char[i]].as_long()) for i in range(260) ])
457. print prettify(pm)
458.
459. print 'First name =', prettify(pm[0:16])
460. print 'Last name  =', prettify(pm[16:32])
461. print 'Nickname   =', prettify(pm[32:48])
462. print 'Age        =', struct.unpack('i', pm[48:52])[0]
463. print 'Email      =', prettify(pm[52:84])
464. print 'Question 1 =', prettify(pm[84:116])
465. print 'Answer 1   =', prettify(pm[116:132])
466. print 'Question 2 =', prettify(pm[132:196])
467. print 'Answer 2   =', prettify(pm[196:260])
468.
469. # 32..36
470. # 48..52
471. # 52..56
472. # 196..200
473.
474. '''
475. # 4
476. f8 = struct.unpack('f', pm[8:12])[0]
477.
478. f32 = struct.pack('f', f8 - 3.9604035e-11)
479. print f32.encode('hex')
480.
481. f32 = struct.pack('f', 7.6956873e-30 / f8)
482. print f32.encode('hex')
483. '''
484.
485. '''
486. # 19
487.
488. f96 = struct.unpack('f', pm[96:100])[0]
489.
490. f50 = struct.pack('f', 7.740607e31 - f96)
491. print f50.encode('hex')
492.
493. f50 = struct.pack('f', 0.064559929 * f96)
494. print f50.encode('hex')
495. '''
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top