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.........'):
  386.   s.add(char[i] == ord(c))
  387.  
  388. for i, c in zip(range(16, 32), 'M-M-Miller\n.....'):
  389.   s.add(char[i] == ord(c))
  390.  
  391. for i, c in zip(range(32, 32+16), 'The Stammer\n....'):
  392.   s.add(char[i] == ord(c))
  393.  
  394. for i, c in zip(range(52+2, 52+2+30), 'stammer@fake-email.test\n......'):
  395.   s.add(char[i] == ord(c))
  396.  
  397. for i, c in zip(range(84, 84+13), 'What is your '): # ??
  398.   s.add(char[i] == ord(c))
  399.  
  400. for i, c in zip(range(116, 116+16), 'Fluffball\n......'):
  401.   s.add(char[i] == ord(c))
  402.  
  403. for i, c in zip(range(132, 132+64), 'What are three defining characteristics of your pet?\n...........'):
  404.   s.add(char[i] == ord(c))
  405.  
  406. for i, c in zip(range(196+16, 196+16+43), ', but most importantly, he want food right '):
  407.   s.add(char[i] == ord(c))
  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')):
  422.   s.add(char[i] == ord(c))
  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')):
  437.   s.add(char[i] == ord(c))
  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')):
  452.   s.add(char[i] == ord(c))
  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. OK, I Understand
 
Top