pwn-thy-bytes-primitive-obsession.py

import struct
from z3 import *
import string

def prettify(data):
  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'

s = Solver()
char  = [ BitVec('char_%d' % i, 8) for i in range(260) ]
word  = [ BitVec('word_%d' % i, 16) for i in range(260) ]
dword = [ BitVec('dword_%d' % i, 32) for i in range(260-4) ]

for i in range(260): s.add(char[i] >= 0)

# TODO: fix this
for i in range(130):
  s.add(word[i] & 0xff == ZeroExt(8, char[2*i]))
  s.add((word[i] >> 8) & 0xff == ZeroExt(8, char[2*i + 1]))

for i in range(260-4):
  for j in range(4):
    s.add((dword[i] >> (8*j)) & 0xff == ZeroExt(24, char[i + j]))

# CHARS

# 1
s.add(char[0] * char[6] == -118, char[0] - char[6] == 55)

# 2
s.add(char[0] + char[7] == 111, char[0] * char[7] == -82)

# 9
s.add(char[16] - char[2] == -23, char[16] / char[2] == 0)

# 10
s.add(char[17] + char[3] == -97, char[3] * char[17] == 10)

# 21
s.add(char[36] - char[37] == -33, char[36] * char[37] == -100)

# 22
s.add(char[44] - char[66] == 1, char[44] + char[66] == 91)

# 23
s.add(char[1] - char[54] == -5, char[1] / char[54] == 0)

# 24
s.add(char[1] / char[55] == 0, char[1] - char[55] == -6)

# 29
s.add(char[45] == char[82], char[82] * char[45] == 68)

# 33
s.add(char[67] - char[78] == 55, char[78] * char[67] == 38)

# 36
s.add(char[84] - char[85] == -17, char[84] / char[85] == 0)

# 37
s.add(char[72] + char[92] == -89, char[92] * char[72] == -66)

# 38
s.add(char[72] - char[93] == -65, char[72] * char[93] == -14)

# 41
s.add(char[79] + char[83] == 92, char[79] == char[83])

# 43
s.add(char[84] / char[94] == 0, char[84] - char[94] == -30)

# 44
s.add(char[85] + char[94] == -35, char[85] / char[94] == 0)

# 46
s.add(char[90] - char[92] == -6, char[90] + char[92] == -20)

# 49
s.add(char[73] * char[91] == -128, char[91] - char[73] == -84)

# 53
s.add(char[95] / char[126] == 2, char[126] * char[95] == 124)

# 54
s.add(char[95] - char[127] == 68, char[95] / char[127] == 2)

# 55
s.add(char[93] + char[106] == -44, char[93] - char[106] == 10)

# 63
s.add(char[128] / char[130] == 1, char[128] + char[130] == 92)

# 64
s.add(char[130] * char[129] == 68, char[129] / char[130] == 1)

# 65
s.add(char[110] - char[73] == -70, char[73] * char[110] == -40)

# 66
s.add(char[111] - char[138] == -68, char[111] / char[138] == 0)

# 67
s.add(char[131] / char[136] == 1, char[131] + char[136] == 78)

# 68
s.add(char[131] / char[137] == 0, char[131] + char[137] == -113)

# 75
s.add(char[148] - char[162] == -15, char[162] * char[148] == -60)

# 76
s.add(char[149] / char[162] == 0, char[149] + char[162] == -38)

# 78
s.add(char[154] / char[107] == 1, char[154] + char[107] == -90)

# 79
s.add(char[160] / char[139] == 0, char[160] - char[139] == -4)

# 80
s.add(char[158] * char[161] == -125, char[161] + char[158] == -60)

# 82
s.add(char[159] * char[166] == 54, char[166] + char[159] == -27)

# 83
s.add(char[164] - char[155] == 82, char[155] * char[164] == 64)

# 84
s.add(char[164] + char[170] == -27, char[164] / char[170] == 0)

# 90
s.add(char[171] + char[184] == 42, char[184] * char[171] == 64)

# 91
s.add(char[165] - char[169] == 6, char[169] * char[165] == -101)

# 93
s.add(char[166] + char[176] == -30, char[176] * char[166] == -35)

# 94
s.add(char[167] + char[177] == -23, char[167] - char[177] == -1)

# 95
s.add(char[167] - char[178] == 2, char[167] / char[178] == 1)

# 97
s.add(char[184] * char[180] == 96, char[180] + char[184] == 122)

# 98
s.add(char[185] * char[181] == 38, char[181] / char[185] == 2)

# 99
s.add(char[185] / char[186] == 1, char[186] * char[185] == 68)

# 103
s.add(char[179] - char[192] == -14, char[179] / char[192] == 0)

# 105
s.add(char[187] - char[202] == -73, char[187] + char[202] == -91)

# 109
s.add(char[200] * char[193] == 38, char[193] - char[200] == -55)

# 110
s.add(char[200] - char[201] == -10, char[201] * char[200] == -53)

# 112
s.add(char[212] - char[220] == -71, char[220] * char[212] == -60)

# 115
s.add(char[203] - char[228] == -72, char[203] + char[228] == -96)

# 116
s.add(char[213] + char[229] == -127, char[229] * char[213] == 32)

# 121
s.add(char[201] * char[230] == -78, char[230] - char[201] == -1)

# 122
s.add(char[231] / char[256] == 1, char[231] - char[256] == 15)

# 123
s.add(char[240] + char[246] == -48, char[240] / char[246] == 0)

# 124
s.add(char[241] + char[246] == -35, char[241] / char[246] == 0)

# 127
s.add(char[242] + char[243] == -108, char[242] - char[243] == 84)

# 133
s.add(char[247] / char[258] == 0, char[247] - char[258] == -19)

# 134
s.add(char[247] / char[259] == 10, char[259] * char[247] == -24)

# 135
s.add(char[257] - char[221] == -5, char[257] + char[221] == -29)

# WORDS

# 5
s.add(word[2] + word[6] == -23149, word[2] / word[6] == 2)

# 8
s.add(word[9] * word[1] == -1004, word[9] - word[1] == -17687)

# 11
s.add(word[9] / word[11] == 0, word[9] + word[11] == -26183)

# 16
s.add(word[19] + word[12] == -8250, word[19] / word[12] == 0)

# 18
s.add(word[14] == word[15], word[14] / word[15] == 1)

# 25
s.add(word[24] - word[30] == -16461, word[24] / word[30] == 0)

# 26
s.add(word[28] * word[30] == -2766, word[28] / word[30] == 1)

# 27
s.add(word[29] * word[33] == -10967, word[29] - word[33] == 64)

# 28
s.add(word[29] + word[38] == 28641, word[29] - word[38] == 23289)

# 30
s.add(word[31] * word[32] == -3166, word[31] + word[32] == -14639)

# 34
s.add(word[35] - word[40] == 15931, word[35] + word[40] == -25961)

# 35
s.add(word[40] / word[41] == 1, word[40] * word[41] == -28604)

# 39
s.add(word[39] - word[37] == -17719, word[39] + word[37] == -24173)

# 40
s.add(word[43] * word[37] == 32069, word[43] / word[37] == 1)

# 45
s.add(word[44] - word[45] == 18605, word[44] + word[45] == -30317)

# 47
s.add(word[48] + word[50] == -7353, word[48] / word[50] == 1)

# 48
s.add(word[49] * word[57] == 4134, word[49] - word[57] == 17975)

# 50
s.add(word[52] - word[54] == 16215, word[52] + word[54] == -25749)

# 56
s.add(word[51] * word[55] == -30272, word[51] - word[55] == 16370)

# 57
s.add(word[54] / word[56] == 0, word[54] - word[56] == -36)

# 58
s.add(word[58] * word[59] == 24574, word[58] + word[59] == -11589)

# 59
s.add(word[60] - word[72] == -767, word[60] / word[72] == 0)

# 60
s.add(word[61] + word[72] == -11834, word[61] - word[72] == 1788)

# 61
s.add(word[62] + word[63] == 14490, word[62] - word[63] == -9154)

# 62
s.add(word[62] - word[64] == -9154, word[62] + word[64] == 14490)

# 71
s.add(word[68] * word[70] == -23552, word[68] + word[70] == -10944)

# 72
s.add(word[69] + word[70] == -9838, word[69] - word[70] == -3758)

# 73
s.add(word[73] + word[74] == -13691, word[73] / word[74] == 0)

# 74
s.add(word[73] + word[75] == -11639, word[73] * word[75] == -12000)

# 77
s.add(word[76] - word[71] == -1023, word[76] * word[71] == -25432)

# 81
s.add(word[78] + word[71] == -9525, word[78] / word[71] == 0)

# 85
s.add(word[86] - word[87] == -4785, word[86] + word[87] == -8305)

# 86
s.add(word[87] / word[97] == 2, word[87] * word[97] == -31808)

# 89
s.add(word[84] + word[91] == -23843, word[84] - word[91] == 9205)

# 101
s.add(word[94] / word[95] == 1, word[94] == word[95])

# 102
s.add(word[95] + word[102] == -27058, word[95] * word[102] == 30144)

# 107
s.add(word[101] + word[109] == -25628, word[101] / word[109] == 0)

# 108
s.add(word[104] + word[117] == -31330, word[104] / word[117] == 3)

# 111
s.add(word[105] - word[113] == 1280, word[105] + word[113] == -5666)

# 113
s.add(word[107] - word[112] == 1269, word[107] * word[112] == -9542)

# 114
s.add(word[107] + word[114] == -10538, word[107] - word[114] == 5102)
  
# 117
s.add(word[108] * word[111] == -23936, word[108] + word[111] == -30316)

# 118
s.add(word[108] + word[113] == -27933, word[108] / word[113] == 0)

# 120
s.add(word[115] / word[119] == 0, word[115] * word[119] == -20544)

# 125
s.add(word[116] + word[121] == -26144, word[116] * word[121] == -31504)

# 126
s.add(word[116] * word[124] == 17792, word[116] + word[124] == -5236)

# 129
s.add(word[118] * word[122] == 32624, word[118] / word[122] == 0)

# 130
s.add(word[122] + word[125] == -10545, word[122] - word[125] == 2045)

# 131
s.add(word[126] * word[127] == 15616, word[126] + word[127] == -7544)

# 132
s.add(word[128] + word[129] == 31196, word[128] - word[129] == 25838)

# DWORDS

# 7
s.add(dword[14] / dword[38] == 0, dword[14] * dword[38] == -696380050)

# 12
s.add(dword[20] - dword[46] == 1816607519, dword[20] / dword[46] == 746)

# 31
s.add(dword[62] - dword[68] == -117309447, dword[62] + dword[68] == -774585645)

# 52
s.add(dword[120] - dword[170] == 99762675, dword[120] * dword[170] == 709227474)

# 69
s.add(dword[132] + dword[150] == -490023232, dword[132] - dword[150] == 100137454)

# 70
s.add(dword[132] * dword[210] == -1934577991, dword[132] + dword[210] == -1802641466)

# 92
s.add(dword[176] + dword[218] == -1796872996, dword[176] / dword[218] == 0)

# 100
s.add(dword[186] * dword[192] == 685543492, dword[186] / dword[192] == 1)

# 104
# s.add(dword[196] * dword[206] == 1254425096, dword[196] / dword[206] == 1)

# 128
s.add(dword[252] + dword[248] == -712382840, dword[252] * dword[248] == -829629184)

# predict
for i, c in zip(range(16), 'Andrew\n.........'):
  s.add(char[i] == ord(c))

for i, c in zip(range(16, 32), 'M-M-Miller\n.....'):
  s.add(char[i] == ord(c))

for i, c in zip(range(32, 32+16), 'The Stammer\n....'):
  s.add(char[i] == ord(c))

for i, c in zip(range(52+2, 52+2+30), 'stammer@fake-email.test\n......'):
  s.add(char[i] == ord(c))

for i, c in zip(range(84, 84+13), 'What is your '): # ??
  s.add(char[i] == ord(c))

for i, c in zip(range(116, 116+16), 'Fluffball\n......'):
  s.add(char[i] == ord(c))

for i, c in zip(range(132, 132+64), 'What are three defining characteristics of your pet?\n...........'):
  s.add(char[i] == ord(c))

for i, c in zip(range(196+16, 196+16+43), ', but most importantly, he want food right '):
  s.add(char[i] == ord(c))

'''
# 17

f24 = struct.unpack('f', pm[24:28])[0]

f54 = struct.pack('f', 1.3727851e17 / f24)
print f54.encode('hex')

f54 = struct.pack('f', 4.3609316e27 - f24)
print f54.encode('hex')
--> 7374616d
'''
for i, c in zip(range(54, 54 + 4), '7374616d'.decode('hex')):
  s.add(char[i] == ord(c))

'''
# 20

f104 = struct.unpack('f', pm[104:108])[0]

f50 = struct.pack('f', 4.2070047e30 / f104)
print f50.encode('hex')

f50 = struct.pack('f', 4.6942686e30 + f104)
print f50.encode('hex')
--> 00006d72
'''
for i, c in zip(range(50, 50 + 4), '00006d72'.decode('hex')):
  s.add(char[i] == ord(c))

'''
# 106

f238 = struct.unpack('f', pm[238:242])[0]

f196 = struct.pack('f', 2.0547047e28 - f238)
print f196.encode('hex')

f196 = struct.pack('f', 0.17785008 * f238)
print f196.encode('hex')
--> 6765206d
'''
for i, c in zip(range(196, 196 + 4), '6765206d'.decode('hex')):
  s.add(char[i] == ord(c))

assert s.check() == sat
m = s.model()
pm = ''.join([ chr(m[char[i]].as_long()) for i in range(260) ])
print prettify(pm)

print 'First name =', prettify(pm[0:16])
print 'Last name  =', prettify(pm[16:32])
print 'Nickname   =', prettify(pm[32:48])
print 'Age        =', struct.unpack('i', pm[48:52])[0]
print 'Email      =', prettify(pm[52:84])
print 'Question 1 =', prettify(pm[84:116])
print 'Answer 1   =', prettify(pm[116:132])
print 'Question 2 =', prettify(pm[132:196])
print 'Answer 2   =', prettify(pm[196:260])

# 32..36
# 48..52
# 52..56
# 196..200

'''
# 4
f8 = struct.unpack('f', pm[8:12])[0]

f32 = struct.pack('f', f8 - 3.9604035e-11)
print f32.encode('hex')

f32 = struct.pack('f', 7.6956873e-30 / f8)
print f32.encode('hex')
'''

'''
# 19

f96 = struct.unpack('f', pm[96:100])[0]

f50 = struct.pack('f', 7.740607e31 - f96)
print f50.encode('hex')

f50 = struct.pack('f', 0.064559929 * f96)
print f50.encode('hex')
'''