ログイン
編集不可のページディスカッション情報添付ファイル
ytoku/CTF/Writeup/AdventCalendarCTF2014/2014-12-22

MMA

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進数で表記して,カンマで区切られた正規表現全てにマッチする時(正確には正規表現に含まれるカンマの数だけ入力文字列をカンマ区切りで増やしてマッチ),フラグとして表示している。

カンマで区切られた正規表現は次のような形式しか無い

二番目の式は無視してよく,一番目はつまり$x_i = a_1 \vee x_j = a_2$という形の制約である。 つまりこれは充足可能性問題である。特に2-SATなので高速に解くことが出来る。SATソルバに解かせることにした。

まず正規表現を整形しておく。

% perl -pe 'm{qr/(.*)/}; $_ = $1; s/,|$/\n/g; s/\[01\]/./g' < wtfregexp.pl > re

SATソルバに投入する。

   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

ytoku/CTF/Writeup/AdventCalendarCTF2014/2014-12-22 (最終更新日時 2014-12-25 09:07:01 更新者 ytoku)