wtfregexp
問題
BIG REGEXP IS HERE.
wtfregexp.pl.xz
メモ
解法
Perlプログラムは二行あり，1行目に長い正規表現，2行目にプログラムが書かれている。次のプログラム部分は次の通りで，
1 $ARGV[0] && ((unpack('B*', $ARGV[0]) . ',') x ((()= $RE =~ /(,)/g)+1)) =~ $RE && print "you got flag: $ARGV[0]\n";
ここで行われている処理は，コマンドライン引数に与えられた文字列を2進数で表記して，カンマで区切られた正規表現全てにマッチする時(正確には正規表現に含まれるカンマの数だけ入力文字列をカンマ区切りで増やしてマッチ)，フラグとして表示している。
カンマで区切られた正規表現は次のような形式しか無い
(?:[01]…[01](?:<0か1>[01]…[01]|[01]…[01]<0か1>)[01]…[01])
(?:[01]…[01])
二番目の式は無視してよく，一番目はつまり$x_i = a_1 \vee x_j = a_2$という形の制約である。 つまりこれは充足可能性問題なので，SATソルバに解かせることにした。
まず正規表現を整形しておく。
- カンマで区切って改行を入れる
- [01]を.に置き換える
% perl -pe 'm{qr/(.*)/}; $_ = $1; s/,|$/\n/g; s/\[01\]/./g' < wtfregexp.pl > reSATソルバに投入する。
1 from z3 import *
2 import re
3
4 def bin2str(b):
5 s = ""
6 for i in range(0, len(b) - 1, 8):
7 s += chr(int(b[i:i+8], 2))
8 return s
9
10 # setup SAT solver
11 bit = [Bool(i) for i in range(256)]
12 s = Solver()
13
14 # parse regex and add constraints to the solver
15 with open("re") as f:
16 for line in f:
17 match = re.search("^\(\?:(\.*)\(\?:(\d)\.+\|(\.+)(\d+)", line)
18 if match is None: continue
19 pos1 = len(match.group(1))
20 val1 = match.group(2) == "1"
21 pos2 = len(match.group(1))+len(match.group(3))
22 val2 = match.group(4) == "1"
23
24 s.add(Or(bit[pos1] == val1, bit[pos2] == val2))
25
26 s.check()
27 m = s.model()
28
29 binstr = ""
30 for i in range(256):
31 if is_true(m[bit[i]]):
32 binstr += "1"
33 else:
34 binstr += "0"
35
36 flag = bin2str(binstr)
37 print flag
% python solve.py ADCTF_l091C4L_r39Ul4r_3xpR3ss10N
