Skip to content

Instantly share code, notes, and snippets.

@x0nu11byt3
Forked from LiveOverflow/fsec_solve.py
Created July 7, 2023 06:48
Show Gist options
  • Save x0nu11byt3/51f9f1d9f0da0f9677fc68aa4ba70769 to your computer and use it in GitHub Desktop.
Save x0nu11byt3/51f9f1d9f0da0f9677fc68aa4ba70769 to your computer and use it in GitHub Desktop.
Fsec2017 z3 solution
from z3 import *
import struct
# calculate e,f,d for a given input password
def calc(m):
e = 0
f = 0
d = 0
for i in xrange(0, len(m)):
c = ord(m[i])
e += c
f ^= c
d = (struct.unpack("i",struct.pack("I",(d << 0x5)&0xffffffff))[0] - d) + c;
return d,e,f
# try z3 for a given password length
def check(length):
print "Try to find a valid password for length: {}".format(length)
s = Solver()
# a character has to be one of: APSYD0GNIL1_
def is_valid(x):
return Or(
(x == ord('A')),
(x == ord('P')),
(x == ord('S')),
(x == ord('Y')),
(x == ord('D')),
(x == ord('0')),
(x == ord('G')),
(x == ord('N')),
(x == ord('I')),
(x == ord('L')),
(x == ord('1')),
(x == ord('_')))
# dynamically create a Bit vector for the password length
vec=""
for i in xrange(0,length):
vec += "pw[{}] ".format(i)
m = BitVecs(vec, 8)
# add the rules for the alphabet to each character
for i in xrange(0, length):
s.add(is_valid(m[i]))
# init e and f with 0
e=0
f=0
# perform the calculations that can be solved with z3
# d not included
for i in xrange(0, length):
e += m[i]
f ^= m[i]
# The extracted rules
s.add(e == 0x56a)
s.add(f == 0x28)
s.add(((BV2Int(m[0x1]) * BV2Int(m[0x2]) * BV2Int(m[0x3])) / 0x104) == 0x69b)
s.add(((BV2Int(m[0x4]) + BV2Int(m[0x5]) - BV2Int(m[0x6])) + BV2Int(m[0x7])) == 0x97)
s.add(m[0xd] == m[0xe])
s.add(m[0x2] == m[0x8])
s.add(m[0x7] == m[0xb])
# unecessary: s.add(m[0xc] == (length << 0x2))
# unecessary: s.add((m[0x0] - m[0x1]) == 0x4)
# explorative part. Set certain values by hand
s.add(m[0] == ord('P'))
s.add(m[1] == ord('L'))
s.add(m[2] == ord('A'))
s.add(m[3] == ord('Y'))
s.add(m[4] == ord('1'))
s.add(m[5] == ord('N'))
s.add(m[6] == ord('G'))
s.add(m[7] == ord('_'))
s.add(m[8] == ord('A'))
s.add(m[9] == ord('N'))
s.add(m[10] == ord('D'))
# check if there is a solution to those rules
while s.check() == z3.sat:
# get a model that satisfies the rules
model = s.model()
out = ""
nope = []
#print "\n#### Model ####"
for i in m:
if str(i):
out += chr(model[i].as_long()&0xff)
nope.append(i!=model[i])
# prevent this solution to come up again
s.add(Or(nope[:-1]))
# check if the password satisfies d
d,e,f = calc(out)
print length, out, hex(d),hex(e),hex(f), d ==-2098257644
if d==-2098257644 or d == 0xC177908A:
print out
exit()
print s.check()
for x in [17,19,20]:
check(x)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment