MacにZ3をインストールした。
新しいMacを手に入れたので環境構築を行っている。
その過程で、Z3のインストールにハマったので忘備録を書いておく。
目標
Z3はMicrosoftが開発しているSMTソルバで、様々な言語のバインディングがある。
公式でサポートしているのはC/C++, Java, Python, OCaml等でHaskellでは非公式のラッパーライブラリを用いる。
github.com
z3: Bindings for the Z3 Theorem Prover
トラブル
まず、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-haskellがmercurialで管理されていたのでしばらくプルリクの送り方を勉強してからにする予定である。
当分は問題の少なそうなコミットを適当に探した結果、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"だと配列アクセスの後、関数呼び出し。
実験
今回書いたソートのコードは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ポイント稼いでいて格の違いを見せつけてきました。(本当は運営がテストのため得点を入れていただけです)
決勝の形式について
学生大会の決勝は普段のJeopadyスタイルではなく、Attack&Defenceという形式でした。
決勝のシステムについて簡単に説明します。
- 各チームに一台サーバが用意される。
- 各サーバでは3つのWEBサービスを動かす。
- 得点はAttackポイントとDefenceポイントに分かれる。
試合経過
決勝開始と同時に各サーバへのアクセスが許可される。
ただし、各サーバの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インジェクション
- XSS
- ブログを表示する部分にXSSの脆弱性があった。この脆弱性を用いれば、運営がフラグを書きこんだ際にjavascriptを用いてフラグを自サーバにリークさせることが可能だと考えられる。適切にhtmlspecialcharsで囲うことで修正した。
この全てを対策したあとではアクセスログを読む限りvulnerable_blogを使ってフラグを奪われることはなかったように思えた。しかしながら、他のチームはどんどん自分のチームのフラグを奪ってAttackポイントを稼いでいた。
試合中にはその原因はついにわからなかったが、おそらくsboxのフラグを盗まれていたのだろう。
結果
negainoidoの最終結果は11位でした。Attackポイントは上位チームに引けを取らない数字だったのに、防衛が全く足りていなかったのが敗因でした。
初見殺しが多かったもののゲーム自体は面白かったと思います。
大会後の懇親会で振る舞われたお寿司は美味しかったです。
来年からは学生枠で参加するのは難しいですが、Attack&Defenceの経験が積めたのでまた機会があればより善戦できるはずです。
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のコードを書いて実験してみた。
$ 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
このコードを書いた時の私の気持ちはこうだ。
- 入力はデカイので末尾再帰にする必要がある。アキュムレータ引数を用意しよう。
- read_intのドキュメントにはファイルの末尾に達したら、End_of_file例外が投げられるとかいてある。tryで包んで例外を捉えよう。
- 例外の名前打ち込むの面倒だし、使い捨てのコードだから_でマッチさせてもいいよね!
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を当てたい。表示しているのはよく読むと
という等式のようだ。どう考えても、左辺+記号は*の間違いだろう。
つまり
となる、があたえられるわけだ。
ここから
つまり、を素因数分解すればの約数(素数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
よって、が得られた。
次に、
のを復元したい。これも簡単で、と求められる。
最後に
からと求められる。
離散対数はPARI/GPを用いた。
? znlog(3792102298388437469,Mod(2510510340, 6302662162225894921)) %1 = 1510490612
が求まったのでサーバに送れば良い。
FLAG: SECCON{SECCoooo_oooOooo_ooooooooN}
たぶん、想定解ではないが、いずれにせよ桁が小さすぎるのでどうやっても解けるとおもう。
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時
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
23時
24時
深夜
みんな自宅に帰った。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 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位だった。
去年は3人で2000点くらいだったのでまあまあよくできたと思う。
日本人チームで9位なので学生枠で決勝に行けそう?
またatetubouとtailed(とflowlight氏)が参加していたICPCの方もなかなか良い結果だったようだ。
Template HaskellでJSONデコーダの導出
概要
最近、CodeRunnerというAIコンテストの予選BでJSONデータをいじる必要が出てきたのでHaskellでJSONを読めるように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とかの拡張とかライブラリのインポートをしなくても良いのが便利かもしれない。