PlaidCTF 2015 "RE GEX" solver

re_gex_solver.py

#!/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