はじめに
picoCTF2018のWrite-Upです。僕は生活習慣崩壊ズとして参加し、33問解いて9325点取りました。チームとしては29935点で総合順位は44位でした。アメリカの高校生換算だと13位みたいです。嬉しい。(10位までが賞金です)
アメリカの高校生換算で13位相当だった pic.twitter.com/3vK7QCetVr
— 漁師 (@6Lgug) October 22, 2018
解いた問題が結構多くなってしまったので、解説が数行で終わってしまうような問題は別記事に分けました。
それでは、各問題について書いていきます。
- はじめに
- script me
- circuit123
- Help Me Reset 2
- fancy-alive-monitoring
- roulette
- Ext Super Magic
- Flaskcards Skeleton Key
- SpyFi
- eleCTRic
- James Brahm Returns
- 感想
script me
- genre : General Skills
- point : 500
括弧列が与えられるので、その生成規則を考えて問題を解けという問題。与えられる生成規則はこちら : script me
まずこの括弧列(?)の生成規則について考えました。いろいろと睨みながら考えていましたが、括弧列の深さが深い方に浅い方が取り込まれる、同じであれば連結という結論に至りました。(データ構造をマージする一般的なテク)
また、競プロのように計算量を改善しなくてもいい程度の量なので、併合の都度深さを計算し直しても恐らく問題ないです。なので、適当に実装していい感じにしました。
コードです。(これはその時書いたコードをなくしてしまったため、再現です)
circuit123
- genre : Reversing
- point : 800
暗号とデコーダのソースが与えられるので、デコードしなさいという問題。与えられるファイル群はこちら : circuit123
Keyを2進数にしたものの各bitを変数とし、それにXorやらOrやらを演算して新しい変数を作り、その変数に対してさらに演算をし…と繰り返し、一つの変数に纏めます。その変数がFalseになるような数字がkeyになります。
まずKeyは128bitなので、全探索は無理です。一応DAGなので、制約を辿っていい感じにするものも書けそうでしたが、相当辛いと感じたのでやめました。
ヒントにHave you heard of z3?とあったので、Z3でググりました。どうやら制約を指定するとそれを満たす変数を調べてもらうことができる便利ライブラリ(SATソルバ)みたいです。
コードでXorやOrの演算をしているところをそのまま制約と見て、チェッカを改変してあげることでZ3に突っ込めるコードを出力させてあげることにしました。出たコードを実行すると見事に出てくれたので、後はそれを適当に整形するスクリプトを書きました。
以下がZ3コードを出すコードです。これもその時使ったコードをなくしてしまったので再現です。
出力されたZ3コード、その出力のパースに使ったC#コード、その出力のデコードに使ったPythonコードは別のGistに置きました。(とても長いため)
Help Me Reset 2
- genre : Web Exploitation
- point : 600
むちゃくちゃ怪しい解法で通しました。多分非想定解です。
① Help Me Resetを解く。なんと、この問題は途中で消失してしまった(期間限定)。
② Help Me Resetの回答URLを履歴から見つけてくる。
③ 2でも同じところにアクセスする。
④ フラグがある。
前作のセーブデータがあったらボーナスが貰えるゲームっぽい(小並感)
fancy-alive-monitoring
- genre : Web Exploitation
- point : 400
IPアドレスを入力して、それにpingを送るプログラムです。入力チェックはクライアントとサーバー双方にありましたが、クライアント側は適当に改変できるのでサーバーのみのソースを置きます。 : source
サーバー側のチェックを見てみます。URLの正規表現は以下 :
^(([1-9]?[0-9]|1[0-9]{2}|2[0-4][0-9]|25[0-5]).){3}([1-9]?[0-9]|1[0-9]{2}|2[0-4][0-9]|25[0-5])
とても長くて見えにくいですが、([1-9]?[0-9]|1[0-9]{2}|2[0-4][0-9]|25[0-5])部分は0-255までの数字かどうかのチェックです。この部分を[0-255]と表すことすると、これは^([0-255].){3}[0-255]となります。
この正規表現に気になる部分な二箇所あります。一箇所目はドットのエスケープが抜けているので、ドットの部分に任意の文字を挿入できるということ、もう一つは正規表現に終端チェック($)がないので、後ろに任意の文字列を繋げられるということです。
通ったIPはexec('ping -c 1 '.$ip, $cmd_result);のようにコマンドに埋め込まれて実行されているので、後ろに任意の文字列を繋げられるということは&などで別タスクとして任意のコマンドを実行できるということです。また、ipアドレス部分も1a1a1a1等にできるので、pingを送る長い処理を待つことなく迅速にコマンドを実行できます。
このプログラムではコマンドの出力に特定の文字列が含まれているかどうかで二択の出力を返しています。条件を満たしていたら特定の出力を出す、そうでなければ出さないという具合にすると出力にtrue/falseを出せます。なので、二分探索的にコマンドの出力を推測できることになります。(今回は実装が大変だったので二分探索などは行いませんでした。)
ソルバは以下 :
(合わなかったので、漁師がドットをアンダーバーに置換して通しました。)
roulette
- genre : General Skills
- point : 350
問題のソースはこちら: roulette.c
この問題は2つの脆弱な箇所を見つける必要がありました。チームメイトがどちらも見つけ、僕はそれを実装する形になりました。ぞへが乱数の脆弱性、漁師がオーバーフローの脆弱性を見つけましたが、僕は乱数の脆弱性の方しか理解できていません。なので、本稿では乱数の脆弱性についてのみ触れます。
乱数を初期化しているシードが金額の初期値として与えられているので、シードは分かります。シードが分かれば次からの乱数をすべて予測できるので、次からルーレットを当てる/外すは自由となります。
オーバーフローの脆弱性は特定の数字を入れるとそれがマイナスとして扱われるようです。このマイナスをbetした状態で負けると当然金額も増えるので、負けて増やすことができます。
なぜどちらの脆弱性も必要かと言うと、クリア条件が「特定の回数以上勝った状態で、とても多い金額に到達する」であるからです。乱数のみならば目標金額に到達せず、オーバーフローのみなら勝ちを引けません。
実装は、問題のプログラムのソースに「シードを任意でセットする」と「入力に関わらず常に勝ちにする」という実装を加えただけなので省略します。
これは余談ですが、脆弱性を後から見つけた漁師はその時学校で、乱数を見つけたぞへは睡眠中(?)だったので僕が実装することになりました。なんで正午なのに寝てるんですか?
Ext Super Magic
- genre : Forensics
- point : 250
ファイルが与えられます。シグネチャを見るとディスクイメージだとわかるので、マウントしようとしましたができません。
何処かが壊れてるんだろうなあと思ったので、とりあえず同じサイズでディスクイメージを作成してヘッダ部分をコピペしてあげました。そうすると動いたみたいです。それっぽいjpgイメージがあると漁師が言っていたので探しました。あったので引っ張ってきたらフラグがありました。
Flaskcards Skeleton Key
- genre : Web Exploitation
- point : 600
問題文でSecret_key: a7a8342f9b41fcb062b13dd1167785f8なる"Secret_key"が与えられています。adminを取ると勝ちです。
漁師によると、FlaskというPythonによるWebフレームワークがあり、与えられたSecret_keyはこれのcookieの正当性チェックに用いられるkeyのようです。この問題もFlaskで動いているので、このkeyがあればcookieを偽装することが可能だということです。
これのsession-cookieは、eyJfZnJlc2giOmZhbHNlLCJ1c2VyX2lkIjoiOSJ9.DqGfag.grYAqLOASF2MpQmJXT8V4wDZ7SQという感じで入っています。これはbase64.time.hashという形で、base64が読みたい内容、dateはcookieの日時(2000-01-01からの経過時間)、hashが正当性チェック用のhashです。これが偽装できれば任意のユーザーでログインできます。
base64をデコードしてみると、{"_fresh":false,"user_id":"9"}という形になっています。_freshはよくわからないがfalseで固定のようで、user_idがユーザーID(連番)であると思われます。Adminは恐らく0か1なので、ここが0か1になっているCookieを生成したいです。
あとは単純にサーバーの動きをこちらでも実装してあれげばいいので、flaskをインストールしてサーバーと同じようにcookieを生成しました。
SpyFi
- genre : Cryptography
- point : 300
問題のソース : Source
フラグを含んだ文字列の前に任意の文字を入れられる文字列を暗号化した結果を返してもらえます。暗号はAESですが、ブロック方式はECBモードです。これは文字列を16byteに分割し、それぞれについて暗号を掛けます(画像:Wikipedia)
つまり同じ16文字のブロックは常に同じ文字列を返すことが分かります。
ここで問題で与えられる文字列を見てみます。自由な文字列を挿入できるので文字列の長さを変えることができます。これを上手くやると、任意の16文字についての暗号化結果を入手できることが分かります。
また、不明部分(picoCTF{???}のハテナ部分)までの文字数も分かっているので、不明部分が一文字だけ含まれたブロックを作成することもできます。
それを行ったのが以下です。
アンダースコア(_)は位置をズラすための無駄な文字、アスタリスク(*)は求めたいブロックの文字列をそこに入れます。この場合だと"de is: picoCTF{?"です。不明部分である?を可能な文字について全探索してあげ、暗号文が一致するものがあればそれが一文字目だと分かります。
もちろん一文字分かれば二文字目、それが分かれば…と続けていけるので、フラグの終端までそれを繰り返します。
ソースコードです。
eleCTRic
- genre : Cryptography
- point : 400
与えられた特定の文(flagのファイル名)を暗号化した文を入手できれば勝ちです。特定の文字を含むファイル名以外であれば任意の文を暗号化可能です。
ソースを読んでみるとCTRモードで動いていることが分かります。これは暗号で使うキーを各ブロック毎に変更することでセキュアな暗号方法を実現するものです。(画像:Wikipedia)
具体的には、特定の初期値(Nonce)とcounterを暗号化し、それと平文をXORすることで
暗号文を生成しています。(平文はAESなどの暗号アルゴリズムを直接通過しません。)
しかし、この問題だとカウンタが動いていません。つまり、平文とXORする文字列はどのブロックでも変わらないのです。
flagのファイル名はアンダースコアを含んでいて、これは暗号化できない文字列であるので___…___flag_hoge.txt のような文字列を暗号化するアプローチは取れません。なので、平文とXORする文字列を特定します。
平文はASCIIで与えられているので、適当な文字列を与えて暗号文とXORしてあげれば目的の文字列を入手できます。これにより、文を暗号化することができます。
これはソルバというより計算の問題だったので、オンラインのBase64デコードやXORが簡単に可能なサイト(Cryptii)を使用しました。
James Brahm Returns
- genre : Cryptography
- point : 700
POODLEをします
ソース:
おまけ:asm-4
ぞへがFlagらしきものを出したのに通りませんでした。適当にエスパーして通しました。
感想
2週間ずっとCTFをやるっていうのもなかなかに楽しいですね。たくさん解ける問題があってずっと速度が落ちなかったのも楽しかったです。また、東工大のHaruharaMaiチームと接戦を繰り広げられたのでよかったです。最後まで負けていたんですが、ぞへが最後の50分くらいで通した激アツ展開でした。
スコアの伸びのグラフです。3/4くらいのところで上がっているのは、僕が最後の三問くらいを一気に通せたからです。たのしかった。