プロフィール

大山恵弘

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

最近の記事

最近のコメント

最近のトラックバック

月別アーカイブ

ブロとも申請フォーム

ブログ内検索

RSSフィード

リンク

FC2カウンター

スポンサーサイト

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

【セキュリティ】 Model Checking An Entire Linux Distribution for Security Violations 【モデル検査】

In ACSAC 2005.
http://www.cs.ucdavis.edu/~hchen/mops/

839パッケージ、6000万行からなるRH9 Linuxを、彼らのプログラム静的解析器MOPSでモデルチェックしましたって話。バグを108個見つけた。

ユーザはまず、セキュリティに関する性質を、システムコールや関数呼び出しなどの操作の遷移に関する有限状態オートマトンで表現する。するとMOPSがソースコードの全部のありうる実行パスを調べて、そのオートマトンの性質が成立するかどうかを検査する。保守的に警告を出すので偽陽性は出る。エラー報告機能を賢くしてそれに対応している。

本研究でチェックした性質は、TOCTTOU(バグ41個発見)、標準ファイルデスクリプタ(バグ22個発見)、一時ファイル(バグ34個発見)、strncpy(バグ11個発見)、chroot jail(バグ発見なし)、フォーマット文字列(バグは不明)の6つ。

セキュリティに関係する動作の遷移をオートマトンで表現して、それと実際のプログラムの挙動を比較する侵入検知システムは昔からたくさんある。いわゆるセキュリティオートマトン系の研究。この研究の新しいところは、そういう伝統的な研究と総当たりチェックを組み合わせたって点?
まあとにかくワグナーさんらしい研究という印象です。

静的でなく動的に、オートマトンと実際の実行を比較する研究としては、こんなのとかこんなのがあります。
スポンサーサイト

【仮想機械】 Diagnosing Performance Overheads in the Xen Virtual Machine Environment 【性能解析】

In VEE '05
http://www.usenix.org/publications/library/proceedings/vee05/

Xenのための統計的性能プロファイリングツールを作りました、そして、Xenのネットワーク処理のオーバヘッドを解析しましたって話。複数のVMの協調プロファイリングができる。

ツワエネポエルさんは最近こんな仕事もしてるのかと、そっちに驚き。

Virtual Multiprocessorにもこういうツールがあると、チューニングしやすいかもしれません。

| ホーム |


 BLOG TOP 


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