環境整備メモ

haskell vim

vimでhaskell書くためにやったことメモ。
初心者用。
Mac用。
やった結果はここです。
seizans/dotfiles · GitHub

ghc-mod は haskell 開発用のモジュールで、その vim プラグインを使いましょう。
Vim の開発環境
ghc-mod の Vim プラグイン ghcmod-vim を書いた - eagletmt's blog
ghc-mod の Vim プラグイン ghcmod-vim を書いた - eagletmt's blog
ghcmod.vim 0.1.0 - eagletmt's blog

(Emacsの人はたぶんこちら)
EmacsとGlossでお絵描きしてみるよ

やることはこちらに書いてあるような内容。
Bundleでghc-modをいれる方法 - プログラミングお勉強きろく
Vim-users.jp - Hack #238: neobundle.vim で plugin をモダンに管理する
VundleからNeoBundleへの移行 - SUGILOG

ざっくり言うと、
vim設定ファイルをgithubで管理して、
その設定ファイルでvimプラグインを管理する。
プラグインの中には別のgithubから持ってくる必要があるものもあって、
それは設定ファイルのレポジトリの中でsubmoduleとして管理する。

  • ~/.vimrc には source ~/dotfiles/vimrc とだけ書く
  • ~/dotfiles/vimrc に設定は書く。~/dotfiles は github で管理
  • 入れるプラグインを書いたら vim を1回立ち上げなおして :NeoBundleInstall
  • cd ~/.bundle/vimproc してから make -f make_mac.mak

これをやれば例えば、
Haskellファイル内でカーソル位置の変数の型を把握したければ、
:GhcModType とコマンドすればOK。
なのだけど、タイプするのが面倒なのでショートカットしたいですよね。

  • Ctrl + Space で :GhcModType を実行するために知ること

vim のkeymapでCtrl-Spaceが設定できなかったので調べてみた。 - dgdgの日記

keymapping 全体の解説は
Vim: Key mappingを極める - while (”im mirrored”);


このへんはまだ
Vim-users.jp - Hack #241: Haskellで使いたい関数を使ってからそのモジュールをimportする

Conduit に入門してみた

Haskell

昨日の朝に押上を出発して日本時間の翌日3時頃モルディブに到着しました。海が綺麗です。
移動時間が退屈だったのでFE覚醒をやっていたのですが、揺れながらのDSは私には少し難しい作業だったのであきらめて、流行りのConduitに入門してみました。

Conduit とは何か？

HaskellのIO系ライブラリで、IO関連のモジュールを理想的に分割するためのモノ、というのが私の認識です。
まだ見始めたばかりですが、以下のようなことが嬉しい気がします。

  • 生産、加工、消費、という分割をさせ、柔軟な合成をできる仕組み
  • リソース管理と処理を分割させ、コードが良い感じになる

より詳しくは他の資料をご覧いただければ。
現在私が認識している資料としては以下のものがあります。

とりあえずhackageのドキュメントを見つつ、いくつかコードを写経することにしました。
Conduitのバージョンは今日の段階では0.4.2ですが、上記の資料は前のバージョンのために動かなかったりしたので、0.4.2で動くようにしてみたという感じです。
Conduit作者のSnoymanさんのブログでは、今頑張ってテストしてる0.5をもうすぐリリースできるだろうとかいう話なのですが、とりあえずあげておきます。

サンプルコード断片

この2つの資料に載っているコードを写しました。
ghciでロードして関数を叩いてみると動きが見えると思います。

{-# LANGUAGE OverloadedStrings #-}                                                                                          
import Control.Monad.IO.Class (liftIO)
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import qualified Data.ByteString.Char8 as BC
import Data.Conduit
import qualified Data.Conduit.Binary as CB
import qualified Data.Conduit.List as CL
import Data.Monoid (mappend)

-- src に存在するファイル名を与えると dest で指定したファイル名にコピーする
copyFile :: FilePath -> FilePath -> IO ()
copyFile src dest = runResourceT $ CB.sourceFile src $$ CB.sinkFile dest

consumer :: Sink ByteString (ResourceT IO) ()
consumer = do
    mw <- CB.head
    case mw of
      Nothing -> return ()
      Just w  -> do
        liftIO . putStr $ "XXX "
        liftIO . BC.putStrLn . BS.singleton $ w
        consumer

consumer2 :: Sink ByteString (ResourceT IO) ()
consumer2 = do
    mw <- CB.head
    case mw of
      Nothing -> return ()
      Just w -> do
        liftIO . putStr $ "YYY "

        liftIO . BC.putStrLn . BS.singleton $ w

listFeeder :: Source (ResourceT IO) ByteString
listFeeder = CL.sourceList ["12", "34"]

fileFeeder :: Source (ResourceT IO) ByteString
fileFeeder = CB.sourceFile "File"

test1 :: IO ()
test1 = runResourceT $ listFeeder $$ consumer
test2 = runResourceT $ (listFeeder `mappend` fileFeeder) $$ consumer
test3 = runResourceT $ (listFeeder `mappend` fileFeeder) $$ (consumer2 >> consumer)
test4 = runResourceT $ listFeeder $$ CB.isolate 10 =$ consumer
test5 = runResourceT $ listFeeder $= CB.isolate 3 $$ consumer
Conduit で tail コマンド

これをまるっと写して 0.4.2 で動くようにしてみました。
runhaskell mytail.hs filename 15
とかやれば、
tail -n 15 filename
と同じ出力が得られます。

{-                                                                                                                           - 方針
 -  Sourceでは、seekして後ろから4096バイトずつ(又はファイルサイズの1/10バイトずつ)取得する。
 -  Conduitで、後ろからn個目の改行がある所までで入力を切る。
 -  Sinkは後ろから順に積んでいく。
 -}

import Control.Applicative ((<$>))
import Data.Monoid (mappend)
import Control.Monad (when)
import Control.Monad.IO.Class (liftIO)
import qualified Data.ByteString as BS
import qualified Data.ByteString.Char8 as BC
import Data.Conduit
import System.Environment (getArgs)
import qualified System.IO as SI

type FileSize = Integer

readLen :: FileSize -> Integer
readLen s
    | s < std  = std
    | otherwise = min limit x
  where
    x = s `div` 10
    std = 4096
    limit = 10 * 1024 * 1024


reverseFile :: MonadResource m => FilePath -> Source m BS.ByteString
reverseFile fp = sourceIO initialize close pull
  where
    initialize = do                                                                                                         
        h <- SI.openBinaryFile fp SI.ReadMode
        s <- readLen <$> SI.hFileSize h
        b <- SI.hIsSeekable h
        if b
          then do
            SI.hSeek h SI.SeekFromEnd (-1)
            return $ Just (h, s)
          else return Nothing
    close st@Nothing       = return ()
    close st@(Just (h, _)) = SI.hClose h
    pull  st@Nothing       = return IOClosed
    pull  st@(Just (h, l)) = do
        pos <- liftIO $ SI.hTell h
        if pos == 0
          then return IOClosed
          else do
            let len = min pos l
            liftIO $ SI.hSeek h SI.RelativeSeek (-len)
            x <- liftIO $ BS.hGetSome h $ fromIntegral len
            liftIO $ SI.hSeek h SI.RelativeSeek (-len)
            return $ IOOpen x

stackSink :: Monad m => Sink BS.ByteString m BS.ByteString
stackSink = sinkState BS.empty push close
  where
    close = return
    push st i = return (StateProcessing $ i `mappend` st)


limitLinesReverse :: Monad m => Int -> Conduit BS.ByteString m BS.ByteString
limitLinesReverse count = conduitState count push close
  where
    close _ = return []
    push 0 i = return (StateFinished (Just i) [])
    push n i = do
        let (n',bs) = loop n i
        if n' == 0
            then return (StateFinished Nothing [bs])
            else return (StateProducing n' [bs])
    loop n x
        | c <= n = (n - c, x)
        | c > n  = (0, BC.drop (pos - 1) x)
      where
        c = BC.count '\n' x
        pos = BC.elemIndices '\n' x !! (c - n)

main :: IO ()
main = do
    [fp, n] <- getArgs
    x <- runResourceT $ reverseFile fp $= limitLinesReverse (read n) $$ stackSink
    BC.putStrLn $ BC.drop 2 x

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

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

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 を使う

暗号技術入門(続)

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

Cryptography

Digital Signature and PKI

認証の技術

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

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

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