cookies.txt      .scr

ただのテキストファイルのようだ

CTFZone 2019 Quals writeup - M394Dr1V3 cr4cKM3

TSGアドベントカレンダー 2019 3日目です。
adventar.org

こないだ11/30 18:00 JST - 12/2 06:00 JST、TSGでCTFZone 2019 Qualsに参加しました。
わりとみんなでまじめに参加して、結果はなんとか10位となりました。
アドベントカレンダー登録時の予定では、Web問あたりがいくつか解けて、ここでwriteupを書くはずだったんですが、かなりエスパー要素があるわ1問あたりの段階数がおおいやらで、全体的にいいところまでは進めても解ききれませんでした。悲しいね。全体的にこれ〇〇〇CONか?

初心に戻って唯一解けたRevering: M394Dr1V3 cr4cKM3のwriteupを書きます。

問題文

M394Dr1V3 cr4cKM3
REV / MEDIUM / 37 solves / 124 pts.

Hey, I've found this old crackme under the rug in the attic, could you solve it for me?
Don't forget to add ctfzone and curly braces before submitting flag (like ctfzone{FLAG_HERE}).
m394Dr1V3_cr4cKM3.zip

調査

まずfileを打ちます。Mega Drive*1

$ file m394Dr1V3_cr4cKM3.bin 
m394Dr1V3_cr4cKM3.bin: Sega Mega Drive / Genesis ROM image: "                " (GM 01234567-89, COPYLEFT CTFZONE)

そっかーっつってWindowsでMegaDriveのエミュレータ/デバッガを探してきます。
Exodusってやつを使いました。
アセンブリブレークポイントもついていて、メモリエディタも揃ってるのでとてもいい感じです。
ブレークポイントはプログラムカウンタの範囲によるものしかなさそうですが、まぁ逆アセンブラウィンドウのRun Toだけでかなり事足ります。
f:id:cookie-s:20191203032021p:plain

crackmeの問題自体は、矢印ボタンで16桁のパスワードを入力して、Aボタンを押すとパスワード判定が走るよくあるやつです。
パスワードの文字範囲は、矢印ボタンで選択可能な文字的に、文字コード0x30 - 0x5Aの範囲のようです。

Mega Driveの仕様については、Sega Retroとかいうサイトを参考にしました。特にメモリマッピングはとても大事です。

あとはGHIDRAでアセンブリ読解をします。GHIDRAの逆コンパイラはだいぶ参考にならなかった気がします。いや俺が悪いのか?きっとそうなんだろうな。
なんだかコード領域をデータ領域と誤解して、リファレンス解析とかにかなり失敗するのですが、たぶん最適ムーブは初心に戻ってstringsするところからです。

$ strings -tx m394Dr1V3_cr4cKM3.bin
...
  16153 Key is correct!
  16163 Incorrect key, please try again
...!

ということで016153をROMイメージから検索します。GHIDRAでMemory Search... アドレス0x0d21がヒットします。見事にGHIDRAはただのデータとして解析していますが、無理やりDでコード片として解析させます。
そして少し上の方にスクロールすると、すごーくパスワード判定ロジック的ななにかが見えます。
f:id:cookie-s:20191203033608p:plain
メモリの初期化をしておいて、ひたすらにmov, add, mul, lslなどで算術演算を行ったあとに、cmpとbranchを繰り返すあれです。
とてもじゃないが算術演算の回数が多すぎて人力でやれるものじゃないので、Z3の制約式に変換して解かせることにします。

みんな大好きZ3で解を出すために、制約生成器をRubyで書きました。入力はGHIDRAにでてくる逆アセンブル結果(gist: 03_input.diasasm)です。

メモリ初期化および最後の比較の場所は、大した量じゃないので手でRubyコードに埋め込みます。
算術演算を、ひたすらPythonに置換します。

newvは、こないだTSGゴルフ大会でunlambda生成器を作ったときに習得したidiomですが、手軽に連番を生成できて便利です。
このPython(gist: 02_constraints.py)を実行すると、めでたく解がでてきます。

矢印キー操作もかなりむずいので、雑にエミュレータのメモリエディタからRAM:0x000000に算出されたパスワードを書き込むと、めでたくフラグが出てきます。
f:id:cookie-s:20191203041031p:plain

*1:ちょっと僕の世代にはセガのハードの区別はつかないので、競技中はずっと脳内でどこかで見た「せがた三四郎」のCMの曲が流れてました。