Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
PlaidCTF 2015 "RE GEX" solver
#!/usr/bin/env python
#
# PlaidCTF 2015 "RE GEX" solver
# @zxcvgm
#
from z3 import *
validchars = 'plaidctf'
flaglen = 171
def parse(pattern, bv):
pos = 0
i = 0
pattern_conditions = []
while i < len(pattern):
if pattern[i] == '.':
n = 0
if i + 1 >= len(pattern) or pattern[i+1] != '{':
i += 1
n = 1
else:
i += 2
n = ''
while pattern[i] != '}':
n += pattern[i]
i += 1
i += 1
n = int(n)
pos += n
elif pattern[i] == '[':
chars = ''
i += 1
while pattern[i] != ']':
chars += pattern[i]
i += 1
i += 1
char_class_cond = And(*[bv[pos] != validchars.find(c) for c in chars])
pattern_conditions.append(char_class_cond)
pos += 1
else:
assert False, 'unknown char %s at pos %d' % (pattern[i], i)
return pattern_conditions
# read patterns
f = open('regex_patterns.txt', 'rb')
patterns = [l.strip() for l in f]
f.close()
chars = [Int('c%d' % i) for i in xrange(flaglen)]
solver = Solver()
for c in chars:
solver.add(c >= 0)
solver.add(c < len(validchars))
all_conditions = []
for p in patterns:
pp = parse(p, chars)
all_conditions.append(Or(*pp))
solver.add(And(*all_conditions))
#print solver
assert solver.check() == sat
model = solver.model()
pattern_txt = ''.join(validchars[model[chars[i]].as_long()] for i in xrange(flaglen))
print pattern_txt
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment