【IT】モデル検査手法を使ったウィンドウズの安定性を高めるデバイスドライバー検証ツールStatic Driver Verifier

『ウィンドウズ』の安定性を高めるドライバー検証ツール

　これまでに起こったウィンドウズのクラッシュの多くは、オペレーティング・システム(OS)
自体ではなく、デバイスドライバーのバグに起因することがわかっている。デバイスドライ
バーとはプログラムの下層にあって、キーボードやハードディスク、モニター、ネットワーク
カードのような周辺機器とOSとのやりとりを可能にするコードだ。

　デバイスドライバーはOSの中の深いところで動くため、コードを書くのも難しいし、デ
バッグも難しい。そしてデバイスドライバーが正しく動かないと、コンピューター全体が
止まる場合もある。米マイクロソフト社の基礎研究部門であるマイクロソフトリサーチの
研究員トム・ボール氏は「デバイスドライバーが正常に動かなければ、OS全体もおかしく
なる可能性がある」と語る。

　そんな中、世界最大のソフトウェア・バグ生産者であるマイクロソフト社は、ウィンドウズ
OSの安定性を大幅に向上させるためのバグ対策技術の開発に取り組んでいる。ワシン
トン州レドモンドにある同社の本拠地で進められてきた、このほとんど知られていないプ
ロジェクトが、やがては業界全体におけるソフトウェアの信頼性の水準を引き上げるかも
しれない。

　マイクロソフト社はすでに『Static Driver Verifier』(SDV：スタティック・ドライバー・
ベリファイアー)というドライバー検証ツールを開発している。SDVは「モデル検査」という
手法を使い、ウィンドウズ用デバイスドライバーのソースコードを分析して、ドライバーが
本来行なうべきことを数学的にモデル化したものと、プログラマーが書いたコードが一致
するかどうかを調べる。ドライバーがモデルと一致しない場合、SDVがドライバーにバグが
あるかもしれないと警告する。（中略）

　『スラム』というプロジェクトの一環としてマイクロソフトリサーチで研究が進められて
きたこの技術は、ゲイツ会長の発表から3年後、マイクロソフトリサーチを離れて開発者の
手に委ねられることになった。SDVは、プログラムが正しく実行されるかどうかを証明する
ことはできないが、多くのエラーを見つけ出すことはできる。こうしたエラーは今まで、
プログラム開発過程でのチェックをくぐり抜け、顧客を悩ませ続けてきた。

　スラム・プロジェクトをスリラム・ラジャマーニ氏とともに率いてきたボール氏は「SDVは
ランタイム分析ではなく、コードの静的分析(コンパイル時分析)を通じてバグを見つける」
と説明した。一般的なドライバーなら数分でチェックが完了するが、複雑なものでは分析に
20分もかかることがある。「SDVが見つけるバグの多くは実際のバグだが、静的分析である
ため、誤ってバグと報告することもあり得る」（中略）

　モデル検査はデバイスドライバーでは有効だが万能薬ではない。少なくとも『Microsoft
Word』(マイクロソフト・ワード)や米アドビシステムズ社の『Acrobat』(アクロバット)のような
複雑なプログラムでは機能しない。これらのプログラムが実際に行なうはずの動作を
形式化することは、非常に難しいためだ。

　こうした複雑で大がかりなアプリケーションについては、一部の専門家は、モデル検査
ではなく、ソースコードをスキャンして一般的なミスを探す特別なプログラム・チェッカー
に着目している。

　そうした自動コード分析ソフトウェアの1つが、米アウンス・ラブズ社の『プレクシス』
(Prexis)だ。同社の創立者であるジャック・ダナヒー最高技術責任者(CTO)は「われわれ
の製品は、単にバグを探すのではない」と話す。プレクシスはセキュリティーの問題――
たとえば、大切な情報を暗号化せずにネットワークに送ってしまうプログラムなど――
につながる設計上のミスも検知するという。（略）

記事全文、関連ニュース、リンク等はこちらです。
Hotwired Japan/Simson Garfinkel 日本語版：藤原聡美／高森郁哉　2005年11月10日
http://hotwired.goo.ne.jp/news/20051116304.html

関連スレ
【IT】状態遷移表モデル設計だけでモデル検査技術の利用を可能にする次世代モデルベース開発
http://news18.2ch.net/test/read.cgi/scienceplus/1119790521/

2げｔ

デスドライバーにみえた

　すまん、誰か2行ぐらいに訳してくれ。

>>4
まだまだ開発中

どうせＭＳ純正ドライバでもひっかかるんだろ？

関連スレ追加です。

NTT、高信頼性Linuxシステムを実現する新ファイルシステム「NILFS」を公開
http://news18.2ch.net/test/read.cgi/scienceplus/1127755789/
【スパコン】マイクロソフトがスーパーコンピュータ向けOS参入
http://news18.2ch.net/test/read.cgi/scienceplus/1132204432/

とりあえずデバイスドライバにリング0権限を与えるの止めればいいと思うよ。

そんなことより、ちゃんとドキュメントまとめとけよ。
WindowsCEのドライバ書いているんだが、必要な情報が巨大なドキュメント内の
あちこちに飛び散ってて解かり辛いったらありゃしない。
実装すべきものが一通り揃っているか激しく不安なんだが。

どうせそのSDVとやらにもバグがあるんだろ

ウホッ IDがDLL
欝だ・・・