最初に
12/2 に出した問題のwriteupです。この投稿は、ISer Advent Calendar 2018 の23日目として書かれました。昨日は、とんがり さんの
でした。
Statement
副作用も、libcもいなくなったとき残るのは、型安全で純粋な素晴らしい世界のはずだった......
nc external.pwn.ctf-day3.tsg.ne.jp 31000
接続すると、min-camlのプログラムをサーバーに提出でき、サーバーはmin-camlコンパイラでコンパイルして実行をしてくれます。シェルを取れるようなプログラムを提出してフラグを得てください。ただし、min-camlコンパイラには問題を成立させるための以下に示すパッチが入っています。
パッチの概要
Writeup
今回バイナリは、PIE + NX bitでコンパイルされます。なので、考えるべきは
- 命令が配置されたアドレスリーク
- eipの取り方
- getsh
の３つです。
命令が配置されたアドレスリーク
これは、min-camlのクロージャを使います。クロージャとは、住井先生のクロージャ変換 の説明を見たほうがより分かりやすいと思いますが、「関数（アドレス）」と「自由変数束縛」を束ねたものをクロージャといいます。クロージャの構造はヒープの上に配置され、よってこのクロージャの中にある関数のアドレスから、命令の配置された場所が分かります。
ところで、クロージャはクロージャ変換に際して作られますが、このとき、自由変数が無い、クロージャが必要ないと保守的に判断できる場合は、実行効率の向上の為直接関数呼び出しが行われるようになっています。したがって、適切な関数を作る必要があり、例えば関数を引数に取るような関数に適用する関数などがそれにあたります
let rec g f = f 1 in let rec f x = x + 1 in let _ = g f
クロージャをヒープに置いた上で適当な配列の配列外へのアクセスを行えば、無事、命令の配置された場所が得られます
let rec g f = f 22 in let rec f x = x in let int80 = l.(1) + g f in
ただし、22は、ヒープに置かれるfの位置に対するint80であるmin_caml_startまでのオフセットです。
eipの取り方
この問題の本質部分です。個人的には、ideal.patchで与えたパッチによって、「ヒープ上の関数アドレスの書き換え」や「リターンアドレスの書き換え」ができないようにしたつもりでいます。よって、そのような方法以外でeipを取る必要があります。自分で書いたプログラムのeipを取るっていうのも変な話ですが。
min-camlの型システムは、"基本的に健全" だと思われます。すなわち、型がついたプログラムは、実行時に型エラーが起こることは無いはずです。やってみるとわかりますが、非常によく型推論をして型付けしてくれます（まぁそれはそうなんですが）。
ただし、これには例外があり、外部関数への関数適用は、正しい推論ができないという点です。というのも、外部関数はリンカでリンクされるものであり、その内部がmin-camlで閉じていないためです。このため、min-camlは、min-camlのプログラム内での「使われ方」が一貫しているかどうかまでしか見ていません。すなわち、fという外部関数に対して、f: int -> intであるような使い方をするコードと，f: int -> boolを両立させることは出来ないが、しかしプログラム内で一貫していれば任意の型付けをさせることができます。この話はtyping.mlの120行目付近 がその詳細です。
これを用いてcreate_arrayという外部関数を誤認させます。create_arrayは、本来引数に「配列の長さ」(int)と、「初期値」 (いくつかの型（関数や配列、整数など）についてそれに対する動作が定義されている、いわゆるアドホックな多相性を保有しているが、実態は32bitの数値を受け取るような実装) の２つを受け取って、配列(初期値の型の配列型)を返すような関数です。この関数は、min-camlの実装としては直接呼ばれない想定で、Array.makeないしArray.createが、言語レベルで実装されたアドホック多相を有した関数として存在します。
今回この誤認を用いて、create_arrayを Fun((int, int), (Fun(int, int, int, int), unit)) 、すなわち、２つの整数を受け取って、「4つの整数を受け取ってunitを返す関数」を返す関数として誤認させることで、型システムを騙すことができます。このとき関数を返す関数で返される値は、上で説明したようにクロージャであることに注意が必要で、Arrayを通して一段ポインタを挟んだ状態が正しいクロージャの構造です。
簡単には
let f = create_array 1 12345678 in f 1 2 3 4
というプログラムをmin-camlで実行したときどのような動作（セグメンテーションフォルトになると思うが）をするかを見てみると様子が分かると思います。
getsh
eipが取れればgetshをするのはそれほど難しくないです。自分の想定解では、min-camlのプログラム中にうまくコードを書くことで「int 0x80」を埋め込み、eipを奪ってそこに飛ばし、execve("/bin/sh", NULL, NULL)をする という方針でやりました。int 0x80は、x86のアセンブリにするとcd80であり、プログラム中に即値代入としてこの値を入れるプログラムを書けば、
277: bb cd 80 00 00 mov $0x80cd,%ebx
というコード片が得られるのでこれを用いればよいです。"/bin/sh"は、Arrayがheap上に確保されることを思い出せば、長さ1の配列を二個連続で確保すれば
let bin = Array.make 1 1852400175 in let sh = Array.make 1 6845231 in
これで、ヒープの上に"/bin/sh\x00"が作られるので、binのアドレスを文字列の先頭だと考えれば、これで/bin/shが得られます。あとは、システムコールの引数として、eax, ebx, ecx, edxに値が入るようにすればよく、これは関数呼び出しで対応できます。
回答者
kcz146 さんが解いてくれました。わいわい。
writeupがあります
実は最初は、見落とすべきでないような非想定解が存在し、二問目を出してしまいましたが、それもアツい感じで解かれました。CTF的解答という感じで面白いのでぜひ見てみてください。
非想定だったというのは簡単に言うとArrayへのアクセスの配列外参照で適当なクロージャのアドレスに飛ばすことができるようになってしまいました。これを防ぐために、二問目は配列のアクセス自体をできなくなるようにしました。
なので、上で書いた命令アドレスのリークがやや複合的になり、これはfloat_of_intの型を壊してアクセスします。タプルのアクセスは実質的にdereferenceとして機能するので、これにより、クロージャのアドレスがリークできます。
全体
let k = 32973 in let l = Array.make 1 k in let rec g f = f 33 in let rec f x = x in let l = Array.make 2 g in let (l,_) = float_of_int l in let (l,_) = l in let int80 = l + g f in let f = create_array 1 int80 in let bin = Array.make 1 1852400175 in let sh = Array.make 1 6845231 in f 11 bin 0 0
二問どちらのフラグも取ることができます。
まとめ
min-camlは、程よく小さく、しかしサイズに対してはよく出来たコンパイラで、遊んでいてたのしいです。まぁしかし現実のシステムでこういう問題作りたいですね。
あと今日SECCON International Finalで、優勝しました（？）（わいわいって言いながらNIRVANAを見る係をしていた）
