MacにZ3をインストールした。

新しいMacを手に入れたので環境構築を行っている。
その過程で、Z3のインストールにハマったので忘備録を書いておく。

目標

Z3はMicrosoftが開発しているSMTソルバで、様々な言語のバインディングがある。
公式でサポートしているのはC/C++, Java, Python, OCaml等でHaskellでは非公式のラッパーライブラリを用いる。
github.com
z3: Bindings for the Z3 Theorem Prover

今回はOCamlHaskell両方のバインディングをインストールしたい。

トラブル

まず、z3をmlバインディングつきでインストールする。

$ git clone https://github.com/Z3Prover/z3.git
$ cd z3
$ scripts/mk_make.py --ml # --mlはmlバインディングをインストールするフラグ
$ make -C build
$ make -C build install

これでlibz3.dylibが/usr/local/lib以下にインストールされ、mlバインディングのライブラリは~/.opam/`opam switch show`/lib/Z3以下にインストールされる。

次にZ3のHaskellバインディングライブラリをインストールしようとして失敗した。

$ cabal install z3 -f examples
=> ERROR!

これをデバッグしていくと、libz3.dylibに_Z3_get_error_msg_exという関数がないことが原因だとわかった。

$ gobjdump -T /usr/local/lib/libz3.dylib | grep _get_error
0000000000028af0 g       1e SECT   01 0000 [.text] __Z22exec_Z3_get_error_codeR11z3_replayer
0000000000028b40 g       1e SECT   01 0000 [.text] __Z21exec_Z3_get_error_msgR11z3_replayer
0000000000069880 g       1e SECT   01 0000 [.text] __Z21log_Z3_get_error_codeP11_Z3_context
0000000000069a10 g       1e SECT   01 0000 [.text] __Z20log_Z3_get_error_msgP11_Z3_context13Z3_error_code
0000000000034060 g       0f SECT   01 0000 [.text] _Z3_get_error_code
00000000000340f0 g       0f SECT   01 0000 [.text] _Z3_get_error_msg
$

原因究明

Z3のレポジトリを読んでいつこの関数が消えたのかということを調べたら、去年の11月ごろに以下のコミット周辺で消されていることが判明した。
github.com
このコミット以前では次のようなAPIになっていた。

Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err);
Z3_API char const * Z3_get_error_msg(Z3_error_code err);

実装を読むとZ3_get_error_msgはZ3_get_error_msg_ex(0, err)と同じ振る舞いをするようだ。
ずいぶん前からZ3_get_error_msg自体はdeprecatedになっており、代わりにZ3_get_error_msg_exを使えということになっていた。

コミットの以後はつぎのようなAPIになっている。

Z3_API char const * Z3_get_error_msg(Z3_context c, Z3_error_code err);

つまり、長らく負の遺産となっていたZ3_get_error_msgをまともなAPIに直したということだろう。
しかし、このとき同時にZ3_get_error_msg_exも消し去ってしまうのは後方互換性の考え方からしてちょっと配慮が足りないのではないだろうか。当分の間はZ3_get_error_msg_exはdeprecatedのまま残しておいてwrapperライブラリ開発者が対応する時間を与えるべきだったと思う。

解決策

z3-haskellの開発者にプルリクを送ろうかとも考えたが、z3-haskellmercurialで管理されていたのでしばらくプルリクの送り方を勉強してからにする予定である。
当分は問題の少なそうなコミットを適当に探した結果、c2108f74f1e5c5ab96c6e4cc189ccbc55dca339aをチェックアウトしてからビルドすれば問題なさそうである。
そもそもz3のバージョンが変わらないのにAPIの仕様が変わっているのがすごくよくないと思うので、z3にはstableなブランチを是非とも作って欲しいものだ。

5/30 21:30 追記

そもそも、masterブランチで開発されているのはz3-4.4.2でありRelease前のバージョンだと気付いた。stableなバージョンも普通にgithubのreleasesにあった。
Releases · Z3Prover/z3 · GitHub
master HEADは極めてunstableでないとわかったので大人しく最新releaseであるz3-4.4.1をインストールするのが無難だろう。

$ git clone https://github.com/Z3Prover/z3.git
$ cd z3
$ git checkout refs/tags/z3-4.4.1
$ python scripts/make_mk.py --ml --prefix=/usr/local
$ make -C build
$ make -C build install

vectorを使ったData.List.sortより4倍速いsortアルゴリズムの実装

Data.List.sortがあまりに遅くてつらいので、vectorを使って書いてチューニングしたら約4倍速くなりましたという話をします。その過程でvectorのmonadic indexingとは何かという話をします。

仕様としてData.Listと互換性を持たせるため、次のようなインターフェースにしました。

{-# INLINE sort #-}
sort :: Ord a => [a] -> [a]
sort = sortBy compare
sortBy :: (a -> a -> Ordering) -> [a] -> [a]
sortBy = ...

次に実装を見てきます。

import qualified Data.Vector as V
...
sortBy cmp = V.toList . mergeSortAux . V.fromList
    where 
    mergeSortAux l = ...

入力はリストで与えられるので、まず最初にfromList :: [a] -> Vector aを使ってData.Vector.Vectorに変換し、mergeSortAux :: Vector a -> Vector aを使ってソートした後に、toList :: Vector a -> [a]を用いてリストに戻します。Unboxed Vectorを使うとさらに速くなりますが、ソートできるデータが制限されてしまうので今回はBoxed Vectorを使います。

mergeSortAuxの実装はただのマージソートです。今後ところどころunsafeなんとかを使っていますが、これは今回のアルゴリズムでは境界値外アクセスすることはないので配列の境界チェックを省くために行っているだけです。怖くないよ。

import qualified Data.Vector as V
...
sortBy cmp = ...
    where 
    mergeSortAux l
        | n <= 1 = l
        | otherwise = merge (n1, l1') (n2, l2')
             where
                n  = V.length l
                n1 = div n 2
                n2 = n - n1
                l1 = V.unsafeSlice 0  n1 l
                l2 = V.unsafeSlice n1 n2 l
                l1' = mergeSortAux l1
                l2' = mergeSortAux l2
    merge = ... 

さて、最後にmergeの実装を見てきましょう。

{-# LANGUAGE BangPatterns #-}
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as MV

sortBy cmp = ...
    where
    ....
    merge (!n1,!as) (!n2,!bs) = V.create $ do
        res <- MV.unsafeNew (n1+n2)
        let go i1 i2 = ...
        go 0 0

V.create :: (forall s. ST s (MVector s a)) -> Vector aを使ってMVector s aをVectorに変換します。
do構文の中ではマージ後の配列を格納するres :: MVector s aを確保し、go関数で先頭から順番に値を埋めていく感じです。

        let go i1 i2 | i1 >= n1 && i2 >= n2 = return res
                     | i1 >= n1 = tick2 i1 i2
                     | i2 >= n2 = tick1 i1 i2
                     | otherwise = do
                         v1 <- V.unsafeIndexM as i1
                         v2 <- V.unsafeIndexM bs i2
                         case cmp v1 v2 of
                            GT  -> do
                                 MV.unsafeWrite res (i1 + i2) v2
                                 go i1 (i2 + 1)
                            _   -> do
                                 MV.unsafeWrite res (i1 + i2) v1
                                 go (i1 + 1) i2
            tick1 i1 i2 = do
                V.unsafeIndexM as i1 >>= MV.unsafeWrite res (i1 + i2)
                go (i1 + 1) i2
            tick2 i1 i2 = do
                V.unsafeIndexM bs i2 >>= MV.unsafeWrite res (i1 + i2)
                go i1 (i2 + 1)

goの中でV.unsafeIndexMを使っていますが、これの意味について説明します。

indexMについて

例として以下のようなIndexTest.hsを考えます。

gist4eb6a528eed4ef665e9bcf1d91441094

$ ghc -O2 IndexTest.hs
$ ./IndexTest
test1: safe!
test2: safe!
IndexTest: Prelude.undefined

実行するとtest3でundefinedエラーが発生します。

コンパイルの中間コードをdumpして何が起こっているのかを読みます。

$ touch IndexTest.hs
$ ghc -ddump-simpl -O2 IndexTest.hs > IndexTest.log

ghc -ddump-simpl -O2 IndexTest.hs (GHC 7.10.2)

test1のコンパイル結果を見ましょう。

a1_r5Mg
  :: V.Vector Int
     -> GHC.Prim.State# GHC.Prim.RealWorld
     -> (# GHC.Prim.State# GHC.Prim.RealWorld, () #)
[GblId, Arity=2, Str=DmdType <S,1*H><L,U>]
a1_r5Mg =
  \ (v_a2pg :: V.Vector Int)
    (eta_B1 [OS=OneShot] :: GHC.Prim.State# GHC.Prim.RealWorld) ->
    case v_a2pg
    of _ [Occ=Dead]
    { Data.Vector.Vector ipv_s2CZ ipv1_s2Db ipv2_s2Dc ->
    ((check_r2i0
        lvl2_r5Mf
        (case GHC.Prim.indexArray# @ Int ipv2_s2Dc ipv_s2CZ
         of _ [Occ=Dead] { (# ipv3_a5vA #) ->
         ipv3_a5vA
         }))
     `cast` ...)
      eta_B1
    }

test1 [InlPrag=NOINLINE] :: V.Vector Int -> IO ()
[GblId, Arity=2, Str=DmdType <S,1*H><L,U>]
test1 =
  a1_r5Mg
  `cast` ...

ごちゃごちゃしてますが重要なことはcheck関数呼び出し時に

(check_r2i0
        lvl2_r5Mf
        (case GHC.Prim.indexArray# @ Int ipv2_s2Dc ipv_s2CZ
         of _ [Occ=Dead] { (# ipv3_a5vA #) ->
         ipv3_a5vA
         }))

と(case...)の部分が遅延評価されているということです。
この部分は元のソースコードでは(V.unsafeIndex v 0)の部分に対応します。
このため、余計なオーバーヘッドが生じてしまいます。

次にtest2のコンパイル結果を見ます。

a3_r5Mk
  :: V.Vector Int
     -> GHC.Prim.State# GHC.Prim.RealWorld
     -> (# GHC.Prim.State# GHC.Prim.RealWorld, () #)
[GblId, Arity=2, Str=DmdType <S,1*U(U,A,U)><L,U>]
a3_r5Mk =
  \ (v_a2ph :: V.Vector Int)
    (eta_B1 [OS=OneShot] :: GHC.Prim.State# GHC.Prim.RealWorld) ->
    case v_a2ph
    of _ [Occ=Dead]
    { Data.Vector.Vector ipv_s2Dk ipv1_s2Dl ipv2_s2Dm ->
    case GHC.Prim.indexArray# @ Int ipv2_s2Dm ipv_s2Dk
    of _ [Occ=Dead] { (# ipv3_a5vA #) ->
    ((check_r2i0 lvl4_r5Mj ipv3_a5vA)
     `cast` ...)
      eta_B1
    }
    }

test2 [InlPrag=NOINLINE] :: V.Vector Int -> IO ()
[GblId, Arity=2, Str=DmdType <S,1*U(U,A,U)><L,U>]
test2 =
  a3_r5Mk
  `cast` ...

今度はcheckの呼び出しの前にindexArray#が呼び出されています。
しかし、配列の要素自体は評価しないのでundefinedエラーは発生しません。

最後にtest3のコンパイル結果を見ます。

a2_r5Mi
  :: V.Vector Int
     -> GHC.Prim.State# GHC.Prim.RealWorld
     -> (# GHC.Prim.State# GHC.Prim.RealWorld, () #)
[GblId, Arity=2, Str=DmdType <S,1*U(U,A,U)><L,U>]
a2_r5Mi =
  \ (v_a2pj :: V.Vector Int)
    (eta_B1 [OS=OneShot] :: GHC.Prim.State# GHC.Prim.RealWorld) ->
    case v_a2pj
    of _ [Occ=Dead]
    { Data.Vector.Vector ipv_s2Df ipv1_s2Dg ipv2_s2Dh ->
    case GHC.Prim.indexArray# @ Int ipv2_s2Dh ipv_s2Df
    of _ [Occ=Dead] { (# ipv3_a5vA #) ->
    case ipv3_a5vA of vx_a2zI { GHC.Types.I# ipv4_s3c7 ->
    ((check_r2i0 lvl3_r5Mh vx_a2zI)
     `cast` ...)
      eta_B1
    }
    }
    }

test3 [InlPrag=NOINLINE] :: V.Vector Int -> IO ()
[GblId, Arity=2, Str=DmdType <S,1*U(U,A,U)><L,U>]
test3 =
  a2_r5Mi
  `cast` ...

この場合もcheckの呼び出し前にindexArray#を呼び出していて余計なオーバーヘッドは生じないのですが、さらに配列の要素も評価してしまうのでこの例ではundefinedエラーとなってしまいます。

まとめると

  • check "test1" (V.unsafeIndex v 0)だと配列アクセスのためのサンクが作って関数呼び出し。
  • check "test3" $! (V.unsafeIndex v 0)だと配列アクセスと要素の評価の後、関数呼び出し。
  • V.unsafeIndexM v 0 >>= check "test2"だと配列アクセスの後、関数呼び出し。

ちなみにindexM系がモナド内でしか使えないのはある種のHackなのでモナドの種類は関係ないはずです。

実験

今回書いたソートのコードはgistにまとめています。
gist1b847adefb53e04eedd1b7adabfcc330

次のようなテストプログラムを書いて実験を行いました。

gistecc5317d3f07cc2890f68da58bdec379

入力として30万要素のランダムな整数列を与えてみます。

$ ./Main < test300000.in > test300000.out
[2016-04-04 04:38:12.623993 UTC] Parsing: begin
[2016-04-04 04:38:12.709319 UTC] Parsing: end
[2016-04-04 04:38:12.709578 UTC] Parsing: 0.085326s
[2016-04-04 04:38:12.709794 UTC] Vector: begin
[2016-04-04 04:38:12.976383 UTC] Vector: end
[2016-04-04 04:38:12.976596 UTC] Vector: Sorting: 0.266589s
[2016-04-04 04:38:12.976818 UTC] List: begin
[2016-04-04 04:38:14.018594 UTC] List: end
[2016-04-04 04:38:14.018809 UTC] List: Sorting: 1.041776s
[2016-04-04 04:38:14.019109 UTC] result validation begin
[2016-04-04 04:38:14.022344 UTC] Correct!
[2016-04-04 04:38:14.126167 UTC] output done
[2016-04-04 04:38:14.126446 UTC] Elapsed Time: 1.502174s
[2016-04-04 04:38:14.126715 UTC] Speedup (Data.List.sort / VecSort.sort) = 391%

Data.List.sortは1.04秒かかっていたのに対してVecSort.sortは0.267秒でおよそ4倍高速になりました。もちろん、ソートされたリストの最初の幾つかの要素が欲しい場合などではData.List.sortの方が速いこともありますが、全体をソートしたい場合にはたくさんのメモリを消費するリストを用いたソートよりも、省メモリなVectorを用いたソートを用いたほうがよいと思います。

SECCON 2015 Final (Intercollege) 参加記

先週の土曜日にSECCONの決勝大会にnegainoidoというチームで参加してきました。
SECCON 2015 決勝大会 | SECCON 2015 NEWS

北千住駅から降りて東京電機大学に着くと受付にかっこいい可視化システムが置いてありました。優勝したチームdodododoは試合開始前から201ポイント稼いでいて格の違いを見せつけてきました。(本当は運営がテストのため得点を入れていただけです)
f:id:autotaker:20160202151856j:plain

決勝の形式について

学生大会の決勝は普段のJeopadyスタイルではなく、Attack&Defenceという形式でした。
決勝のシステムについて簡単に説明します。

  • 各チームに一台サーバが用意される。
  • 各サーバでは3つのWEBサービスを動かす。
    • vulnerable_blog: ブログ(というか掲示板?)PHPで書かれていた。
    • keiba: 競馬予想をするウェブサービス。nodejsで動かす。
    • sbox2015: ユーザがアップロードしたプログラムをサーバで実行する危険極まりないサービス。PythonCGIとして書かれていた。
  • 得点はAttackポイントとDefenceポイントに分かれる。
    • Attackポイント:他のチームのサーバからフラグを抜き出して運営サーバに送信することで攻撃されたチームの総得点の3%を奪うことができる。
    • Defenceポイント:運営が5分おきに各チームのWEBサービスの動作を確認するスクリプト(mechanize)を走らせる。それによってサービスが動いていることが確認できたら、一つのサービスあたり100ポイントもらえる。

試合経過

決勝開始と同時に各サーバへのアクセスが許可される。
ただし、各サーバのIPアドレスはエスパーしなければならない。
決勝に参加するようなウィザード級ハッカーにはその程度朝飯前なのだろう。
数分後、エスパー力の低いチームのためにIPアドレスが公開された。
とりあえず事前にもらったパスワードでサーバに接続しに行く。
ところでユーザ名は?
これはrootで良かったようだ。この程度ならなんとかエスパーできた。

このSSHなのだが、だいたい1分くらい放置すると接続を切られてしまう。
(試合が終わったあとに調べたら対処法はあったらしい。)
サーバの中をみるとvulnerable_blogとsbox2015は/var/www/以下で動いていることが確認できた。
keibaに関しては自分でnohup node app.js等で動かす必要があった。

ちなみに最初の15分は運営の動作確認スクリプトが走らないので、得点を得ることはできない。この間に、できる限り動作を把握することが肝要なのだろう。

開始15分が過ぎて、各チームの得点に変化が現れた。だいたいのチームがDefenceポイントを得点し始めた。Defenceポイントはとりあえず何もしなくてももらえるようだ。
さて、得点を伸ばすためにはAttackポイントをとりつつ、ほかのチームから得点を奪われないようにフラグを守る必要がある。ん?.... フラグ? .....

フラグって何だ????

特にサーバのソースコードやデータベース等に自分のフラグが置かれている様子はない。
意味がわからない。
そうこうしているうちにエスパー能力に優れた他のチームが攻撃を開始し出した。彼らにはフラグが何であるか理解できているのだろう。

しばらくしてチームメイトが他チームの攻撃を解析して、どうやらvulnerable_blogのDBの中にフラグが潜んでいるらしいことを突き止めてくれた。
データベースにはブログの利用者の投稿が残されている。それには投稿タイトル、内容、削除キーが含まれていた。
どうやらDefenceポイント確認のために運営が5分おきにブログに投稿を行うのだが、そのときの削除キーが自分のチームのフラグだったらしい。
そしてこれは試合後にわかったことだが、他のサービスでも運営の動作確認時に自分のチームのフラグが書き込まれるというゲームだったようだ。

試合中にはvulnerable_blog中のフラグのみしか気付けなかったので、他のチームからこれを奪うことにした。
奪うために利用したのはsbox2015に存在する自明な任意コード実行の脆弱性であった。
案外多くのチームのフラグをこの方法で奪うことができたようだ。
攻撃はTailedとcympfhに任せて、自分はvulnerable_blogの防衛を行うことにした。

vulnerable_blogでは次のような脆弱性を発見し修正した。

  • adminページの脆弱なパスワード
    • デフォルトではadminページにログインパスワードが"test"になっていたので推測されにくそうなものに変更した。adminページにログインすると各投稿の削除キーが閲覧できるのでフラグを盗まれるおそれがある。
  • SQLインジェクション
    • ブログを投稿する際のフォーム、及び投稿を閲覧する際のindex指定部等に脆弱性があったので適当にmysql-real-escape-stringで囲った。
  • XSS
    • ブログを表示する部分にXSS脆弱性があった。この脆弱性を用いれば、運営がフラグを書きこんだ際にjavascriptを用いてフラグを自サーバにリークさせることが可能だと考えられる。適切にhtmlspecialcharsで囲うことで修正した。

この全てを対策したあとではアクセスログを読む限りvulnerable_blogを使ってフラグを奪われることはなかったように思えた。しかしながら、他のチームはどんどん自分のチームのフラグを奪ってAttackポイントを稼いでいた。
試合中にはその原因はついにわからなかったが、おそらくsboxのフラグを盗まれていたのだろう。

結果

negainoidoの最終結果は11位でした。Attackポイントは上位チームに引けを取らない数字だったのに、防衛が全く足りていなかったのが敗因でした。
初見殺しが多かったもののゲーム自体は面白かったと思います。

大会後の懇親会で振る舞われたお寿司は美味しかったです。
来年からは学生枠で参加するのは難しいですが、Attack&Defenceの経験が積めたのでまた機会があればより善戦できるはずです。
f:id:autotaker:20160202152155j:plain

OCamlの末尾再帰について

この記事はMLアドベントカレンダー22日目の記事です。

プロローグ

autotakerはHaskellのList.sortが遅いので嘆いていた。
あまりに遅いので簡単なコードを書いて実験することにした。

gist082402e29104b2f21a6d

$ wc test300000.in
  300000  300000 2994897 test300000.in
$ head test300000.in
-145530267
165962464
79995549
-41622317
-133297703
38688159
191031379
-188084614
-187672271
-148432431
./ListSort < test300000.in > test300000.out
[2015-12-22 06:48:09.644106 UTC] begin
[2015-12-22 06:48:09.71299 UTC] parse done
[2015-12-22 06:48:10.610641 UTC] sort done
[2015-12-22 06:48:10.610854 UTC] Sorting: 0.897651s
[2015-12-22 06:48:10.707304 UTC] output done
[2015-12-22 06:48:10.707538 UTC] Elapsed Time: 1.063198s

30万個の整数列をソートするのに900msもかかるのだ。

比較のためにC++でもソートしてみた。

gist1b7a9a6f6b9c0f446ae5

$ g++-5 -std=c++11 -O3 sort.cpp -o sort
$ time ./sort < test300000.in > test300000.out
Sorting: 22ms

real	0m0.151s
user	0m0.133s
sys	0m0.010s

C++のstd::sortは爆速でわずか22msでソートが完了した。なんとHaskellのList.sortの40倍以上の速さである。これはいくらなんでも速すぎる。
調べたところstd::sortはIntro sortと呼ばれるQuick sortを少し賢くしたようなアルゴリズムで実装されている一方でList.sortはmerge sortに毛が生えたようなアルゴリズムで実装されているらしい。アルゴリズムが違うならまあ仕方ない。

ところで、標準ライブラリのソートにマージソートが採用されていてよくHaskellと比較される関数型言語があるではないか。
そうOCamlである。OCamlコンパイラGHCに比べてそれほどアグレッシブな最適化をするわけでもないし、さすがにOCamlよりは速いだろうと予想してコードを書いてみた。

OCamlのソートのバグ?

さて、ここまでが長い前振りで、ここから今回の本題に入ろう。
まず、次のようなOCamlのコードを書いて実験してみた。


gistebed443ea61424295eca

$ ocamlopt sort.ml -o sort-ml
$ time ./sort-ml < test300000.in > test300000.out
Sorting: 0.14416s

real	0m0.874s
user	0m0.393s
sys	0m0.470s

全体の実行時間が遅いのは主に入出力のせいなので気にしないこととして、
OCamlのList.sortは144msであり、Haskellの6倍以上速い。
これは意外な結果だったが、念のため出力があっているかを確認したときに興味深いことがわかった。

$ diff test300000.ans test300000.out | head
2,3d1
< -214745540
< -214744494
14d11
< -214729150
18d14
< -214725140
21d16
< -214723392
37d31

なんと正しくソートできていないではないか!
この短く単純なコードのどこに私はバグを仕込んでしまったのだろう。

まずは入力を正しく読めているか確認した。

let main _ = 
    let ps = read_ints [] in
    let start_t = Sys.time() in
    Printf.fprintf stderr "length: %d\n" (List.length ps);
    let qs = List.sort compare ps in
    let end_t = Sys.time() in
    Printf.fprintf stderr "Sorting: %.5fs\n" (end_t -. start_t);
    output_ints qs;;
./sort-ml < test300000.in > test300000.out
length: 261056
Sorting: 0.14787s

どうやらバグはread_intsにあるらしい。

let rec read_ints acc =
    try
        let v = read_int() in
        read_ints (v::acc)
    with
        _ -> List.rev acc

このコードを書いた時の私の気持ちはこうだ。

  1. 入力はデカイので末尾再帰にする必要がある。アキュムレータ引数を用意しよう。
  2. read_intのドキュメントにはファイルの末尾に達したら、End_of_file例外が投げられるとかいてある。tryで包んで例外を捉えよう。
  3. 例外の名前打ち込むの面倒だし、使い捨てのコードだから_でマッチさせてもいいよね!

3つ目が私の怠慢であることは認めるが、上の二つは正しそうに思えないだろうか。

私は自身の怠慢を認め、期待する例外の名前を正しく書くことにした。

let rec read_ints acc =
    try
        let v = read_int() in
        read_ints (v::acc)
    with
        End_of_file -> List.rev acc
$ ocamlopt sort.ml -o sort-ml
$ ./sort-ml < test300000.in > test300000.out
Fatal error: exception Stack_overflow

!!!!!Fatal error: exception Stack_overflow!!!!!
読者の中にはもう気づいた人もいるだろうが、実はこのread_intsは末尾再帰になっていないのだ。
なぜかというと、read_intsにはread_ints(v::acc)を呼び出したあとに例外処理のコードがあるので、例外をキャッチした時にどのハンドラに渡すかを保存するためにスタックが必要になるためだ。

正しく末尾再帰にするためには例外をoption型に変換してやらないといけない。

let rec read_ints acc =
    let r = try Some (read_int()) with 
        End_of_file -> None in
    match r with
        Some(v) -> read_ints (v::acc)
        | None -> List.rev acc

このコードは多少不恰好だが、定数サイズのスタックしか消費しない。

gist764a6d75741e2f807bc5

$ ocamlopt sort1.ml -o sort1-ml
$ time ./sort1-ml < test300000.in > test300000.out
length: 300000
Sorting: 0.18463s

real	0m0.972s
user	0m0.436s
sys	0m0.530s
$ diff test300000.out test300000.ans

こうしてバグは修正された。めでたしめでたし。

後日談というか、今回のオチ

こうしてOCamlコードのバグは直ったわけだが、実験の結果、OCamlのList.sortは184msであり、やはりHaskellのList.sortがクソ遅いのはアルゴリズムのせいではなく、実装が悪いのだと考えられる。
競技Haskellerとしてこんな状況は許されないのでメモリ効率が悪いListの代わりにVectorを使ってマージソートを実装した。
gistdb303c4aae8e1ce9776b

$ ghc -O2 VecSort.hs
[1 of 1] Compiling Main             ( VecSort.hs, VecSort.o )
Linking VecSort ...
$ ./VecSort < test300000.in > test300000.out
[2015-12-22 07:58:53.725504 UTC] begin
[2015-12-22 07:58:53.805494 UTC] parse done
[2015-12-22 07:58:54.00343 UTC] sort done
[2015-12-22 07:58:54.003704 UTC] Sorting: 0.197936s
[2015-12-22 07:58:54.092547 UTC] output done
[2015-12-22 07:58:54.092758 UTC] Elapsed Time: 0.367043s

このように198msと、OCamlと大差ない時間になった。

SECCON 2015 Qual Writeup Crypto 200 Find the prime numbers

問題

つなぐと

2622440554406490912 + 0147433867683690946 = 4258610457570922687

などと表示される。数字は3秒おきに更新される。

解法

もらったソースを読む。

	while 1:
		x = pow(random.randint(1000000000, 9999999999), n, (n * n))
		o = (pow(n + 1, 1, n * n) * x) % (n * n)
		y = (((pow(o, l, n * n) - 1) // n) * d) % n
		if y == 1:
			break
	c = (pow(n + 1, int(v["num"]), n * n) * x) % (n * n)
	h = (c * o) % (n * n)
	q = "%019d + %019d = %019d" % (c, o, h)
	print q
	
	z = "QUERY_STRING"
	if z in os.environ and os.environ[z] != "":
		if w[e]["time"] < t and os.environ[z] == v["num"]:
			print "SECCON{" + v["flag"] + "}"
		w[e]["time"] = t + 60
		w[e]["outp"] = q
	else:
		w[e]["time"] = t + 3
		w[e]["outp"] = q

何をやっているのかはよくわからないが、v["num"]を当てれば良いらしい。
まず、nを当てたい。表示しているのはよく読むと

 x (n + 1)^k + (n + 1) x = (n + 1)^{m+1} x^2 \mod n^2
という等式のようだ。どう考えても、左辺+記号は*の間違いだろう。
つまり
 a * b = c \mod n^2
となる、 a, b, cがあたえられるわけだ。
ここから
 a * b = c + l n^2
 l n^2 = a * b - c
つまり、 a* b - c素因数分解すれば n^2の約数(素数p,q)が得られる。
たかだか36桁程度なのでmsieveを使って解ける(べつにためし割りでも大丈夫だろう)

$ msieve -v 386636553706711704268844486594760065
factoring 386636553706711704268844486594760065 (36 digits)
p1 factor: 5
p1 factor: 7
p2 factor: 11
p5 factor: 42727
p5 factor: 42727
p5 factor: 58757
p5 factor: 58757
prp15 factor: 159337556575289

よって、 n = 42727 \times 58757 = 2510510339が得られた。
次に、
 x (n + 1)^k + (n + 1) x = (n + 1)^{m+1} x^2 \mod n^2
 xを復元したい。これも簡単で、 x = b(n + 1)^{-1} \mod n^2と求められる。
最後に
 x (n + 1)^k = a から k = \log_{n+1}(a x^{-1}) と求められる。
離散対数はPARI/GPを用いた。

? znlog(3792102298388437469,Mod(2510510340, 6302662162225894921))
%1 = 1510490612

 k = 1510490612が求まったのでサーバに送れば良い。
FLAG: SECCON{SECCoooo_oooOooo_ooooooooN}

たぶん、想定解ではないが、いずれにせよ桁が小さすぎるのでどうやっても解けるとおもう。

使ったPythonスクリプト

giste65da419e982225b22de

SECCON 2015 Qualに参加しました。

チームnegainoidoで参加しました。

チームメンバーはautotaker, atetubou, cympfh, garasubo, isurugieri, tailedだった。
atetubouとtailedは台湾旅行(ICPCのアジア地区予選)中だったので遠隔参加でした。

コンテスト開始時

開始直後にatetubouがStart SECCON CTFを通した。

2015-12-05 15:02:16: negainoido: 50 (+50), Start SECCON CTF

SECCON Warsはやることははっきりしていたのでgarasuboに取り組んでもらった。

16時

2015-12-05 15:58:23: negainoido: 150 (+100), Reverse-Engineering Android APK 1

by autotaker

2015-12-05 16:03:40: negainoido: 250 (+100), Command-Line Quiz

by atetubou

2015-12-05 16:21:37: negainoido: 350 (+100), SECCON WARS 2015

by garasubo

コンテストサーバがおもくなりフラグを送信できなかったり、問題が見られなかったりでイライラしていた。

17時

2015-12-05 17:03:16: negainoido: 450 (+100), Connect the server

by tailed, autotaker

2015-12-05 17:45:33: negainoido: 750 (+300), Decrypt it

by atetubou

台湾でICPCの準備中とは思えないatetubouとtailedの仕事の早さに驚かされた。
本戦に行けることになったときに、チーム内で選抜をするという脅しをかけたのが良かったのかもしれない。
atetubouにunzipが既知平文攻撃ではないかと教えてもらい、cympfhが手元でpkcrackを走らせ始めた。

Entry formについてtailed, autotaker, cympfhでいろいろと試す。

18時

2015-12-05 18:39:55: negainoido: 850 (+100), Entry form

by tailed, cympfh, autotaker
Entry formの問題でtailedがブラインドOSインジェクションで/SECRETS/以下を読む。
atetubouとtailedが移動でafkしている間にbackdoor123.phpを発見して解いた。

garasuboが帰宅。

19時

isurugieriがCodeThanksFestivalから帰ってきて参加。
晩御飯を食べる。

20時

2015-12-05 20:00:45: negainoido: 950 (+100), Unzip the file

by cympfh
pkcrackがようやく解読してくれた。長い戦いだった。
atetubou, tailedがホテルに移動し、スカイプ通話ができるようになった。
実装の面倒なQRを分担して片付けることになった。
isurugieriとcympfhがQR(Windows)、実装に定評のあるatetubouがQR(Nonogram)を担当。

22時

2015-12-05 22:00:29: negainoido: 1150 (+200), Find the prime numbers

by autotaker, tailed

2015-12-05 22:06:51: negainoido: 1450 (+300), Exec dmesg

by tailed

2015-12-05 22:45:55: negainoido: 1750 (+300), QR puzzle (Nonogram)

by atetubou
Find the prime numbersは何をしているのかはよくわからなかったが、解くだけなら簡単な素因数分解と離散対数を解くだけだった。なんだったんだろう。

23時

2015-12-05 23:36:37: negainoido: 1850 (+100), Steganography 3

by atetubou, tailed
OCRでバイナリを読んで実行した。floodfillの意味をtailedがエスパーしてくれた。
QR(Windows)のデバッグが楽しそうだった。

24時

2015-12-06 00:25:10: negainoido: 2050 (+200), QR puzzle (Windows)

by cympfh, isurugieri, autotaker

2015-12-06 00:48:04: negainoido: 2150 (+100), Steganography 1

by autotaker

このあと、tailedが途中まで書いてくれたQR(Web)のデバッグをcympfhとautotakerでやった。
バグはなおったが、strong-qr-decoderがうまく動かないため、とりあえず諦めた。

深夜

みんな自宅に帰った。TreeWalkerは解法が見えてしまったので、睡魔と闘いながらautotakerが解析した。

2015-12-06 06:18:30: negainoido: 2350 (+200), FSB: TreeWalker

by autotaker
明らかに時間かけすぎだった。寝るべきだった。

翌朝8時

2015-12-06 08:45:12: negainoido: 2400 (+50), Last Challenge (Thank you for playing)

by atetubou?

2015-12-06 08:47:28: negainoido: 2800 (+400), QR puzzle (Web)

by tailed
台湾勢が残しておいた問題を朝飯前に片付けてくれた。ありがたい。
atetubouとtailedはICPCのコンテストに出かけた。

午前中

2015-12-06 10:24:50: negainoido: 3000 (+200), Fragment2

by autotaker

2015-12-06 11:09:12: negainoido: 3100 (+100), 4042

by autotaker, garasubo, isurugieri, tailed
少し寝たら神託が降りてきてあっさり解けた。神に感謝したい。

コンテスト終了まで

この時点で方針の立っている問題がなくなってしまったので、autotaker, cympfh, garasuboの3人でHardware1を解きに行くことにした。LEDの配置さえわかればなんとかなるかと思っていたが、大量のトランジスタがあることに気づき、自分たちの無力を悟った。

結果

3100pts 26位だった。
f:id:autotaker:20151206172710p:plain
去年は3人で2000点くらいだったのでまあまあよくできたと思う。
日本人チームで9位なので学生枠で決勝に行けそう?

またatetubouとtailed(とflowlight氏)が参加していたICPCの方もなかなか良い結果だったようだ。

Template HaskellでJSONデコーダの導出

概要

最近、CodeRunnerというAIコンテストの予選BでJSONデータをいじる必要が出てきたのでHaskellJSONを読めるようにAesonを触ってみた。さらにTemplateHaskellを用いてレコード型の定義からJSONデコーダを自動導出できるようにしてみた。

背景

予選Bの問題は以下のリンクから閲覧できる。coderunner.jp

問題自体も面白いが、今回興味があるのはAPIで渡されるJSONデータである。
そのJSONは以下のような仕様になっている。

  • power: 現在の攻撃力
  • damage: 今までに与えた合計ダメージ
  • hp: 一番前の敵の体力
  • maxhp: 一番前の敵の初期体力
  • hps: 後ろにいる敵の体力の配列(戦う順に並んでいて最後に戦う敵が一番最後になる)
  • friend: 同じ部屋にいる自分以外のユーザーの配列(id昇順)
    • id: ユーザーID
    • power: そのユーザーの現在の攻撃力
    • damage: そのユーザーの今までに与えた合計ダメージ
  • log: イベントの配列(イベントは情報取得APIを前回リクエストしてから今回リクエストした間に起きたもののみを差分として表示する)
    • id: 攻撃したユーザーのユーザーID
    • enemy: 攻撃された敵のID(一番前の敵を含む残り敵数に等しい)
    • time: ためた時間[ミリ秒表記]
    • hp: 攻撃される前の敵の体力

このような構造はHaskellのレコード型を用いて自然に書くことができる。フィールド名にアンダースコアをつけているのは後でLensを使いたいからだ。

module Info where
data GameInfo = GameInfo { _myPower   :: Int
                         , _myDamage  :: Int
                         , _curHp     :: Int
                         , _maxHp     :: Int
                         , _hps       :: [Int]
                         , _friends   :: [Friend]
                         , _logs      :: [Log] }
                         deriving Show

data Friend = Friend { _friendId     :: String
                     , _friendPower  :: Int
                     , _friendDamage :: Int }
                     deriving Show

data Log = Log { _userId  :: String
               , _enemyId :: Int
               , _time    :: Int
               , _hp      :: Int }
               deriving Show

ここで問題となるのがフィールド名の衝突である。
例えばAPIの仕様では"id"というフィールド名はfriendの配列の中とlogの配列の中の両方で使われている。Haskellでは同じフィールド名を異なるレコード型に用いるためには別のファイルに記述しなければならず面倒である。同じファイルに定義する場合にはプリフィックスをつけるなどして適当に名前を変更しなければならない。

JSONのパーズ

JSONデータのパーズにはAesonというライブラリを使う。
aeson: Fast JSON parsing and encoding | Hackage
ライブラリに

decode :: FromJSON a => ByteString -> Maybe a

という関数があるので、GameInfo, Friend, LogのそれぞれをFromJSONのインスタンスにしてやれば良い。

{-# LANGUAGE OverloadedStrings #-}
import Data.Aeson
import Data.Aeson.Types

instance FromJSON Log where
    parseJSON (Object v) =
        Log <$> v .: "id"
            <*> v .: "enemy"
            <*> v .: "time"
            <*> v .: "hp"
    parseJSON invalid = typeMismatch "Log" invalid

instance FromJSON Friend where
    parseJSON (Object v) =
        Friend <$> v .: "id"
               <*> v .: "power"
               <*> v .: "damage"
    parseJSON invalid = typeMismatch "Friend" invalid

instance FromJSON GameInfo where
    parseJSON (Object v) =
        GameInfo <$> v .: "power"
                 <*> v .: "damage"
                 <*> v .: "hp"
                 <*> v .: "maxhp"
                 <*> v .: "hps"
                 <*> v .: "friend"
                 <*> v .: "log"
    parseJSON invalid = typeMismatch "GameInfo" invalid

簡単だし、typeMismatchとかいう関数を呼べばエラーメッセージもいい感じに出してくれる。
実際にパーズするのはこんな感じでできる。

import qualified Data.ByteString.Lazy as B
import Data.Aeson(eitherDecode)
import Text.Printf

testAeson :: FilePath -> (GameInfo -> IO ()) -> IO ()
testAeson path cont = do
    putStrLn $ "Case: " ++ path
    s <- B.readFile path
    case eitherDecode s of
        Left err -> putStrLn err
        Right info -> cont info

main = testAeson "sample.json" print
$ cat sample.json
{"power":2604996,"damage":40599634,"hp":13879712,"maxhp":39050001,"hps":[10857025,17480761,27899524],"friend":[{"id":"PlayerB","power":1542564,"damage":72452052},{"id":"PlayerC","power":1522756,"damage":52232156}],"log":[{"id":"PlayerC","enemy":4,"time":5017,"hp":39050001},{"id":"PlayerB","enemy":5,"time":5017,"hp":25158831},{"id":"PlayerA","enemy":5,"time":4265,"hp":43349056}]}

$ cat sample-e.json
{"power":2604996,"damage":40599634,"hp":13879712,"maxhp":39050001,"hps":[10857],"friend":[],"log":[0]}

$ ghci InfoTest.hs
GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help
[1 of 2] Compiling Info             ( Info.hs, interpreted )
[2 of 2] Compiling Main             ( InfoTest.hs, interpreted )
Ok, modules loaded: Info, Main.
*Main> testAeson "sample.json" print
Case: sample.json
GameInfo {_myPower = 2604996, _myDamage = 40599634, _curHp = 13879712, _maxHp = 39050001, _hps = [10857025,17480761,27899524], _friends = [Friend {_friendId = "PlayerB", _friendPower = 1542564, _friendDamage = 72452052},Friend {_friendId = "PlayerC", _friendPower = 1522756, _friendDamage = 52232156}], _logs = [Log {_userId = "PlayerC", _enemyId = 4, _time = 5017, _hp = 39050001},Log {_userId = "PlayerB", _enemyId = 5, _time = 5017, _hp = 25158831},Log {_userId = "PlayerA", _enemyId = 5, _time = 4265, _hp = 43349056}]}
*Main> testAeson "sample-e.json" print
Case: sample-e.json
Error in $.log[0]: failed to parse field log: expected Log, encountered Number

Template Haskellで自動導出

上のインスタンス宣言はレコード型のフィールド名とJSONオブジェクトのレコード名の対応関係さえ与えてやれば自動導出できそうなのでやってみた。
一応aesonのライブラリ自体にもGenericを用いた自動導出とTemplateHaskellを用いた自動導出があるのだが、それらはHaskellのデータ型をイイ感じのJSONにするのには向いていても、すでにあるJSON型をデコードするのにはあまり向いていないように見えた。

自動導出器はTemplate.hsに実装した。
使い方はこんな感じである。

{-# LANGUAGE TemplateHaskell #-}
module Info where
import Template

data Log = Log { _userId  :: String
               , _enemyId :: Int
               , _time    :: Int
               , _hp      :: Int }
               deriving Show

data Friend = Friend { _friendId     :: String
                     , _friendPower  :: Int
                     , _friendDamage :: Int }
                     deriving Show

data GameInfo = GameInfo { _myPower   :: Int
                         , _myDamage  :: Int
                         , _curHp     :: Int
                         , _maxHp     :: Int
                         , _hps       :: [Int]
                         , _friends   :: [Friend]
                         , _logs      :: [Log] }
                         deriving Show

mkFromJSON ''Log [ ('_userId,  "id")
                 , ('_enemyId, "enemy")
                 , ('_time,    "time")
                 , ('_hp,      "hp") ]

mkFromJSON ''Friend [ ('_friendId,     "id")
                    , ('_friendPower,  "power")
                    , ('_friendDamage, "damage") ]

mkFromJSON ''GameInfo [ ('_myPower,  "power")
                      , ('_myDamage, "damage")
                      , ('_curHp,    "hp")
                      , ('_maxHp,    "maxhp")
                      , ('_hps,      "hps")
                      , ('_friends,  "friend")
                      , ('_logs,     "log") ]

mkFromJSONというマクロがFromJSONのインスタンスを自動導出してくれる。第一引数には導出したい型の名前、第二引数にはフィールド名の対応関係を記したリストを渡せば良い。一応簡単なエラーハンドリングもしているのでフィールド名の漏れ等も検出して教えてくれるようになっている。

Template.hsの実装はこんな感じ。TemplateHaskell触ったのは初めてだったのでチュートリアル等を見ながらなんとなく実装した。QuasiQuote使いつつやればそんなに難しくもなかった。
これらのサイトが参考になった。
できる!Template Haskell (完) - はてな使ったら負けだと思っている deriving Haskell - haskell
Language.Haskell.TH.Syntax

{-# LANGUAGE TemplateHaskell #-}
module Template(mkFromJSON) where
import Language.Haskell.TH
import Data.Aeson
import Data.Aeson.Types
import qualified Data.Text as Text
import Control.Monad

validateInfo :: Name -> [(Name,String)] -> Q Name
validateInfo name fieldmap = do
    info <- reify name
    dec <- case info of
        TyConI dec -> return dec
        _ -> fail $ nameBase name ++ " must be a type constructor"
    cons <- case dec of
        DataD _ _ _ cons _ -> return cons
        _ -> fail $ nameBase name ++ " must be a data type"
    cnstr <- case cons of
        [cnstr] -> return cnstr
        _       -> fail $ nameBase name ++ " must have only one constructor"
    (cname,fields) <- case cnstr of
        RecC cname fields -> return (cname,map (\(x,_,_) -> x) fields)
        _ -> fail $ nameBase name ++ " must be a record type"
    mapM_ (\(field,_) -> unless (field `elem` fields) $
            fail $ "invalid field name" ++ nameBase field)
          fieldmap
    mapM_ (\field -> unless (field `elem` map fst fieldmap) $
            fail $ "corresponding JSON field of the field " ++ nameBase field ++ " is not found")
          fields
    return cname

mkFromJSON :: Name -> [(Name,String)] -> Q [Dec]
mkFromJSON name fieldmap = do
    cnstr <- validateInfo name fieldmap
    vars <- mapM (\y -> (,) y <$> newName "x") fieldmap
    v <- newName "v"
    let invalid = [| typeMismatch $(stringE $ nameBase name) $(varE v) |]
        -- body = do
        --    x1 <- v .: JSONfield1
        --    x2 <- v .: JSONfield2
        --    ...
        --    xn <- v .: JSONfieldn
        --    return $ $cnstr{ field1 = x1, ... fieldn = xn }
        body = doE (stmts ++ ret)
        stmts = [ bindS (varP tvar) [| $(varE v) .: Text.pack $(stringE jsonfield)|] 
                           | ((_,jsonfield),tvar) <- vars ]
        ret = [ noBindS (appE (varE 'return) (recConE cnstr fieldDefs)) ]
        fieldDefs = [ return (field, VarE tvar) | ((field,_),tvar) <- vars ]
    [d| instance FromJSON $(conT name) where
             parseJSON (Object $(varP v)) = $body
             parseJSON $(varP v)          = $invalid |]

終わりに

実装自体は出来たが、これでコードが短くなったかと言われれば微妙だ。
使う側にOverloadedStringsとかの拡張とかライブラリのインポートをしなくても良いのが便利かもしれない。