z3 を使ってみる
SAT/SMTソルバであるz3を使ってCTFの問題を解いてみた、という記事。
m1z0r3内の勉強会でz3を取り扱ったものの、途中で資料作るのがめんどくさくなって問題の解説を放棄してたのでその分ここでwriteupを書きます。
z3pyは導入済みで、大まかな扱い方はわかっているという前提で行きます。
今回扱う問題は以下の4問
- HackIt 2017：crypto 150
- CSAW CTF 2017：Another Xor (crypto 100)
- CSAW CTF 2017：Almost Xor (crypto 200)
- D-CTF 2017：Forgot my Key (misc 点数忘れた)
HackIT 2017 crypto 150
フラグ形式は、flag{...}となっている。
また、平文は Hello, Alice! ではじまる。
encrypt関数では、「平文のi文字目の最上位bitから順にとったビットと、lfsrの最下位bitから順にとったビットのxorをとっていく」ただし、lfsrの最下位bitによってはpolyを用いてlfsrを更新する。
という文字に起こすとなんともよくわからない感じになる処理をしている。
しかしよく読むと、暗号化と言えどxorをとっているだけ。さらに平文の出だしが与えられているため、xorをとるとlsbがわかる。lsbがわかるということはlfsrやpolyの一部がわかっていくことになる。
したがって、z3に投げてやれば解けそうなことがわかる。
わざわざ暗号文を変数として宣言して制約を追加しているが、練習用につけたようなものなので無くても解けるはず。
- CTF（crypto）でz3を使うときの変数はビットベクトルでだいたいOK
- z3で解を求めるまでの流れ
が理解できればok。また、ビットベクトルは符号付きなので符号無し右シフトするときはLShRを使いましょうというのがこの問題から得られる知見。
CSAW CTF 2017 Another Xor
フラグ形式は flag{...}
plaintext = flag || key || md5
となっている。ただし || は連接を表す。この plaintext と、key を plaintext 長だけ繰り返したものの xor をとった暗号。
まずはじめに、key の長さを考える。flag が n 文字、key が m 文字だと仮定する。
すると、flag 部分と xor を取り終わった時点での key は、n%m 文字目となっている。
続いて plaintext の key 部分と、先ほどの続きの key の xor をとっていく。このとき、plaintext の方は key が一周するが、xor をとる方の key もちょうど一周することに注目する。具体的には、n%m + 1文字目から xor をとっていき、途中で頭に戻ったあとn%m文字目まで続いていく。
つまり、key 同士の xor をとっている部分の暗号は以下のようになる。
key[0] xor key[n%m] = c[x]
key[1] xor key[n%m+1] = c[x+1]
⋮
key[i] xor key[m-1] = c[x+i]
key[i+1] xor key[0] = c[x+i+1]
⋮
key[m-1] xor key[n%m-1] = c[x+m-1]
さて、ここで c[x] xor c[x+1] xor ... xor c[x+m-1] を考える。
すると、key の各文字について2回ずつ xor をとることと等しくなり、0 となる。
以上より、暗号文から md5 分を取り除いた後、後ろから1文字ずつ xor をとっていき 0 になったときの文字数が key の長さとなる。
key の長さがわかったら、後は z3 に投げるだけ。
この問題の z3 部分は割と単純。
8bit 幅のビットベクトルを文字数分宣言して、printable な範囲に制約をつけ、フラグの頭はわかっているため制約をつけ、xor をするだけ。
解の取り出し方部分（get_result）については katagaitai 勉強会 #9 に出たときにいただいた、bataさんのソルバから引っ張ってきています。
CSAW CTF 2017 Almost Xor
フラグ形式は flag{...}
先ほどの Another Xor の高難易度版。
一見複雑そうな処理をしているものの、追っていくと実は単純。
平文長だけ鍵を繰り返し、平文も鍵もそれぞれn文字の倍数長にパディング。
後は双方からnビットずつ取り出して足していくだけ。
と、これだけの処理。なお足した後はnビットでマスクするため暗号文の長さはパディング後の平文と同じ。
ちなみに、CSAW CTF当日中はここまで理解した後、問題で渡されたファイルをそのまま使ってz3につっこもうと色々やってたものの、この程度の処理なら自分で書き直したほうが早かった。
nの候補として1,2,3,4,6のみを使っているのは、平文の文字数がnの倍数であることがわかるため。仮にnの倍数でない場合、パディングによりヌルバイトが平文、鍵双方につけられるため、暗号化後もヌルバイトとなる。しかし、今回の暗号文にはそれがないためnの倍数長であったとわかる。
nビットだけ取り出す方法についての知見が得られた。
D-CTF 2017 Forgot my Key
cryptoというジャンルが無く、miscとして出された問題。
フラグ形式は、DCTF{sha256}
問題を見ると、PHPで書かれた処理と暗号文がある。（PHPを知らなくても、関数をググってればすぐにたどり着く）
DCTF{sha256}|md5 という平文に対して、適当な初期値とmd5値を使って暗号化がされていく。また注意が必要な点として、unpackのフォーマットがh*となっている。
これにより、0x12→21とunpackされる。
sha256やmd5であることから諸々の文字数は判明しており、暗号文の1文字目から初期値もわかる。
以上のことを踏まえると、後はz3に投げて解くだけとなる。
今回はハッシュ値の部分の制約を0-9a-fとしている。
また、ビットクトルで剰余をとるときにはURemという関数を使わないとうまく計算できない。
その際にZeroExtという関数を使っているが、これはビットベクトルを1bitゼロ拡張している。足した際にオーバーフローしてしまうことをこれにより防いでいる。
はじめから9bitのビットベクトルを宣言してもいいが、なんとなく気持ち悪いのでこうした。
実際にゴリゴリ書いて使えるかは別にしても、z3がどんな問題に対して使えるのかを知っておくことは大事。z3に投げれば解ける（手動だとありえん時間がかかる）問題に対面したときに無駄に時間を溶かしてしまうかそうでないかは成績に直結するので。
と感じました。
