#!/usr/bin/env python | |
# | |
# PlaidCTF 2015 "RE GEX" solver | |
# @zxcvgm | |
# | |
from z3 import * | |
def bitpos(pos): return (170 - pos) * 3 | |
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 >> bitpos(pos) & 7) != 'plaidctf'.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() | |
bv = BitVec('pattern', 171 * 3) | |
solver = Solver() | |
all_conditions = [] | |
for p in patterns: | |
pp = parse(p, bv) | |
all_conditions.append(Or(*pp)) | |
solver.add(And(*all_conditions)) | |
#print solver | |
assert solver.check() == sat | |
pattern = solver.model()[bv].as_long() | |
pattern_txt = ''.join('plaidctf'[pattern >> bitpos(i) & 7] for i in xrange(171)) | |
print pattern_txt |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment