Skip to content

Instantly share code, notes, and snippets.

@expend20 expend20/s.py
Created Jul 31, 2019

Embed
What would you like to do?
#FlareOn5 12
#!/usr/bin/env python
from itertools import chain, product
import string
from z3 import *
suffix = '@flare-on.com'
stored = [0xfc7f, 0xf30f, 0xf361, 0xf151, 0xf886, 0xf3d1, 0xdb57, 0xd9d5, 0xe26e, 0xf8cd, 0xf969, 0xd90c, 0xf821, 0xf181, 0xf85f]
c_add = [[],
[10, 15],
[9, 14],
[9, 14, 10, 15],
[8, 13],
[8, 13, 10, 15],
[8, 13, 9, 14,],
[8, 13, 9, 14, 10, 15],
[7, 12],
[7, 12, 10, 15],
[7, 12, 9, 14],
[7, 12, 9, 14, 10, 15],
[7, 12, 8, 13],
[7, 12, 8, 13, 10, 15],
[7, 12, 8, 13, 9, 14]]
LEN = 30
x = [BitVec("x%d"%i, 32) for i in range(0, LEN)]
sum1 = BitVecVal(0, 32)
diff = BitVecVal(0, 32)
s = Solver()
for i in range(0, len(x)):
s.add(x[i] >= 0x21, x[i] <= 0x7a)
for i in range(0, LEN - len(suffix)):
diff -= 0xc00
sum1 += x[i]
j = i + 1
sum1 -= diff
sum1 &= 0xffff
sl = len(suffix)
for i in range(j+1, sl):
s.add(x[j + 1 + i] == ord(suffix[i]))
for i in range(0, int(len(x) / 2)):
xcurr = ((x[i*2 + 1] - 0x20) << 7) + (x[i*2 + 0]) - 0x20
if not i:
xprev = xcurr
else:
for ii in range(0, 16):
xcurr = xcurr * 2 + 1
xprev = (xprev * 2)
is_h = 0
if ii in c_add[i]:
is_h = 1
xprev += (((xcurr) >> 16) ^ is_h)
xprev &= 0xffff
xcurr &= 0xffff
s.add((xprev + sum1) & 0xffff == stored[i])
if(s.check() == sat):
m = s.model()
pr = ''
for i in range(0, len(x)):
try:
pr += chr(int(str(m[x[i]])))
except ValueError:
pr = '<unprintable>'
break
print(pr)
else:
print("unsat")
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.