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 *
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