Skip to content

Instantly share code, notes, and snippets.

@ShikChen
Created April 20, 2015 08:46
Show Gist options
  • Save ShikChen/9b263d0dd17a19d223a4 to your computer and use it in GitHub Desktop.
Save ShikChen/9b263d0dd17a19d223a4 to your computer and use it in GitHub Desktop.
PlaidCTF 2015 REG EX
import itertools
import re
import z3
base = 'plaidctf'
r = open('regex_57f2cf49f6a354b4e8896c57a4e3c973.txt').read().strip()
s = re.search(r'\((.*)\)', r).group(1)
s = s.split('|')[3:]
s = [re.findall(r'(.*?)\[(.*?)\]', it) for it in s]
solver = z3.Solver()
sol = z3.Array('sol', z3.IntSort(), z3.BoolSort())
for x in s:
pos = 0
rule = []
for a, b in x:
m = re.match(r'\.{(\d+)}', a)
if m:
pos += int(m.group(1))
else:
pos += len(a)
b = [base.index(it) for it in b]
b = [bin(it)[2:].rjust(3, '0') for it in b]
b = zip(*b)
for j, y in enumerate(b):
y = [it == '1' for it in y]
var = sol[pos * 3 + j]
if all(it == True for it in y):
rule.append(var)
elif all(it == False for it in y):
rule.append(z3.Not(var))
pos += 1
solver.add(z3.Or(*rule))
print solver.sexpr()
print solver.check()
sol = solver.model()[sol].as_list()[:-1]
sol = [a.as_long() for a, b in sol if z3.is_true(b)]
val = [0] * 171
for i in sol:
val[i / 3] |= 1 << (i % 3)
for per in itertools.permutations(base):
s = ''.join(per[it] for it in val)
if re.match(r, s) is None:
print s
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment