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 点数忘れた)
Backdoor CTF 2017 writeup
m1z0r3で出てました。2050点で21位、個人的には以下の6問を解きました。
ジャンルは適当につけて、実際に解いた順ではなくジャンルでソート。
・complex rsa (200, crypto)
・stereotypes (点数忘れた, crypto)
・imagerev (点数忘れた, crypto)
・baby-0x41414141 (150, pwn)
・just-do-it (250, pwn)
・funsignals (点数忘れた, pwn)
問題数が多いので雑にいきます。めんどくさいのでソルバも省略。
complex rsa
「RSAは破られることがあるらしいから2回も暗号化したったwww」みたいな問題文。
2つの公開鍵と暗号文が渡される。公開鍵のパラメータを見てみると、nの値が等しくeの値は異なる。RSA暗号の性質上、同じ法の元でe1,e2を用いて暗号化するということは、e = e1 × e2 % n を用いて暗号化したに等しい。
そこでeを計算してみるとそこそこ大きな値になるので、wiener's attackをして終了。
stereotypes
以下の3つのファイルが渡される
・plaintext:文末がちょっとだけ伏せられた平文
・ciphertext:暗号文
・pubkey:RSA公開鍵
明らかにstereotyped message attackなのでやるだけ。
imagerev
encrypt.pyを見ると読む気がなくなるほどめんどくさそう。
が、怪しげな数字のリストが目に付くのでググると、SHA256の実装っぽいことがわかる。つまり、画像のpixel毎にRGB値を SHA256(chr(R)+chr(G)+chr(B))としている暗号もどき。
通常ハッシュの逆算は不可能だが、今回は平文空間が256^3程度しかないので計算可能。予めテーブルを作っておき、暗号文を64バイトずつ切り出していけば平文が求まる。
あとは、全ピクセル数からいい感じの縦横比をguessして画像に起こせばフラグが書いてある。
baby-0x41414141
buf = read();
printf(buf);
exit();
という感じのプログラム。
ご丁寧にフラグ出力用の関数が用意されているので、書式文字列攻撃によってexitのGOTをフラグ出力関数に書き換えて終了。
フラグ出力関数がある問題が久々すぎて、どっかに/bin/sh用意してsystem呼んでってやろうとしてて30分くらい無駄にした。
just-do-it
自明なbofがあるので、writeへret2pltして適当にlibcのアドレスをリークさせた後、ret2libcでsystemを呼んでおしまい。
やるだけ。
funsignals
readを呼んだ後、読み込んだものを引数にsigreturnを呼ぶ。
sigreturnの引数は自由に操れるので、いわゆるSROPの簡単なバージョン。
フラグは実行ファイル中に書かれているので、sigreturnでwriteを呼べばフラグが出力される。
しばらくなぜかraxだけうまくセットされずに悩み、結局よくわからないところに積んだ値がraxになったのでそれで解いた。
まとめ
(有名どころと比べると)レベル感としては比較的易しめだった。24hで5人制限と考えればこんなものかも?
extend meも手をつけていたものの、ナンチャラアタックすらいらないとは思わなかった。とはいえlength extensionしても解けるはずなのに解けてなくてつらい...
ローカルでは解けたんや... リモートじゃ解けないけど...
あとがき
解いたけどwriteup書いてない問題が5問ぐらい溜まってるのでそのうち消化します
ASIS CTF Finals 2017 Mary Motion writeup
9/9~9/11に行われていたASIS CTFにソロ参戦していました。
といっても研究室の合宿中でほぼ時間がとれなかったので、Warm upを2問と一番簡単なpwnだけ解きました。
Mary Motion (pwn, 43pts)のwriteupだけ書きます。
Mary Motion
FSBのある関数とBoFのある関数をそれぞれ呼び出せるプログラム。
脆弱性は見ての通りなので、やるだけ問。
FSBでcanaryをleakし、BoFでret2pltをしてsystemを呼んでやる方針。
/bin/shの確保のためにいったんret2pltでreadして適当な所に置いてます。
まとめ
ただでさえ久しぶりのpwnで色々忘れてるのに、寝不足やら集中できない環境やらで1問解くのが精一杯だった。
pwnとcryptoは色々復習します。
Tokyo Westerns CTF 3rd 2017 writeup
最近全然記事書いてませんでしたが、久しぶりのwriteupです。
(研究やら他の趣味やらで単純にCTF以外のことを色々していたというだけ)
m1z0r3として参加して、479点で68位でした。
自分としては以下の4問を解き、204点を入れました。
・Palindromes Pairs - Coding Phase -(PPC/warmup, 24pts)
・My Simple Cipher (Crypto/warmup, 25pts)
・Baby DLP (Crypto, 64pts)
・Baby RSA (Crypto, 91pts)
それぞれのwriteupです。
Palindrome Pairs - Coding Phase -
単語がいくつか渡されて、それをくっつけて回文が何組作れるか?という問題。
pythonを使っているので、単語の組み合わせはitertoolsを使い、回文判定はスライス記法でやるだけ。
TWCTF{find_favorite_smell}
My Simple Cipher
オレオレ暗号っぽいもの(名前とかあるのかはよくわからない)
フラグの先頭が「TWCTF{」で始まることから逆算するとkeyの頭6文字がわかる。
更に、暗号文の最後の方はフラグが使われておらず、keyとkeyから暗号文が作られているので残りのkeyも逆算可能。
TWCTF{Crypto-is-fun!}
Baby DLP
こちらから数を送ると、が返ってくるシステム。
ここで、0と1を送った場合を考える。
・0を送った場合
返ってくるのは、
・1を送った場合
mの最下位ビットが0のとき、
mの最下位ビットが1のとき、
となる。
したがって、この関係性を見ることでmの最下位ビットを推測することができる。
同様にして、最下位ビットだけでなく各ビットについても求めていくことができる。
一種のLSB oracle Attack?
TWCTF{0f97c1c3ac2aedbd7fb8cd39d50f2b561d31f770}
Baby RSA
となっているRSA暗号。
まず結論だけ言うと、19*n をフェルマー法で素因数分解するだけで解けたらしい。
そんなことには気づかずに頑張って解いたので、せっかくなのでその方法を載せておきます。
素数p, q を以下のように表す。
ここで、qがだいたいpの19倍ぐらいという考えから以下のように置き換え。
ただし
さてこのとき、
であるため、pを変数とした二次方程式として見ることができる。これをpについて解くと、
となる。なおpは必ず正なので√の係数が負の場合は省略した。
つまり、このような整数pが求まるxを総当たりで探せば良いことに帰着する。
しかし、であり、rは512ビットの範囲であるため愚直にxを総当たりしても探しきれない。そこで、平方数判定は容易に行えることを利用して以下のように解いた。
・を超えるギリギリの整数を探す。(rnと置く)
・rnを1ずつ増やしつつ、が平方数となっているか確認
・平方数となっている場合xが求まるので、pが計算可能か確認
nが2052ビットであり、はせいぜい1024ビットであることを考えると、rnのスタートさえしっかりしていれば大した回数は試行せずとも当たるはずである。
rnのスタートについては、以下のような愚直な方法で計算した。
・76nは10進で619桁なので、まずはとする
・1~9について、rn*iが76nを超えない限界を探し、と更新
・同様に1桁ずつ下げていきながら76nを超えない限界を求めていく
このようにして求めたrnを元に先の方法を試したところ、1足しただけですぐに答えが求まった。
TWCTF{secretly_cherry-blossom-viewing}
まとめ
Babyは全然Babyじゃなかった。
pwnはswapやsimple noteもちょろっと見たものの、全然解けなかったので解けるようになりたい。
あと、The Worstはおそらくやることは合ってるはずなんだけどglibcのバージョンが違うのかなんなのか、たぶんrandの出力結果が正しいものが得られてない気がして解けてないのでつらい。
WhiteHat Contest 13 writeup
個人で参加してました。2問解いて300pt、48位くらい(忘れた)でした。
なお、開催時間を48時間と勘違いして終了20分後くらいに3問目をsubmitしました。
あと、説明を全然読んでなかったのでフラグ形式がわからずしばらく悪戦苦闘してました。
解いた3問のwriteupを書きます。
・Mui Ne (pwn 100)
・DaNang (crypto 200)
・Cat Ba island (crypto 200)
Mui Ne (pwn 100)
入力したものをそのまま出力して終了というプログラム。
NX, canaryが有効。
問題文に書いてある通り、FSBが存在します。また、入力をgetsで受け付けているためBoFも存在します。
以下解いた流れ
その1.
まず、1回の入出力では足りないのでmain関数をループさせることを考えます。
mainからのリターンアドレス書き換えが真っ先に思いつきますが、canaryが有効な上に、下のようなよくわからない処理(espのすり替え)をしていてスタックのアドレスがわからないとうまくEIPをとれません。
leave
lea esp, [ecx-0x4]
ret
そこで、FSBによりスタックのアドレスをリークしつつ、__stack_chk_failのgotを上書きしてmainに飛ばしてやります。これにより、適当にBoFするだけでmain関数がループするようになります。
その2.
スタックのアドレスがわかったので、BoFによりmainからのリターンアドレスをうまく書き換えてEIPを奪います。
ちなみに、EIPを奪うときに__stack_chk_failが邪魔になってくるので、再びgotを書き換えてどこかのretに飛ばすことでスルーしてます。
その3.
EIPが奪えたら、あとはシェルをとるだけになります。
今回はlibcが与えられていないので、return to dl-resolveを目指します。
32bitなので、ももテクの記事を参考にstack pivotしてからreturn to dl-resolveして終わり。
flag:WhiteHat{196841c60f4408dd151af3ce7f4dc84f9583cc7a}
DaNang (crypto 200)
encryptというテキストファイルと、makefile.pycが与えられます。
pycは人間には読めないので、easy_python_decompilerでデコンパイルします。
すると、encryptの中身は以下のようになっていることがわかります。
まず、m1,m2がわかれば Common Modulus Attackによりflagがわかりそうなことが自明です。なのでm1(m2)をどうにかして求めることを考えます。
c1,c2を見てみると、平文が44444違うだけの関係であることが見てとれます。
つまり、
という関係の2つの暗号文から平文を求める必要があります。
これは、Franklin-Reiter Related Message Attack により求めることができます。
まとめると、
・Related Message Attack により m1, m2 を求める
・Common Modulus Attack により flag を求める
flag:WhiteHat{4111c011bc640806ef98a32a5caaf9d169a960a0}
Cat Ba island (crypto 200)
どうにかして500億手に入れる問題。 今流行りの5000兆円じゃなくてよかった。
なお、moneyなのかただの数値なのか混同しそうなのでwriteup中ではmoneyの単位を円として書きます。
選べるコマンドは2つで、
1: Get secret code : ランダムな秘密鍵、IVを元にしたCBCモードのAESオブジェクトを作成し、queryという文を暗号化する。 IVのみプレイヤーに対して知らされる。
2: Get money : プレイヤーが送信したIVによって1で作成した暗号文を復号する。このとき、平文に数字が含まれていればその分のmoneyが手に入る。 厳密に言えば正規表現でマッチした最初の部分を手に入れるので、xxx5xxx3xxx みたいに復号されたら5円が手に入る、はず。
これらのコマンドを選びつつ、50回以内に目標金額を貯めるゲーム。
IVをいい感じにいじってどうにかする問題ということは漠然と考えるものの、よくわからないのでまずはIVをそのまま送って復号を繰り返します。すると、必ず1円手に入ることがわかります。つまり元の平文のどこかに必ず1があるということなので、何文字目にあるのかを知りたくなります。
やり方としては、IVのnバイト目を IVn xor 0x31 xor 0x39 として送ります。
結局下位4bitだけが変化するわけですが、元の平文が1のバイトであれば0x39となるので復号結果が9になります。
一方、元の平文が1でない、つまり数字にならない箇所では、下位4bitだけが変化しても数字になることはありません。(asciiで数字の範囲は0x30~0x39なので)
この方法で確かめると、必ず6バイト目に1が来ることがわかります。
なので、この6バイト目を基準に前後1バイトずつを数字になるようにIVをいじっていきます。
数字でないということは、平文の該当バイトの上位4bitが0x3ではない・0x3a~0x3fのいずれかということになります。したがって、IVの該当バイトの上位4bitをいじってみて数字になればok、ならなければ下4bitを調整した上で再び上位4bitをいじる、ということをしてやれば1桁ずつ増やすことができます。
これを、6バイト目を基準に前後1バイトずつ順番に増やしていき、11桁くらいになれば目標金額に届きます。
あとは、なるべく試行回数が少なくなるようにPPCをして終わり。
ちなみに、桁を増やそうと適当にやってると0円を獲得することがあるので、ソルバのleft_flagとかはそれを回避して逆からループを回してるだけです。(平文が制御文字になってる?)
ひたすら読みにくいだけのソルバだけど、2回くらいまわしてたら目標金額達成しました。
flag:WhiteHat{13643c9b5ceece81bd5a6f9b2f8813e4d7b6dab1}
所感
各問題1行感想
・Mui Ne:他の人のwriteupみたらふつうにsystem呼んでた。つらい。
・Da Nang:申し訳程度のrev要素と50点くらいのcrypto
・Cat Ba island:PPC 200
完全に時間を勘違いしていたので、適当に他の問題もこれから見ていきたいなぁという感じです。
あと、昔にstack pivot + return to dl-resolveやったときにbss領域の上のほうにpivotしすぎて死んでたのに今回もやらかした。