katagaitaiCTF#6 関西easyに参加しました

本日（08月13日）に大阪で開催されたkatagaitai CTF勉強会(easy)に参加してきました。

内容は午前はWeb, 午後はReversingでした。WebはHack.lu CTF 2014のHotCows Datingという問題で、ReversingはCSAW CTF 2013のcrackmeという問題をそれぞれ解きました。正直Webの方はBurpの設定が上手くいかずにあまり付いていけませんでした。一応フラグは取得できたもののイマイチ「なんで？」というところが多いので、今回はcrackmeの方を中心にWriteUpを書こうと思います。

crackmeは32bitのLinux用バイナリで、とりあえずWindowsを起動してIDA Pro Freeで解析を開始しました。bindやaccpetなどから単体でサーバーとして動作するプログラムだと分かったので、とりあえずポート番号だけメモして動作しました。crackmeへ接続すると、パスフレーズを聞かれます。パスワードが合っていないと終了してしまいます。あまりIDAを使ったことの無い私は文字列検索で文字列を送信(表示)している部分を見つけ、その周辺から解析を始めました。その結果、明らかに分岐している部分があったので、その上の関数にverifyという名前を付けて関数を見ます。ちょっと前に変数名とコメントを付ける機能を知ってからはじゃんじゃん使ってるので解説が始まる前には解析が終わってたと思います。verify関数(仮)をC言語にすると次のようになりました。

int verify(char* input)
{
  char chr = input[0];
  int hash = 0x539;
  char *pass = input;
  int tmp;
 
  for(; *pass != 0; pass++) {
    tmp = chr + (hash << 5);
    chr = *(pass + 1);
    hash += tmp;
  }
 
  return hash;
}

あらためて見るといかにC言語が苦手かが分かります......
さて、とりあえず自分で解こうと思って6桁くらいまでのブルートフォースを書きましたが一向に終わらないので別の方針を立てることにしました。
そこで、入力を「A」「AA」「AAA」「AAAA」...のように試すと、徐々にハッシュ値が増加していることが分かりました。(4バイトを超えたらまた小さくなる感じでした。)
入力が長く、ASCII値が大きいほどハッシュ値も大きくなるので、二分探索(手動)で0xEF2E3558に徐々に近づけていきました。(でも5分程度で下2桁以外は揃いました。)
6桁でハッシュ値が答えに近づき、最後の方は揃わなそうだったので、最後の1文字だけブルートフォースアタックしました。その結果「aSA6>6」で通りそうだったので送ったらフラグが表示されました。

勉強会が終わった今では頭の悪い解き方です。はい。

ということで、勉強会ではkleeとz3pyを使う方法をやったので、その内勉強会中ずっとやってたz3による解法についてもWriteUpします。z3pyは条件式に当てはまるような入力を見つけてくれるモジュールです。文字列を探す方法は分からなかったのでIntVectorでやってましたが実行できず。スライドを読むとBitVecなら上手くいくそうなので時間がかかりましたが書いてみました。

	# coding: utf-8
	from z3 import *
	s = Solver()
	LENGTH = 6
	# 6文字のテキスト
	text = [BitVec('text[{0}]'.format(i), 32) for i in range(LENGTH)]
	# 全て印字可能文字
	for i in range(LENGTH):
	s.add(32 <= text[i], text[i] <= 126)
	# ハッシュ
	ret = [BitVec('ret[{0}]'.format(i), 32) for i in range(LENGTH + 1)]
	ret[0] = 0x539 # 初期値
	for i in range(LENGTH):
	ret[i+1] = ret[i] + (ret[i] << 5) + text[i]
	# 結果が等しい
	s.add(ret[LENGTH] == 0xef2e3558)
	# 確認
	t = s.check()
	if t == sat:
	m = s.model()
	passcode = ""
	for i in range(LENGTH):
	passcode += chr(m[text[i]].as_long())
	print("RESULT : {0}".format(passcode))
	else:
	print(t)

view raw z3solve_crackme.py hosted with ❤ by GitHub

実行すると入力条件に当てはまるような文字列を見つけて表示してくれます。講師の方の書かれたコードでは40秒程度かかりましたが、このコードでは1秒前後で実行できました。私は講師の方のコードをリストにして初期化に入力、hashともにBitVecを使っただけなのですが、なぜここまで違いが出たのかは全く分かりません......

easyとはいえ、今回の勉強会を通して知らなかったことをたくさん学ぶことができたので、大変有意義な1日でした。主催者やNRI Secureの皆様、ありがとうございます！次のmedも参加する予定なのでよろしくお願いします。