PlaidCTF 2015 "RE GEX" solver
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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