<<EnableMathJax(doller)>>
= wtfregexp =
== 問題 ==
BIG REGEXP IS HERE.

wtfregexp.pl.xz

== メモ ==

== 解法 ==
Perlプログラムは二行あり，1行目に長い正規表現，2行目にプログラムが書かれている。次のプログラム部分は次の通りで，
{{{#!highlight perl
$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$という形の制約である。
つまりこれは充足可能性問題である。特に2-SATなので高速に解くことが出来る。SATソルバに解かせることにした。

まず正規表現を整形しておく。
 * カンマで区切って改行を入れる
 * [01]を.に置き換える
{{{
% perl -pe 'm{qr/(.*)/}; $_ = $1; s/,|$/\n/g; s/\[01\]/./g' < wtfregexp.pl > re
}}}

SATソルバに投入する。
{{{#!highlight python
from z3 import *
import re

def bin2str(b):
    s = ""
    for i in range(0, len(b) - 1, 8):
        s += chr(int(b[i:i+8], 2))
    return s

# setup SAT solver
bit = [Bool(i) for i in range(256)]
s = Solver()

# parse regex and add constraints to the solver
with open("re") as f:
    for line in f:
        match = re.search("^\(\?:(\.*)\(\?:(\d)\.+\|(\.+)(\d+)", line)
        if match is None: continue
        pos1 = len(match.group(1))
        val1 = match.group(2) == "1"
        pos2 = len(match.group(1))+len(match.group(3))
        val2 = match.group(4) == "1"
        
        s.add(Or(bit[pos1] == val1, bit[pos2] == val2))

s.check()
m = s.model()

binstr = ""
for i in range(256):
    if is_true(m[bit[i]]):
        binstr += "1"
    else:
        binstr += "0"

flag = bin2str(binstr)
print flag
}}}
{{{
% python solve.py     
ADCTF_l091C4L_r39Ul4r_3xpR3ss10N
}}}