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