日々の流転

λ. Rouge(る〜じゅ)

Rubyで書いてるLispの簡単な処理系は、Rougeという名前にした。仕様とかいい加減だし、まだ基本的な部分しか実装出来てないけど、以下のような感じでそれなりに動くようになった。よしよし。

rouge> (setq hoge (let ((hoge "hoge")) (lambda () hoge)))
#<procedure>
rouge> (hoge)
"hoge"

λ. 5分で解けた問題の考察を書くために徹夜してる僕は馬鹿ですか? そうですか?、そうですよね。へへん、ばーか、ばーか。

λ. 圏論メモ

• determinant は natural transformation
• natural transformation は polymorphism と考えられる
• monad と自由代数(free algebra)

λ. 『イエスタディを歌って (1)』 冬目 景

を読んだ。

λ. 萩野服部研

「それは要するに『藤沢の歯医者』なんですよー」とか日記に書いてみるテスト

λ. 萩野服部研飲み

.

λ. Re: `→(-_☆ ) 視線!

そういえば、Rubyちゃんもポニーテールでしたっけ?

λ. 極限?

結局、

• 極限(limit) = 逆極限(inverse limit) = 射影極限(projective limit)
• 余極限(colimit) = 順極限(direct limit) = 帰納極限(inductive limit)

って事なのか。limit と inverse limit が同じものを指しているなんて、 なんて酷い名前付けなんだっ(泣)

【2006-04-23追記】檜山さんのグロッサランダム（Glossarandom）でも「75. ‘順極限（帰納的極限）’と‘逆極限（射影的極限）’という言葉がある。圏論的には、逆極限が‘極限’で順極限が‘余極限’、って、どういうことコレ？」と書いてあった。やっぱ、そう思うよなぁ。

λ. On coalgebra based on classes (J. Adámek, S. Milius, J.Velebil)

という論文を向井先生に紹介される。「Don't Be Afraid of Classes 」というフレーズが向井先生の心をとらえたらしい(笑)。それから、こないだメモしてまだ読んでいなかったFinal Coalgebras And a Solution Theorem for Arbitrary Endofunctors と同じ著者だった事に驚く。

λ. ヒキコモリ健康法

タイトルをみて爆笑してしまった。

λ. friday_night

今日もビリヤード。

λ. 夕食

豊田さんと久しぶりに豚菜に行こうかと思ったら、混んでいたので、倉吉でお好み焼き。食べたのは「もちチーズ玉」と「山かけ玉(豚肉のとろろのせ)」。お好み焼きにとろろがこんなに合うなんて知らなかった。

λ. ぬめぱと変態レィディオ24時間生放送

を聴きながらレポート書いてたりしたら、作業が全然進まなかった。あり得ない。

λ. PArrows

PArrows is an arrows based parsing combinator library written in Haskell. The library is similar to Parsec, but arrows allow for more future optimizations.

メモ。モナドではなくArrowsをベースにすれば、Swierstra and Duponcheel のテクニックを使ってより効率的なパーサを書ける(参照: "Generalising Monads to Arrows")。自分もArrowsベースのパーサを書いたことはあるけど、こいつはJavaScriptのソースを生成できるのが面白いな。

(2005-09-28 追記) PArrow は Swierstra and Duponcheel のテクニックは使ってなかった。じゃ、どうしてParsecよりも速いんだろう?

λ. 今週のデスノート

シドウたん頭悪すぎて可愛い。萌える。

λ. 『海辺のカフカ』 村上 春樹

を読んだ。

λ. 人狼審問 : (652)MMR出動だ！

ウケた。

λ. めがまり

良く出来てるなぁ。懐かしい。とりあえず、咲夜・うどんげ・チルノ・霊夢をこの順で倒した。キャラ二人分のライフゲージがあるせいか、ボス戦はそこまで辛くない。といっても、元のロックマン2をもう覚えてないんだけどね。技は、咲夜とチルノの技は魔理沙に、うどんげと霊夢の技はアリスに持たせた。そういえば、ロックマンのボスといえば弱点があるのがお約束のはずだけど、まだ弱点には出会ってない気がする。はて?

パスワードのメモ

●　　　　
　　　●●
●　●　　
●　　　●
●●●●　

λ. 余代数と余帰納法

2006-06-24で「coalgebra等の簡単な解説は近いうちに書こうと思います」と書いたが、このままだといつになっても書けそうにないので、とりあえず書き始めてみる。ちょっとずつ書き足していく予定。

代数と余代数

余代数は代数の双対……といっても何が何だかわかんないと思うので、まずは代数を考える。

代数は集合と演算と演算の満たす規則から構成される。例えば群。集合Gは、演算「e: G」「*: G×G->G」「_^-1: G->G」を持っていて、規則「(a*b)*c = a*(b*c)」「e*x = x」「a^-1*a = e」を満たすとき、群と呼ばれる。同様に集合Lは、演算「⊥: L」「∨: L×L→L」を持っていて、規則「a∨b = b∨a」「a∨(b∨c) = (a∨b)∨c」「a∨a = a」「a∨⊥ = a」を満たすとき、上半束と呼ばれる。これらを見ると、代数では演算はすべて値域がその集合になっていることがわかる(「演算に関して閉じている」という言い方をしたりする)。

圏論では関数の向きを逆向きにすることで双対を考えるので、値域ではなく定義域がその集合になっているような演算を集合に加えることが考えられる。これが余代数。

例) Kripkeモデル

Kripkeモデルは、ノードないしは「世界」の集合 W に、以下の二つの演算を加えた余代数と考えることが出来る。

• 各ノードからの到達可能性を定める関数 W -> ℘(W) と
• 各ノードで成り立つ原子命題の集合を定める関数 W -> ℘(A)

例) オートマトン

言語理論では言語の識別機械としてオートマトンが使われるが、Σをアルファベットの集合とすると、このオートマトンは集合 S に以下の二つの演算を加えた余代数と考えることが出来る。まあ、実際には初期状態も必要なので、この余代数自体ではなく、この余代数の要素をオートマトンと呼ぶべきかも。

• 文字を受け取って状態遷移するための関数 trans: S -> S^Σ
• 受理状態かを判断する関数 accept: S -> Bool

非決定性オートマトンにしたければ、trans: S -> S^Σ を trans: S -> ℘(S)^Σ にすれば良いし、さらにε遷移を許したければ ε: S -> ℘(S) という演算を加えればよい。

例) オートマトン (2)

後で使いたいので、もうちょっと単純なオートマトンも考えておく。 数字(自然数)を表示するディスプレイとボタン一つだけからなり、ボタンを押すと表示されている数字が切り替わるような、そんな機械があったとする。そうすると、この機械は状態の集合Sに以下の二つの演算を加えた余代数としてモデル化できる。

• 現在の数字を得る関数 value: S -> N
• ボタンを押したときに次の状態に遷移する関数 next: S -> S

始代数

余代数の例を幾つか紹介したところで話を代数に戻す。 また唐突だが、自然数全体の集合は、集合Nに以下の二つの演算を加えた代数と考えることが出来る。

• 0: N
• s: N->N

同じ種類の代数 (X, c:X, f:X->X) は他にいくらでも考えることが出来るけど、この (N,0,s) はその中でも「全ての要素が 0 と s の有限回の適用で一意に表記できる」という良い性質を持っている。これは直観的には「潰れていない(0 = s(n) が成り立ったりしない)」ことと「(0とsで表記できない)余計な要素を含んでいない」ことを意味している。

この性質があると嬉しいのは、再帰によって関数を定義することが出来、また(構造)帰納法による証明が出来る点。例えば、以下のような等式を満たす関数は唯一つするので、これによって関数hを定義することが出来る。

• h(0) = c
• h(s(n)) = f(h(n))

この等式を良く見ると、cを集合Xの要素、fをX->Xの関数として、この関数hは実は (N,0,s) から (X,c,f) への準同型になっている。圏論ではこのような「同じ種類の代数への準同型が一意に存在するような代数」のことを始代数(initial algebra)と呼ぶ。

(後で: 帰納法についても書く)

始代数の特徴とはある種の等式の集まりによって関数を定義することが出来、これはつまり「同じ種類の任意の代数への準同型が一意に存在する」ということだった。

(続く)

終余代数 (final coalgebra)

「同じ種類の任意の代数への準同型が一意に存在する」の双対を考えると、「同じ種類の任意の余代数からの準同型が一意に存在する」になる。 なんで、そんなものを考えるか。例えば、上の「オートマトン(2)」で考えた余代数だと、ある状態 s∈S から next を繰り返し適用していって表示される数字を集めると、value(s), value(next(s)), value(next(next(s)), ... という数列が出来るが、以下の二つの点から扱いにくい。

• 異なる s1,s2∈S が同じ数列を生成することがあるかもしれない。この機械を観察することでわかるのは結果の数列だけなので、観察から区別できないような状態が存在することがある。つまり、状態空間が冗長かも知れない。
• また、全ての数列が生成出来るとは限らない。つまり状態が足らないかも知れない。

これらの問題がない、ある意味理想的な余代数が終余代数(final coalgebra)で……

(続く)

λ. 『入門OCaml — プログラミング基礎と実践理解』

OCamlには以前挫折したが、最近またOCamlを使いだしたので、この本を読んでいる。

関連

• 入門OCaml 〜プログラミング基礎と実践理解 - サポートサイト
• ocaml-nagoya
• ITプランニング OCamlのページ

メモ。

p.60

直積型は、複数の型を積み上げて1つの型とすることを抽象化している。

積み上げる???

p.121 幽霊型の説明でいきなりconstraintキーワードってのが出てきて良くわからなかった。

あと、幽霊型と言われて私は James Cheney と Ralf Hinze の「Phantom Types」のようなものを想像したんだけど、違うのね。この論文を読み返したらこんな風に書いてあった。 なるほどなるほど。

The term phantom type was originally coined by Leijen and Meijer [17] to denote parameterized types that do not use their type argument(s). They use phantom types for type-safe embeddings of domain specific languages into Haskell. Their approach is, however, strictly more limited: while they can enforce type constraints when constructing values of a phantom type, they cannot make use of these constraints when decomposing a value. Our proposal exactly fills this gap.

p.157 「サブタイプへのキャストには “:>”演算子を使います」とあるけど、サブタイプではなくスーパータイプでは?

列多相(row polymorphism)。素朴な疑問なのだが、何故「行多相」ではなく「列多相」なのだろう?

p.161 の列多相性と比較されているJavaのコードが変。Javaでも(bounded polymorphism はあるし)普通に書けばダウンキャストは不要のはず。記述の簡潔さを除けば列多相の優位性を示せていないと思う。

class Base {};
class Sub1 extends Base { void cons(){} };
class Sub2 extends Base { void snoc(){} };

class Container<X extends Base> {
    X x;   
    Container(X x_) { x = x_; }
    X peek() { return x; }
};

Sub1 c = new Sub1();
Container<Sub1> container = new Container<Sub1>(c);
container.peek().cons();

Sub2 s = new Sub2();
Container<Sub2> container2 = new Container<Sub2>(s);
container2.peek().snoc();

λ. Erlangでリファレンスを実装

Erlangの並行処理は最低限以下の三つを知っていれば使えるようだ。

• プロセスの生成 Pid = spawn(Fun)
• メッセージの送信 Pid ! Message
• メッセージの受信 receive Pattern1 -> Expression1; Pattern2 -> Expression; ... end

これはちょー簡単で良さそうですな。 ということで、まずは試しに変更可能なリファレンスを作ってみた。

-module(ref).
-export([new/1, get/1, set/2]).

new(Val) ->
  {ref, spawn(fun () -> loop(Val) end)}.

loop(Val) ->
    receive
      {From, get} -> From!{self(), Val}, loop(Val);
      {set, NewVal} -> loop(NewVal)
    end.

get({ref, Pid}) ->
    Pid!{self(), get},
    receive
      {Pid, V} -> V
    end.

set({ref, Pid}, Val) -> Pid!{set, Val}, true.

使ってみると、ちゃんと変更可能なリファレンスとして振舞ってくれる。やった!

% erl
Eshell V5.6.3  (abort with ^G)
1> c(ref).
{ok,ref}
2> X=ref:new(1).
{ref,<0.46.0>}
3> ref:get(X).
1
4> ref:set(X, 2).
true
5> ref:get(X).
2
6> 

λ. LLTVのチケットを購入

今更ながら、LLTVのチケットを購入。

セブンイレブンで発見すれば、たまったQUOカードを消費できるかと思ったら、チケットの支払いは現金でないと出来ないらしい。しょぼーん。

λ. Shibuya.lisp テクニカルトーク#3

Shibuya.lisp テクニカルトーク#3に参加してきた。

今回参加するのにあたって、yad-ELさんの「参加者がやっぱり物見遊山的に見えてしまうんだよね」には、耳が痛かった。 というのも、私はLisp周りでアクティブに活動できているわけではないので、自分が参加することによって、Lisp周りでアクティブに活動されている方や、将来そうなる可能性のある人の席を奪ってしまっていたら申し訳ないので。 まあ、前回と違って、今回は翌日になっても席が埋まってなかったので、まあいっかと思って参加登録しちゃったけど。

(後で書く)

• 世界一短いコードでwebアプリ作成ができるフレームワーク開発 (松本 智行 さん)
• R5RS 完全準拠 JVM 日本語 Scheme インタプリタ 「Gino(仮)」(ilma さん)
• teepeedee2: fast IO in Lisp (John Fremlinさん / MSI)
• Inside c-wrapper (小黒 直樹 さん)
• (現場のScheme)と(Gaucheの進化) (川合 史朗 さん / Scheme Arts, LLC)
• Scheme on Ruby on Rails (Yuumi3さん / Gaucheファンクラブ)
• WebブラウザをインターネットOSのシェルにしてGaucheと対話する (源馬 照明 さん / 名古屋大学大学院多元数理科学研究科)
• 失敗したら会社終わるようなプロジェクトで本当にlispを使ってみた (mitamexさん)
• Emacs上での携帯絵文字の表示と入力補完 (IMAKADOさん / 面白法人KAYAC)

λ. 「掛け算から足し算を作る」を定理証明器で

檜山さんの「掛け算から足し算を作る（パズルとしてやってみよう）」の証明の部分を定理証明器に証明させてみようとしてみた……がうまくいかず。

SPASS で試してみたのが AGS.dfg で、The E Equational Theorem Prover(eprover) で試してみたのが AGS.tptp 。 どちらの場合でも、conjectureを一個ずつ試したところ、x+0=x と加算に関する逆元の存在はすぐに証明できるのだけど、他は組み合わせ爆発している感じ。 適当に補題を追加すればいいかと思ったけど、それでもそもそも公理の数が多いとダメみたい。 ……残念無念。

λ. CTF for ビギナーズ 2015 東京 に参加してきた。

CTF for ビギナーズ 2015 東京 に参加してきた。事前配布された資料を読んで比較的簡単そうという印象だったけれど、実際に講義で手を動かしてみたら良く身につきそうで、想像以上に良かった。

最後のCTF実践には「↻」という名前で参加。 16問中13問を解いて、4600点中3200点で、103人中6位だった。実際にCTFに参加するのもとても面白く、はまってしまう人が多いのも理解できた。講義で扱った範囲だけで楽しめる問題をこれだけ作るのは大変だったのではないかと思うし、運営の人たちには本当に感謝したい。

CTF問題メモ

以下、問題のメモを、解き方を忘れないうちに書いておく。 落ち着いて考えれば全問解けたのではないかと思うと、ちょっと悔しいが、初心者なのでまあ仕方ない。

問題1. 練習問題(まずはここから)(最初にこれを開く)(これを解いてから他の問題をやる) (その他 100)

フラグをsubmitする手順の練習問題。

問題2. Can you login as admin? (Web 100)

ユーザ名とファイル名を指定してログインするシステムで、SQLインジェクションを使ってadminでログインする。 講義でやったとおり「' OR 1=1; --」みたいなのを入れたら通った。

問題3. Find the flag (Web 200)

「Flag is hidden in HTTP traffic.」とあって、HTTPヘッダにフラグが書いてあったのだと思うけれど、詳細は忘れた。

問題4. 1M4G3 V13W3R (Web 300)

画像のアップローダが与えられていて、アップロードされた画像は「view.php?file=076b74f36eee552c.jpg」などのようなURLで参照されていた。 「view.php?file=ファイル名」中のファイル名を適当に書き換えると、どうも「images/ファイル名」からファイルを読んでいるようだったので、「view.php?file=../view.php」と「view.php?file=../index.php」でスクリプトをゲット、スクリプト中のコメントにフラグが書いてあった。

問題5. SQL Injection Level2 (Web 400)

SQLインジェクションの2問目。今度はユーザ名は適切にエスケープされていて、パスワード中にORは使えないそうな。 SQLには不慣れなので、SQLを想像して攻撃するのだと自分には難しいだろうなぁ、と思っていたけれど，適当な文字列をいれてログインを試したところ、実行されたSQLがヒントとして表示され、これなら何とかなるかなと思って考えてみる。

どうも「SELECT username FROM users WHERE username = 'ユーザ名' AND password = 'パスワード';」というようなSQLが実行されているようだったので、これは講義中にやったUNIONのやつだと思って試行錯誤。 不慣れなので何回か試したけれど、最終的にはパスワードに「' UNION SELECT 'admin'; --」的なやつを入れていけた。

後で解説を聞くと、ORは一回だけしか消去していなかったそうで、「OORR」とかしても良かったらしい。 しかし、よくよく考えてみると、パスワードにORという文字列が含まれてはいけないサイトって、サイトとしての根本的な機能に問題がある気が……

問題6. Universal Web Page(笑) (Web 500)

「?lang=en」で英語版、「?lang=ja」で日本語版が表示されるようなサイトが与えられていて、フラグはindex.phpに書かれているそうな。「en」や「ja」の部分を書き換えてみると、その名前のファイルをincludeしているらしいので、「?lang=index.php」としてみたが、どうもphpプログラムの実行エラーになってしまってファイルの中身自体は表示されず。 きっとPHPの変態的な機能を使うと、いけると思ったのだけれど、調べてもよく分からず、行き詰まった。

あとで解説を聞くと、「php://filter/convert.base64-encode/resource=」というのを使えばよかったらしく、事前講習資料ではこの機能についても説明されていたようだ。うぐぐ。 しかし、PHPは一体何を考えてincludeにこんな機能を用意しているのやら。 あと、CTFのために、そうでなければ(自分は)学ばないであろうPHPをあえて、しかもこんなマイナー機能を学ぶのもなぁ、という辺りでちょっとモヤモヤする。

問題7. Insecure Protocol (Network 100)

pcapファイルが与えられているので、Wiresharkで開くとTELNETだったのでFollow TCP Streamすると、パスワードがフラグになっていた。

問題8. Insecure Protocol 2 (Network 200)

pcapファイルが与えられており、Wiresharkで開くとTELNETで、こっちはログイン後にフラグが表示されている感じだけれど、肝心のフラグ部分がマスクされている。 対象のホストにtelnetで繋いでpcapファイル中のユーザ名とパスワードでログインするとフラグが表示された。 なんか、telnetコマンドの使い方でちょっとハマった。

問題9. File Transfer Protocol (Network 300)

pcapファイルが与えられており、Wiresharkで開くとftpの通信らしい。ファイルの一覧を表示後、1.txt, 2.zip, 3.txt というファイルをダウンロードしているようだったので、ftp-data でフィルタリングした後に、Export Select Packet Bytes で適当にファイルとして保存し、書かれていてた内容を連結してフラグをゲット。

問題10. This quiz is a NETWORK challenge (Network 400)

今度はpcapファイルではなくexeファイルが与えられている。 実行してみると謎のメッセージが表示される。 ネットワーク問題なので、どうせWiresharkで通信をキャプチャするんだろう、と思ってキャプチャしてみると、Basic認証付きで表示メッセージのデータを取得した後に、Basic認証無しでflag.txtにアクセスしようとして失敗していた。 なので、最初のBasic認証のデータを(base64デコードした上で)使って、ブラウザからflag.txtにアクセスしたらフラグが読めた。

問題11. Communication (Network 500)

pcapファイルが与えられていて、Wiresharkで開くとHTTPっぽかったので、 File → Export Objects → HTTP したところ、lime240.exe (LimeChat?)、rfc1459.txt (IRCのRFC)、trafficというファイルをダウンロードしていていた。trafficを保存するとこれはzipファイルになっていて、中からtraffic.pcapが出てきた。これをWiresharkで見てみるとIRCの通信っぽい。中に「ctf4b{ }」という文字列があるのは発見したが、この個数分の空白をとりあえずsubmitしても不正解、というところで時間切れ。

lime240.exeを保存した上で、それを使って traffic.pcap の中身に従って、IRCサーバに接続して同じことをしてみれば、マスクされていないフラグが表示されたのかな……多分。

問題12. NOT onion (Binary 100)

exeファイルが与えられていて、fileでgifファイルとわかったので、gifとして開いたらフラグが表示された。 画像ファイルからフラグを書き写すのが一番面倒くさい部分だった。

問題13. 読めますか？(Binary 200)

なんか表示できない変なpngファイルが与えられたので、とりあえずstringsしてctf4bでgrepしたらフラグをゲット。 pngとして表示できなかったのは、無理やりファイルを書きかえてpngとして不正なファイルになっていたためか?

問題15. READ and BURST (Binary 300)

アセンブリの実行結果を問う問題。 計算すれば良い。

問題16. DETECTIVE IDA (Binary 400)

謎のファイルが与えられていて、fileコマンドで判別するとexeファイルで、実行すると Passphrase を問われる。 IDA Pro 上で実行して Set IP で Passpharase の判定結果の分岐を正しい方に変更してみるも、文字化けした結果しか出力されず。 多分、パスフレーズのデータも使って復号化する形になっているのだろうと思い、IDA Pro の画面上のディスアセンブル結果でもパスフレーズっぽい文字列が表示されているのも見つけたが、IDA Pro の使い方がよくわからず、色々やっているうちに時間切れ。 後で解説を聞くと、文字列を照合する際の長さとかに注意して、ちゃんと追えばよかったらしい。

問題17. 5394 (Binary 500)

アセンブリの実行結果を問う問題その２。 ループを含む処理になっていて、手で考えるのが面倒臭かったので、とりあえずRubyに書き換えて実行し、フラグをゲット。

問題14?

あと、問題リストをよく見たら、14番めの問題が欠番になっていたことに気づいた。 ひょっとしてURLを書き換えてアクセスすると、隠し問題があったりしたんだろうか？

関連リンク

• CTF for ビギナーズ 東京 #ctf4b - Togetterまとめ
• CTF for ビギナーズ 東京の参加募集の一幕 - Togetterまとめ
• 発表申し込みした時の自分の投稿 (G+)