newbieからバイナリアンへ

newbieからバイナリアンへ

コンピュータ初心者からバイナリアンを目指す大学生日記

【pwn 9.2】 STLC - TSG CTF 2019

 

 

0: 参考

 

github.com

 

softwarefoundations.cis.upenn.edu

 

 

 1: イントロ

前回に引き続きTSG CTF 2019のpwn問題を解いていく

今回は Hard 問題の "STLC"

 

結論から言うと初見では全く歯が立たず、作問者様のwriteupを割とすぐに且つ割と全面的に参考にさせていただいた

(ちなみに、このCTFの問題で唯一の0solved問題。恐ろしい)

まぁ作問者様のwriteupが英語ゆえ

英語を日本語に翻訳し、且つ内容を自分が理解できるように翻訳しながら書き進めていく

 

 

難しそうな問題ゆえあまり解きたくはないが

pwnと銘打っている以上びびる自分に鞭を打ち

自らをsatos気持ちでやっていく

 

 

 

2: とっかかりの脆弱性へのとっかかり

STLCについて

本問題はSTLCという関数型言語(?)のインタプリタを題材としている

pwnの問題でインタプリタとかVM系の問題を解くのは初めてだ

まずはSTLCについて簡単に説明を書いておくが

関数型言語が何者かも知らんし、ラムダ計算が何者かもわからない

とにかく本文を解くのに必要な知識を必要最低限な理解度で箇条書しておく

 

\x:Bool. x
 == Bool->Bool 恒等関数
\x:Bool. \y:Bool. x
  == Bool -> (Bool->Bool)
\x:Bool->Bool. f(f true)
  == Bool->Bool -> Bool  高階関数

なお2変数関数は実際には1変数関数を引数にとる1変数関数である

 

 

Capture Avoiding Substitutionについて

ラムダ計算における引数名は同一性を保証する以外に全く意味を持たない

たとえば以下の2つの関数は全く同じである

(\x:A->A. \y:A. x y)
(\n:A->A. \m:A. n m)

(なお x y は関数xに引数としてyを渡すことを意味する)

 

さてそれを踏まえた上で置換を行うことを考える

下のような置換は正しい

(\x:Bool->Bool. \y:Bool. x y) f
 <==> (y:Bool. f y)

 

例えば全体の引数fが関数定義内で用いられている変数yと同名であった場合には以下のように置換されるのが正しい

(\x:Bool->Bool. \y:Bool. x y) y
 <==> (\z:Bool. y z)

 

以下の置換は正しくない

(\x:Bool->Bool. \y:Bool. x y) y
 <==> (\y:Bool. y y)

 

正しくない方の置換では本来ラムダの支配下(?)にないはずの引数まで

関数定義内の変数として認識されてしまっている

このような誤りをしないように式を解釈する機構をCapture Avoiding Substitutionという

(ラムダからのcaptureをavoidするsubstitutionという安直な名前)

 

 

本問に於いて

さて、本問では上記のcapture avoiding substitutionが実装されていない

すなわち上に示した正しくない方の置換がなされるということになる

 

作問者様のwriteupから引用すると以下のような解釈がなされることになる(引用開始)

the input

f1 = (\f:I->I. \g:A->A. g)
f2 = (\x:(I->I)->(A->A)->A->A. \f1:A->A. x dec) f1 (\d:A. d)

leads to the output

> f1 = (\f:(I->I).(\g:(A->A).g)) :: ((I->I)->((A->A)->(A->A)))
> f2 = dec :: ((A->A)->(A->A))

(引用終わり)

 

関数f1はI->I関数とA->A関数の2つをとりA->A関数をそのまま返すため、型は(I->I)->(A->A)->(A->A)

f2の方は少しわかりづらいため型を以下に整理しておく

 

(\x:(I->I)->(A->A)->A->A. \f1:A->A. x dec)

型 :( (I->I)->(A->A)->(A->A) ) -> (A->A) -> ( (A->A)->(A->A) )

説明:(I->I)->(A->A)->(A->A)関数とA->A関数をとり、前者に対してdec関数を適用する関数

 

(\x:(I->I)->(A->A)->A->A. \f1:A->A. x dec) f1

型 :(A->A) -> ( (A->A)->(A->A) )

 

f2 = (\x:(I->I)->(A->A)->A->A. \f1:A->A. x dec) f1 (\d:A. d)

型 :(A->A) -> (A->A)

 

 

さて、こうしてできあがったf2の定義は正しくは(capture avoiding substitutionが実装されていれば)

f2 = (\g:A->A. g) :: A->A -> A->A

であるはずである

但し今回"f1"に対して衝突が起こっているため置換がうまく行かず

結果f2という関数がdec関数になってしまい

しかも本来I->I型であるdec関数が、(A->A)->(A->A)型になってしまっている

 

 

 

 

3: XXX

 

ああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああああわからんわからんわからんわからんわからんわからんわからんわからんわからんわからんわからんわからんわからんわからん

 

上のようにして組み込みdec関数を作ると型チェック無しでstruct Var(と想定しているstructure)のvarから減算するが、他の型のものをdecに渡してやることでdecに相当する位置にあるポインタを操作することができる

みたいなところまでわかったけどその後がわからんわからんわからんわからん

 

この問題考えてたら1日のQOLが5.2割低下し、且つ自分の頭じゃこの先考えても泥沼に嵌りそうなため、これにて終了!!!!!!!!!!