Skip to content

Instantly share code, notes, and snippets.

@vitapluvia

vitapluvia/solve-laz3y.py

Created April 19, 2018 05:43
Show Gist options
  • Save vitapluvia/c1ba814c191e74bef9f3bab0e2096ca3 to your computer and use it in GitHub Desktop.
Save vitapluvia/c1ba814c191e74bef9f3bab0e2096ca3 to your computer and use it in GitHub Desktop.
Download ZIP
Solution for laz3y (350) - Byte Bandits CTF 2018
Raw
solve-laz3y.py
#!/usr/bin/env python
from z3 import *
''' JS Code =>
190 value[29] == "!" && //X// payload[29] = '!'
191 value[4] == value[8] && //X// 08 & 04 = '_'
192 value[17] == "_" && //X// payload[17] = '_'
193 value[4] == "_" && //X// payload[4] = '_'
194 leng(value) && //X// len(payload) == 30
195 crypto(value) && //X// payload[18:29] == 0bfuscati0n
196 value[10] == value[14] && // p[10] == p[14]
197 a(value) && // p[3] - p[0] == 32 && p[5] - p[12] == 71
198 b(value) && //X// p[12] == p[15] &&
199 //X// p[11] == "l" &&
200 //X// p[12] == "0" &&
201 //X// p[13] == "T" &&
202 //X// p[0] == p[13]
203 c(value) && // p[9] + p[6] - p[1] == 58;
204 d(value) && // (p[0] * p[1] * p[2] * p[3]) / 128 === 767949;
205 f(value)) { // (p[5] * p[6] * p[7]) / 25 === 35581;
'''
partial = 'T???_???_??l0T?0?_0bfuscati0n!'
s = Solver()
flag = [Int(i) for i in xrange(30)]
for x in range(0, 30):
s.add(flag[x] >= ord('!') and flag[x] <= ord('z'))
for x in range(len(partial)):
if partial[x] is not '?':
s.add(flag[x] == ord(partial[x]))
s.add(flag[10] == flag[14])
s.add(flag[3] - flag[0] == 32)
s.add(flag[5] - flag[12] == 71)
s.add(flag[9] + flag[6] - flag[1] == 58)
s.add((flag[0] * flag[1] * flag[2] * flag[3]) / 128 == 767949)
s.add((flag[5] * flag[6] * flag[7]) / 25 == 35581)
# fix errors:
s.add(flag[1] == ord('h'))
s.add(flag[9] != ord('/'))
s.add(flag[10] == ord('_'))
if s.check() == sat:
m = s.model()
print 'Flag{' + ''.join([chr(m[x].as_long()) for x in flag]) + '}'
else:
print 'Not Found.'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment