FC2ブログ

プロフィール

大山恵弘

  • Author:大山恵弘
  • 公式なサイトはこちら

最近の記事

最近のコメント

最近のトラックバック

月別アーカイブ

ブロとも申請フォーム

ブログ内検索

RSSフィード

リンク

FC2カウンター

スポンサーサイト

上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

【ディペンダブル】 On the Challenge of Delivering High-Performance, Dependable, Model-Checked Internet Servers 【モデル検査】

In HotDep'05.
http://hotdep.org/2005/

ディペンダブルなサーバの構築に向けての取り組み。

題材はSSH v2。安全なSSH v2サーバを作る。

OCamlで実装してバッファオーバフローを排除する。
サーバがポリシーに従うことを静的にモデル検査で保証または動的検査で強制する。サーバの動きをオートマトンで表現して、それを検査。ポリシー記述には、C-likeな文法で非決定性有限オートマトンを表現するドメイン特化言語を利用。

ちょっと読んだ感じではSekarらのMCCに近い感じ。

SSHではなくメールサーバ・クライアントですけど、このへんも似た仕事をしてるかも。
スポンサーサイト

<< 【フック】 Detours: Binary Interception of Win32 Functions 【Windows】 | ホーム | 【モデル検査】 Automatic Discovery of API-Level Exploits 【セキュリティ】 >>


コメント

コメントの投稿


管理者にだけ表示を許可する

 BLOG TOP 


上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。