Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
beginners CTF 2018 crackme
#!/usr/bin/env python
from z3 import *
def main():
solver = Solver()
s = [BitVec('s_%d' % i, 8) for i in range(16)]
for i in range(len(s)):
solver.add(s[i] != 0)
solver.add(0x20 <= s[i], s[i] <= 0x7e)
val_x = 0xff
flag_list = [0x9c, 0x9e, 0x8c, 0x3e, 0x68, 0x64, 0x7b, 0x3f, 0x50, 0x63, 0x0a, 0x7f, 0x55, 0x73, 0x1e, 0x64]
for i in range(4):
flag1 = s[0 + i * 4] ^ val_x
solver.add(flag1 == flag_list[0 + i * 4])
val_x = val_x ^ 0x15
flag2 = s[1 + i * 4] ^ val_x
solver.add(flag2 == flag_list[1 + i * 4])
val_x = val_x | 0x20
flag3 = s[2 + i * 4] ^ val_x
solver.add(flag3 == flag_list[2 + i * 4])
val_x = val_x & 0xf
flag4 = s[3 + i * 4] ^ val_x
solver.add(flag4 == flag_list[3 + i * 4])
if solver.check() == sat:
m = solver.model()
print m
flag = ''
for i in s:
flag += chr(m[i].as_long())
print "\nflag: %s" % flag
else:
print "Not found."
if __name__ == '__main__':
main()
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.