2012-03-24

Coq講義の感想など

@yoshihiro503 さんを講師とするCoq講義を受講しました。
感想などを書きます。


トップエスイー(http://www.topse.jp/wp/)の講義で、次のものでした。


トップエスイー特別講義「定理証明と検証」
http://topse.or.jp/docs/?q=node/36


講師は上にも書きましたが、
ITプランニングの今井宜洋さん ( @yoshihiro503 )です。


間違いや非公開情報などあれば、お手数ですがご指摘いただければと思います。



総論(感想)：
・活用できる度合いはドメインによる
　・ただちに強力に役立つ代表的なドメインはアルゴリズムの実装
　・入力に対して出力が満たす性質を定義したい場合も強いと思う
　・side effect は範囲外
・紙での証明が好き(得意)な人は楽しんで証明できると思います


できるようになったこと：
・Coq を使ったプログラミング
・Coq を使った証明(実装した関数が満たす性質の)
・Coq で実装したモジュールの多言語への Extract


定理証明系を活用した場合のメリット
・品質保証
　・ユニットテストでは保証できない「性質」を保証できる
　　・性質とテストケースの違いの本質の一つは無限か有限の違いだと思います
　　・満たすべき性質の列挙を漏らさないように考える必要はもちろんある
　　　・しかし性質を考えるのは個々のケースを考えるより楽しさを感じる(創造性を感じるワーク)
　　・ケースの列挙漏れの心配をせずに済むことはコストメリットを出せる可能性を感じる


定理証明系での難点
　・副作用を伴う処理は範囲外
　　・動的な性質はユニットテストの専売特許と考えられる
　・別言語での既存実装を証明したい、という場合は簡単ではない
　　・変換を含むので、変換ロジックの存在と、変換の妥当性という問題がある


講義で例として @yoshihiro503 さんの
迷路の最短路探索アルゴリズムの実装と、その正当性の証明の
ソースコード読みを行いました。参考資料に挙げておきます。


講義の後、力試しと演習のために、プログラミングCoqを読みつつ、
insertion sort の実装と証明をやってみました。
ところどころつまずくものの、だいたいは独力でできるようになりました。
SearchPattern が便利だと感じていて、証明は頭の中でも進めつつ、
これは成立している事実のはずだが Coq上ではまだ導出していない、
という事柄はSearchPattern を使えば必ずあるなぁ、と思いました。

一応書いたものを晒しておきます。
https://github.com/seizans/coqtest/blob/master/prog_coq/insertion_sort.v

これから作るものに generated by Coq なコードをねじ込んでいきたいと思います。



参考資料：
プログラミングCoq
http://www.iij-ii.co.jp/lab/techdoc/coqt/

迷路の最短経路探索アルゴリズムの実装と証明
https://bitbucket.org/yoshihiro503/maze_solver/src

Coq の証明駆動開発で Merge Sort 実装
http://d.hatena.ne.jp/yoshihiro503/20090923/p1

2012-02-05

Sessionless Authentication

※ 注意!！
この記事は半分厨二病的に自作セッション機構について考えたものです。
「体系的に学ぶ 安全なWebアプリケーションの作り方」(徳丸本)などなど、
自作のセッション管理機構は脆弱性の巣窟になるのでダメ絶対！！と言われています。
https://twitter.com/#!/ockeghem/status/62883095996661760
しかし、大規模Webアプリケーションでは必要になる気がしますし、
この手の情報がWeb上でパッと見つけられなかったので、
有害な記事になる可能性があることを承知しつつ公開しています。
議論、レビューの叩き台になれば良いという意図です。



RESTful なWebサービスは本当に作れるのか考えていました。
セッションがあるとスケールアウトできない気がして。(本当にできない？)

セッションレスが難しい。
セッションレスで認証と認可をどう実現すればよいのか。
セッションレスは正確に言うと、サーバ側でセッションオブジェクトを持たない、ということ。

でも認証情報(IdやisLogon)はどこかが持つ必要があるもの。
これをクライアント側(つまりはCookie)に持たせられるのか？

ちなみにサーバ側にキャッシュサーバを置けばスケールアウトするんじゃね？
という気もしたのですが、まあそれは置いておきます。


まず、普通にCookieにIDやisLogonのvalueを持たせてみます。
ダメです。
書き換えれば他人になれますし、好きにログインできます。

ということで、暗号化かハッシュ化でなんとかできないか考えます。
問題は、key や salt をどうするかです。
なぜなら、例えばkeyがみんな共通だった場合、そのkeyを知る人で悪い人がいたら終了です。
期間で区切って定期的にkey変更すれば大丈夫そうでもありますが、
1人にやぶられると何でもされるのが残念です。

ということで、key か salt を分けます。
salt とします。
ユーザごとに、ID や isLogon など、書き換えられると困る類の属性に対する salt を生成して永続化しておきます。
そしてクライアントに送るCookieは、属性値に、対応するsaltを付けた上でハッシュ化した値とします。
これで、もし誰かが自分のある属性値に対応するsaltを特定できたとしても、
他の属性値を書き換えることや、他人の値になることはできません。

でも実はこれでは、Cookie値そのものを記憶してしまえばログインできます。
結局いつもCookieの中身が同じだからです。
1回ログインして、そのときのIDとisLogonのCookie値を覚えておけば、
次回以降はログイン機能をバイパスしてログインするということもできます。
で、これだけだと必要なものがパスワードからCookie値に変わっただけで、
どのみちCookie値も基本的に本人しか知らないからあまり問題ないです。

しかしCookieが漏れた場合(XSS脆弱性があった場合など)ダメです。
この場合を含め、ログオフ機能のためにも、saltを変更する機能が必要です。


さらに例えば、何らかの所有権限の変更などがあった場合に問題があります。
もう今だとその値を取りえない、という値にしてしまうことが可能だからです。

というわけで対策したいです。
根本的対策１：権限情報の変更などの場合に、salt を変更する
保険的対策１：アプリケーション共通の salt を定期的に生成、変更する
Cookie値 = hash(isLogon, isLogonSalt, appSalt)
という関数にします。



以上、ぼくのかんがえたさいきょうのせっしょんでした。
(まじめな話、叩いたらオープンソースしたい)


※最後に再度注意！！
「自作のセッション管理機構は脆弱性の巣窟になるのでダメ絶対！！」
https://twitter.com/#!/ockeghem/status/62883095996661760

2012-02-05

Yesod the Web Framework on Haskell

Yesod the Web Framework on Haskell
での Web Application開発において、まずやると良いことをまとめておきます。


以下はあとでちゃんと整理します。未完でもあります。でもとりいそぎ共有しておきます。
このへんをやってみたソースをgithubに置いているので、必要に応じてご参照を。
https://github.com/seizans/yesoshiage/tree/master/yesoshiage


・導入マニュアルを見ながら yesod をインストールして scaffold を実行する
http://www.yesodweb.com/page/five-minutes
・Page(Resource) を増やす
　・config/routes で コンテキストパス と Resource と Method の対応を登録する
　　・Resource を書くことは、その名前の data constructor を書いたことになる
　・Resource × Method に対応する Handler を書く(ないとコンパイルエラー)
　　・命名は "getPage1R" のように、Method と Resource をつなげた名前(RはResourceのsuffix)
　　・defaultLayout $ do $( widgetFile "filename" )
　・上のfilenameのhtmlテンプレート(hamlet)ファイルを作成する templates/ 以下に
・DB
　・config/models と、DBテーブルを見て、関係を確認する
　　・sqlite3 [sqliteファイル名]：プロジェクトhomeにsqliteファイルができているはず
　　・SELECT * FROM SQLITE_MASTER;
　・SQLite にデータを入れる
　・DBのデータを取得して表示する
　　・テンプレート(hamlet)にデータを入れる：#{userIdent user}
　　・users <- runDB $ do u <- selectList return u
・Form を使う
　・Form を作る
　・Form の送信データを読み取る
・Session を使う

2012-02-01

暗号技術入門(続)

前回の認証技術の続き。
社内での勉強会用のスライドをアップしました。
基本的に、知らない人向けのものです。
暗号と認証の概要をざっくり総ざらいするためのものです。
概要は、それぞれの技術が、どのような問題を解決するのか、です。

Cryptography

Digital Signature and PKI

2012-01-26

認証の技術

社内での勉強会用のスライドを作成しました。
週次で、セキュリティ関連の技術を何かしら勉強する会です。
2回で認証の技術をやろうということで私が担当しました。
対象はセキュリティエンジニアではなく、普通の人なので、
ハイレベルなものではなく、入門の内容です。
認証(1)：一方向ハッシュ関数
認証(2)：メッセージ認証コード
認証(3)：デジタル署名
認証(4)：公開鍵基盤
章立てを見たらおわかりの方もいると思いますが、結城浩[著]の新版 暗号技術入門の解説です。
詳細の理解は、必要or興味ある人がやればよいと思います。
概要(どんな問題をどのように解決するか)は全員が知っているのが良いと思います。

一方向ハッシュ関数(One-way Hash Function)

メッセージ認証コード(Message Authentication Code)

2012-01-18

Python の関数で部分適用

久しぶりに Python をさわりました。
Amazon Web Services API 用に boto という Python Interface があったからです。
1年半ぶりくらいにさわってだいたい忘れていました。
が、Haskell をやってきたせいか、前より楽しく書けるようになっていました。
map、filter、reduce、lambda、リスト内包表記があって嬉しいです。

で、filter を使っていたのですが、filter に渡す関数を書くのが少し面倒。
毎回 lambda とか書くのが嫌だなー、と思ったんですね。
それで、Python の関数が部分適用を許せば楽に書けるのになぁ、と。

と思ったら標準ライブラリに一応あったみたいですね。(不勉強)

f を2変数関数として、
functools.partial(f, x)
と書くと、f の第一引数に x を適用した結果の関数が返されるというもの。

ということで書いてみました。
文字列を引数で渡して関数を返す関数。
返される関数は、次に引数で渡された文字列が、さっきの文字列引数を含むか判定する関数。

>>> import functools
>>> def contains(string):
...     return functools.partial(lambda s, obj: s in str(obj), string)
... 
>>> filter(contains("om"), ["omrice", "hogehoge", "homuhomu"])
['omrice', 'homuhomu']
2012-01-13

アルゴリズムイントロダクション 練習問題5.1-3

問題

0と1をそれぞれ確率1/2で出力する問題を考える。利用できるのは0か1かを出力する手続きBIASED-RANDOMである。BIASED-RANDOMは1を確率p、0を確率1-pで出力する(0

やっぱり実装まで。期待実行時間は出していない。あと証明もまだ(これはたぶんすぐできる)。
発想

  • PK戦のサドンデスで、先攻が勝ったら1、後攻が勝ったら0を返すとすればよい
public class Utility {
	public static boolean randomBoolean() {
		boolean a = true;
		boolean b = true;
		double p = 0.7;		// Any p is OK. s.t. 0 < p < 1
		while (!(a ^ b) ) {
			a = randomBooleanByProbability(p);
			b = randomBooleanByProbability(p);
		}
		return a;
	}

	// BIASED-RANDOM
	public static boolean randomBooleanByProbability(double p) {
		if (Math.random() < p ) return true;
		else return false;
	}
}
import static org.junit.Assert.*;
import org.junit.Test;
import com.gmail.seizans.algorithm.Utility;

public class UtilityTest {
	@Test
	public void randomBooleanTest() throws Exception {
		int numberOfTrials = 20000;
		double minProb = 0.95;
		double maxProb = 1.05;
		int counter = 0;
		boolean isOk = false;
		for (int i = 0; i < numberOfTrials; i++) {
			if (Utility.randomBoolean() ) counter++;
		}
		if (numberOfTrials * minProb < counter * 2 && counter * 2 < numberOfTrials * maxProb ) {
			isOk = true;
		}
		assertTrue(isOk);
	}
	
	@Test
	public void randomBooleanByProbabilityTest() throws Exception {
		double p = 0.66666;
		int numberOfTrials = 20000;
		double minProb = 0.95;
		double maxProb = 1.05;
		boolean isOk = false;
		int counter = 0;
		for (int i = 0; i < numberOfTrials; i++) {
			if (Utility.randomBooleanByProbability(p) ) counter++;
		}
		if (p * numberOfTrials * minProb < counter && counter < p * numberOfTrials * maxProb) {
			isOk = true;
		}
		assertTrue(isOk);
	}
}