文献

J-GLOBAL ID：200902258172159590   整理番号：09A0079037

仮想機械デバイスドライバ検証の一考察

A Study of Formal Verification of Device Drivers for a Virtual Machine

著者 (5件)： 八木勲 (奈良先端科学技術大学院大) ,  河合栄治 (奈良先端科学技術大学院大) ,  関浩之 (奈良先端科学技術大学院大) ,  品川高廣 (筑波大) ,  加藤和彦 (筑波大)
資料名： 情報処理学会研究報告  (IPSJ SIG Technical Reports)
巻： 2008  号： 122(CSEC-43)  ページ： 37-42  発行年： 2008年11月28日 
JST資料番号： Z0031B  ISSN： 0919-6072  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 近年情報漏洩をはじめとするセキュリティ問題が多数発生している。情報漏洩を防ぐ手段の1つとして,我々はセキュリティ機能を強化した仮想マシンモニタBitVisorを開発している。本稿ではBitVisorのデバイスドライバ検証法について考察する。手始めに,BitVisorのIDEデバイスドライバにおけるセキュリティ機能(データ暗号化機能)の安全性をモデル検査にて検証し,その有効性を確認した。そして検証で得られた知見や既存技術に関する情報を交えながらデバイスドライバの検証法の見通しについて議論する。(著者抄録)

シソーラス用語： *コンピュータセキュリティ ,  情報 ,  計算機プログラム ,  *仮想機械システム ,  オペレーティングシステム ,  暗号 ,  *モデル検査
準シソーラス用語： *デバイスドライバ ,  暗号化 ,  *仮想マシンモニター ,  情報漏洩

分類 (3件)： データ保護  (JD01020V) ,  オペレーティングシステム  (JD03020J) ,  計算理論  (JB02000A)

引用文献 (8件)：

• セキュアVMプロジェクト. http://www.securevm.org/abs.html
• 品川高廣. 準パススルー型仮想マシンモニタ BitVisor の設計と実装. 2008年並列/分散/協調処理に関する『佐賀』サマー・ワークショップ (SWoPP佐賀2008), 佐賀, 8月. 2008
• BALL, T. Thorough Static Analysis of Device Drivers. Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006. 2006, 40, 4, 73-85
• WITKOWSKI, T. Model Checking Concurrent Linux Device Drivers. Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering, 2007. 2007, 501-504
• Information Technology-AT Attachment with Packet Interface-7-(ATA/ATAPI-7). ANSI INCITS 397-2005. 2005

タイトルに関連する用語 (3件)： 仮想機械 ,  デバイスドライバ ,  検証