計算機、デバイス管理方法、プログラム、及び記録媒体
【課題】安全に稼働させられる計算機を提供する。
【解決手段】
ハイパーバイザ部２００は仮想化レイヤにて動作し、仮想マシン３００内のゲストＯＳであるＯＳ部２２０を動作させる。システムモニタ部２１０は、仮想化レイヤにてデバイスの状態遷移を管理する。システムモニタ部２１０は、ドライバ部２４０がデバイスのハードウェアの仕様に従ったアクセスを行わない場合、ハイパーバイザ部２００に報知する。また、モデル検査部２３０は、ドライバ部２４０がデバイスのハードウェアの仕様に従ったアクセスを行うか、オートマトンの状態遷移により検査して認証する。
【解決手段】
ハイパーバイザ部２００は仮想化レイヤにて動作し、仮想マシン３００内のゲストＯＳであるＯＳ部２２０を動作させる。システムモニタ部２１０は、仮想化レイヤにてデバイスの状態遷移を管理する。システムモニタ部２１０は、ドライバ部２４０がデバイスのハードウェアの仕様に従ったアクセスを行わない場合、ハイパーバイザ部２００に報知する。また、モデル検査部２３０は、ドライバ部２４０がデバイスのハードウェアの仕様に従ったアクセスを行うか、オートマトンの状態遷移により検査して認証する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、計算機、デバイス管理方法、プログラム、及び記録媒体に係り、特に仮想化環境でデバイスの管理を行う計算機、デバイス管理方法、プログラム、及び記録媒体に関する。
【背景技術】
【０００２】
近年、コンピュータが社会の様々な環境で用いられるようになっている。このため、ソフトウェアのミス（バグ）や悪意あるソフトウェアにより、コンピュータの動作停止を防ぐ技術が重要となっている。
ここで、コンピュータはデバイスドライバ（ドライバ）と呼ばれるソフトウェアを用いて、コンピュータ内部の装置や周辺機器等である各デバイスを制御している。
このデバイスドライバにミスがあり、ハードウェアの仕様に沿わないアクセスを行うと、当該デバイスがエラー状態となり反応しなくなることがある。この場合、コンピュータのシステムをリセット等する必要があり、常に稼働することが必要なコンピュータでは都合が悪い。
【０００３】
このため、従来からデバイスドライバそのものを検証する技術が存在した。このような従来のドライバの検証技術として、非特許文献１を参照すると、ホーア論理を用いてデバイスのアクセスの正しさを証明する技術が記載されている（以下、従来技術１とする。）。
このようなホーア論理を用いてデバイスドライバを行うことで、多くの演算処理が必要なものの、ソースコードのあるデバイスへのアクセスの操作が正しいことを保証することができる。
【０００４】
一方、従来からハードウェア環境を抽象化して実行する仮想化（Ｖｉｒｔｕａｌｉｚａｔｉｏｎ）技術が用いられてきた。
このような仮想化技術により、仮想化されたゲストＯＳ（Ｇｕｅｓｔ Ｏｐｅｒａｔｉｎｇ Ｓｙｓｔｅｍ）を隔離した環境で実行できる。つまり、仮想化技術では、ゲストＯＳからのデバイスへのアクセスについて、各機器をエミュレーションにより管理して実行する。
これにより、コンピュータ全体の停止を防ぐことができる。よって、仮想化技術を用いることで、より動作停止が少ない安全なコンピュータ・システムを構築することができる。
【０００５】
ここで、従来の仮想化技術を用いたデバイスドライバの管理技術として、特許文献１を参照すると、少なくとも一つのデバイスドライバを含むドメインを多数個具備するドメイン部と、デバイスのハードウェアを構成するシステム資源部、及びＤＭＡ（Ｄｉｒｅｃｔ Ｍｅｍｏｒｙ Ａｃｃｅｓｓ）ドライバ、及び仮想化環境で前記システム資源部に対する前記ドメイン部の接近動作を制御する接近制御モジュールを具備する制御部を含む仮想化環境での安全なシステム保護装置の技術が開示されている（以下、従来技術２とする。）。
従来技術２のシステム保護装置によれば、仮想化環境で悪性コード（ｍａｌｗａｒｅ）など悪意のある接近からシステム資源を保護し、システム障害を解決して安全なサービスを保障することができる。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２００８−２６９５８９号公報
【非特許文献】
【０００７】
【非特許文献１】Ｊｉａｎｊｕｎ Ｄｕａｎ、「Ｃｏｒｒｅｃｔｎｅｓｓ Ｐｒｏｏｆｓ ｆｏｒ Ｄｅｖｉｃｅ Ｄｒｉｖｅｒｓ ｉｎ Ｅｍｂｅｄｄｅｄ Ｓｙｓｔｅｍｓ」、ＵＳＥＮＩＸ ｔｈｅ ５ｔｈ ｉｎｔｅｒｎａｔｉｏｎａｌ ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｓｙｓｔｅｍｓ ｓｏｆｔｗａｒｅ ｖｅｒｉｆｉｃａｔｉｏｎ、２０１０年１０月６日、、インターネット〈URL：http://www.usenix.org/event/ssv10/tech/full_papers/Duan.pdf〉
【発明の概要】
【発明が解決しようとする課題】
【０００８】
しかしながら、従来技術１のソースコードの検査では、ソースコードのない市販ＯＳについてのデバイスの管理を行うことができなかった。
また、従来技術２のシステム保護装置においては、仮想化環境でシステム資源に対して仮想マシンであるドメインの接近動作を制御する接近制御モジュールを備えていた。しかしながら、この接近制御モジュールは、安全なドメインがハードウェア資源に接近することを許容する（段落［００３０］等を参照）だけで、当該ハードウェア資源であるデバイスの状態が不正になるか否かについて判断することはできなかった。このため、安全と判断されたドメインにおけるドライバのバグ等により不正なアクセスがあった場合の安全性を保証できなかった。
【０００９】
本発明は、このような状況に鑑みてなされたものであり、上述の課題を解消することを課題とする。
【課題を解決するための手段】
【００１０】
本発明の計算機は、仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ部と、デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ部に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ部とを備えることを特徴とする。
本発明の計算機は、前記ゲストＯＳの前記デバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行うかを、オートマトンの状態遷移により検査して認証するモデル検査部を備えることを特徴とする。
本発明の計算機は、前記システムモニタ部は、前記モデル検査部で認証されたデバイスドライバからの直接アクセスがあった場合、負荷を抑えて前記デバイスにアクセスさせることを特徴とする。
本発明の計算機は、前記システムモニタ部は、前記モデル検査部で用いた前記オートマトンにより、前記ハードウェアの仕様に従ったアクセスを行うか否かフィルタリングすることを特徴とする。
本発明の計算機は、前記システムモニタ部は、前記認証されたデバイスドライバが前記デバイスのアクセスをした際に、前記デバイスの状態遷移が不正であった場合には、前記デバイスの故障と検知することを特徴とする。
本発明の計算機デバイス管理方法は、コンピュータのデバイスの状態遷移を管理するデバイス管理方法において、前記コンピュータは、仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、仮想化レイヤにて前記デバイスの管理を行うシステムモニタ手段とを備え、前記システムモニタ手段により、前記デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知することを特徴とする。
本発明のプログラムは、コンピュータを、仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段として機能させるためのプログラムであることを特徴とする。
本発明の記録媒体は、コンピュータを、仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段として機能させるためのプログラムを記録したコンピュータ読み取り可能な記録媒体であることを特徴とする。
【発明の効果】
【００１１】
本発明によれば、デバイスのアクセスを仮想化レイヤで管理することで、ソースコードのない市販ＯＳでも、デバイスの状態遷移を管理するコンピュータを提供することができる。
また、本発明によれば、デバイスドライバがデバイスのハードウェアの仕様に従ったアクセスを行うかシステムモニタで管理することで、仮想マシンからのデバイスへのアクセスの安全性を保証するコンピュータを提供することができる。
【図面の簡単な説明】
【００１２】
【図１】本発明の実施の形態に係るコンピュータ１０の制御構成を示すブロック図である。
【図２】本発明の実施の形態に係るデバイス状態遷移管理処理のフローチャートである。
【図３】本発明の実施の形態に係るドライバチェック処理のフローチャートである。
【図４Ａ】本発明の実施の形態に係るシリアルドライバの送信時のモデル検査の概念図である。
【図４Ｂ】本発明の実施の形態に係るシリアルドライバの受信時のモデル検査の概念図である。
【図５】本発明の実施の形態に係るモデル検査処理の画面例である。
【図６】本発明の実施の形態に係るシステムモニタ処理の概念図である。
【図７】本発明の実施の形態に係るシステムモニタ処理のフローチャートである。
【発明を実施するための形態】
【００１３】
＜実施の形態＞
〔コンピュータ１０の構成〕
図１を参照して、本発明の実施の形態に係るコンピュータ１０（計算機）の構成について説明する。
コンピュータ１０は、主にＭＡＣ規格機やＰＣ／ＡＴ互換機等のＰＣ（Ｐｅｒｓｏｎａｌ Ｃｏｍｐｕｔｅｒ）、サーバ、汎用機、携帯電話、スマートフォン、ＰＤＡ（Ｐｅｒｓｏｎａｌ Ｄａｔａ Ａｓｓｉｓｔａｎｔ）、モバイル端末、セットトップボックス、ネットワーク接続機能付きテレビジョン、デジタル画像・音声再生用のメディアプレーヤー、ゲーム機等であり、ＯＳ（Ｏｐｅｒａｔｉｎｇ Ｓｙｓｔｅｍ）の機能を用いて各種プログラムを実行可能である。
また、コンピュータ１０は、本実施形態に係るデバイス状態遷移管理処理を実行するためのハードウェア資源である。このため、コンピュータ１０は、制御部１００と、主記憶部１１０と、補助記憶部１２０と、チップセット１５０とを備えている。
制御部１００は、ＣＰＵ（Ｃｅｎｔｒａｌ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ、中央処理装置）やＧＰＵ（Ｇｒａｐｈｉｃ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）やＤＳＰ（Ｄｉｇｉｔａｌ Ｓｉｇｎａｌ Ｐｒｏｃｅｓｓｏｒ）等の制御手段である。制御部１００は、インテル社製のインテル・バーチャライゼーション・テクノロジー（Ｉｎｔｅｌ ＶＴ）又はＡＭＤ社製のＡＭＤ−Ｖのような、仮想化支援機構を備えていてもよい。また、制御部１００は、ＤＲＡＭのインターフェイス等を備えて、主記憶部１１０に直接アクセスするような構成を用いることが可能である。
主記憶部１１０は、ＤＲＡＭ（Ｄｙｎａｍｉｃ Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ）、ＤＤＲ２／３／４−ＳＤＲＡＭ、ＸＤ−ＲＡＭ、ＳＲＡＭ（Ｓｔａｔｉｃ ＲＡＭ）等の主記憶手段である。
補助記憶部１２０は、ＨＤＤ（Ｈａｒｄ Ｄｉｓｋ Ｄｒｉｖｅ）やフラッシュメモリや光学ドライブ等の補助記憶手段である。
チップセット１５０は、コンピュータ１０の各部位と、他の周辺機器やネットワーク等のデバイスとを接続するためのバスアービタや各種Ｉ／Ｏチップ等を備える周辺機器接続インターフェイス手段である。チップセット１５０が接続する周辺機器としては、表示部と、音声入出力部と、入力部とを含む。表示部は、ＬＥＤ（Ｌｉｇｈｔ Ｅｍｉｔｔｉｎｇ Ｄｉｏｄｅ）、ＬＣＤ（Ｌｉｑｕｉｄ Ｃｒｙｓｔａｌ Ｄｉｓｐｌａｙ）、ＰＤＰ（ＰＰｌａｓｍａ Ｄｉｓｐｌａｙ Ｐａｎｅｌ）、プロジェクタ等を用いることができる。入力部は、キーボード、トラックボール、タッチパネル、マウス等のポインティングデバイスを含む。チップセット１５０が接続するネットワークとしては、ＬＡＮ（Ｌｏｃａｌ Ａｒｅａ Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ Ａｒｅａ Ｎｅｔｗｏｒｋ）、携帯網や無線ＬＡＮ等の各種無線ネットワークを含む。
【００１４】
また、補助記憶部１２０は、ハイパーバイザ部２００（ハイパーバイザ手段）、システムモニタ部２１０（システムモニタ手段）、ＯＳ部２２０（ゲストＯＳ）、モデル検査部２３０（モデル検査手段）、ドライバ部２４０（デバイスドライバ、ドライバ）、及びアプリケーション部２５０（アプリケーション手段）を記憶している。これらの部位は、適宜、制御部１００により主記憶部１１０に読み出されて実行される。また、ＯＳ部２２０、モデル検査部２３０、ドライバ部２４０、及びアプリケーション部２５０は、ハイパーバイザ部２００により実行される仮想マシン３００を構成している。
なお、補助記憶部１２０は、ＨＤＤ等に記憶された上述の各部位の他に、コンピュータ１０のファームウェアやＢＩＯＳ（Ｂａｓｉｃ Ｉｎｐｕｔ／Ｏｕｔｐｕｔ Ｓｙｓｔｅｍ）等を含んでいる。これらについても、適宜、制御部１００により主記憶部１１０に読み出されて実行される。
【００１５】
ハイパーバイザ部２００は、コンピュータの仮想化技術のひとつであるバーチャルマシン（仮想機械）を実現するためのバーチャリゼーション（仮想化）レイヤ（Ｌａｙｅｒ）を構成する仮想化モニタ等の制御プログラムの部位である。すなわち、ハイパーバイザ部２００は、制御部１００に、ゲストＯＳであるＯＳ部２２０を含む仮想マシン３００を実行させるハイパーバイザである。ハイパーバイザ部２００は、複数の仮想マシン３００に、制御部１００の演算資源、メモリ資源等を効率的にスケジューリングし、ハードウェア割り込み等を用いてデバイスにアクセスする。
ハイパーバイザ部２００は、ホストＯＳを必要とせず、コンピュータ１０の主記憶部１１０に読み出されて、ハードウェア資源を用いて直接実行されるＴｙｐｅ １（ネイティブ、Ｎａｔｉｖｅ、ベアメタル、Ｂａｒｅ Ｍｅｔａｌ）方式を用いることができる。
また、ハイパーバイザ部２００は、仮想マシンのエミュレーションにより仮想化されたデバイス（以下、仮想デバイスという。）のデバイスドライバや、チップセット１５０に接続された物理的なデバイス（以下、物理デバイスという。）用のデバイスドライバを備えることができる。ハイパーバイザ部２００は、仮想マシン３００内のドライバ部２４０に対し、仮想デバイスへのアクセスに加えて、準仮想化されたデバイスへのアクセスを行わせることができる。ここで、準仮想化とは、「パラレル（平行）アクセス」又はベアメタル等と呼ばれる「直接アクセス方式」を用いて、物理デバイスにマッピングされたデバイスのメモリやＩ／Ｏに対して直接アクセスを行うことをいう。この準仮想化により、デバイスのエミュレーションのオーバーヘッド（処理遅延）を抑えることができ、リアルタイム（実時間）処理が必要なネットワーク処理やレンダリング処理等に用いることができる。
なお、ハイパーバイザ部２００として、ホストＯＳ上で動作するＴｙｐｅ ２方式の仮想化のハイパーバイザについても用いることもできる。
【００１６】
システムモニタ部２１０は、ハイパーバイザ部２２０と協同して、仮想化レイヤ上で動作するコマンド列のフィルタ等のプログラムの部位である。
システムモニタ部２１０は、仮想化レイヤにおいて、デバイスドライバとは独立に、デバイスへの操作を管理する。つまり、システムモニタ部２１０は、ＯＳ部２２０であるゲストＯＳによるデバイスの状態の遷移を仮想化レイヤにて監視し、デバイスが利用不可能となるような不正なＩ／Ｏコマンド列等（以下、不正コマンドという。）を検知する。システムモニタ部２１０は、不正コマンドの検知が行われた場合、ＯＳ部２２０の当該ゲストＯＳの停止又は当該ゲストＯＳによるそのデバイスの利用を停止する。これにより、システムモニタ部２１０は、デバイスが利用不可能となることを防ぐことができる。このように、システムモニタ部２１０は、デバイスドライバ自体を検証の対象としないため、ソースコードが入手できない商用（市販）ＯＳであるゲストＯＳにも適用することができる。また、システムモニタ部２１０は、ＯＳ部２２０のゲストＯＳのカーネルが、複数回単一のデバイスに対し操作を行った場合でも、不正な操作によりデバイスが利用不可能になることを防ぐことができる。
また、システムモニタ部２１０は、モデル検査部２３０にて動作の認証を行ったドライバ部２４０からの直接アクセスについては、Ｉ／Ｏコマンド列等の監視を行わないか、負荷を抑えた監視を行うように構成することができる。
また、システムモニタ部２１０は、このデバイスの状態の遷移について、上述したデバイスドライバのソースコードを基に、不正コマンドの監視ができる。また、システムモニタ部２１０は、チップセット１５０を介してデバイスの状態を直接監視することも可能である。この際、システムモニタ部２１０は、デバイスが正常なＩ／Ｏコマンド列により正常でない状態に遷移したことを検知して、デバイスの故障や不具合を認識することもできる。
【００１７】
モデル検査部２３０は、ソースコード等のソフトウェアのプログラムを読み、実行経路をすべて調査し、規定されたプロパティ（条件）が満たされるかどうかソフトウェアモデル（以下、モデルという。）のチェック（検査）を行うプログラムやデータの部位である。
モデル検査部は、主にゲストＯＳであるＯＳ部２２０に用いるドライバ部２４０のソースコードを用いて、このモデル検査（チェック）を行う。具体的には、モデル検査部２３０は、ドライバ部２４０のデバイスドライバのソースコードに記載されたオートマトン形式で記載されたデバイスの状態遷移の記載を基に、ソースコードとの整合性がとれているかどうかを検証するモデル検査を行う。このデバイスの状態遷移の記載については、例えば、ＣＳＬＳ（Ｃ Ｓｐｅｃｉｆｉｃａｔｉｏｎ Ｌａｎｇｕａｇｅ ｆｏｒ Ｓｙｓｔｅｍｓ ｓｏｆｔｗａｒｅ）規約を用いることができる。加えて、モデル検査部２３０は、ハイパーバイザ部２００本体が備えるデバイスドライバのモデル検査を行うこともできる。
モデル検査部２３０は、このモデル検査により、仮想化されたソフトウェア層の正確な動作を確認することに対する検証技術を提供することができる。つまり、モデル検査部２３０は、ハイパーバイザ部２００の仮想化レイヤのデバイス・ハンドラーが、ゲストＯＳがデバイスをエラー状態に導かないようにするための、正確なＩ／Ｏコマンドの順番制御（オーダー）を行う動作認証を行うことができる。このように、モデル検査部２３０により動作認証したソースコードは、最適化等したコンパイルを行い、ＯＳ部２２０のドライバ部２４０や、ハイパーバイザ部２００のデバイスドライバとしてに組み込むことができる。そして、モデル検査部２３０で動作認証されたドライバ部２４０は、直接アクセス方式のＩ／Ｏコマンドについて、システムモニタ部２１０にて検証を少なくした監視を行わせることができる。
また、モデル検査部２３０は、特に仮想化レイヤ自体の分離と、デバイスの正確な動作を保証するために、カーネル構築時やドライバ部２４０の更新時に最初に実行することが望ましい。
また、モデル検査部２３０は、ＯＳ部２２０を用いて実行されるアプリケーション・ソフトウェアとして実装することができる。つまり、モデル検査部２３０は、ＯＳ部２２０の仮想マシン内の他のアプリケーションと連動させて実行することができる。
【００１８】
なお、モデル検査部２３０は、ハイパーバイザ部２００と同様の仮想化レイヤで実行されるように構成することもできる。この場合、モデル検査部２３０は、仮想化レイヤで実行されるため、直接アクセスのＩ／Ｏコマンド列を容易に検知して、このオートマトンの状態によりモデル検査を行うことができる。
また、モデル検査部２３０は、ハイパーバイザ部２００やシステムモニタ部２１０と同じモジュールや構成部位として備えられていてもよい。この場合でも、モデル検査部２３０は、ハイパーバイザ部２００やシステムモニタ部２１０と同時並行的には動作させないで検証のみ行うことで、動作を軽くすることができる。
また、モデル検査部２３０は、ドライバ部２４０のドライバのソースコードをチェックするだけでなく、オートマトンによる状態遷移であれば、任意のものを検査可能である。つまり、モデル検査部２３０は、アプリケーション部２５０の通常のウェブブラウザや計算ソフトウェア等の各種アプリケーションのソースコードに状態遷移を記載して、動作のチェックをさせることもできる。
また、ソースコードが存在しない市販ＯＳの場合には、このモデル検査部２３０を用いない構成も可能である。
【００１９】
仮想マシン３００は、エミュレートされた仮想のコンピュータ、すなわち仮想マシン（Ｖｉｒｔｕａｌ Ｍａｃｈｉｎｅ、仮想機械）環境である。仮想マシン３００は、１つ又は複数の仮想マシンを用いることができる。各仮想マシンは、ハイパーバイザ部２００により自動的に制御部１００のＣＰＵコア等に動的に割り当られ、同時又は切り換えられて実行される。
仮想マシン３００は、ＨＤＤ等の同一のパーティション又は複数のパーティションや複数の物理的な補助記憶装置を用いて構成することができる。また、仮想マシン３００は、ｉＳＣＳＩ等を用いて、ネットワーク上のストレージ上のイメージとして構成することもできる。さらに、仮想マシン３００は、仮想ＨＤＤイメージ形式等を用いて、別のＯＳのパーティションにファイルとして含ませることもできる。
【００２０】
ＯＳ部２２０は、ハイパーバイザ部２００により仮想化されて実行される１つ又は複数のゲストＯＳを含む部位である。ＯＳ部２２０は、仮想マシン３００毎に用意することができる。また、ＯＳ部２２０は、ハイパーバイザ部２００がホストＯＳにより実行されるＴｙｐｅ ２方式の仮想化のハイパーバイザであった場合、このホストＯＳも含む。
ＯＳ部２２０は、ＵＮＩＸ（登録商標）、Ｌｉｎｕｘ（登録商標）、ＦｒｅｅＢＳＤ（登録商標）等の、ソースコードを基にカーネルやドライバ等をビルド（再構成）が可能な各種ＯＳをゲストＯＳとして用いることができる。さらに、ＯＳ部２２０は、ＭＡＣ（登録商標）ＯＳ、ウィンドウズ（登録商標）等の、通常はソースコードによりビルドしない市販ＯＳを用いることもできる。
【００２１】
ドライバ部２４０は、周辺機器、ネットワーク等のデバイス（機器）と接続の制御プログラムであるデバイスドライバ（以下、ドライバという。）の部位である。ドライバ部２４０は、ＯＳ部２２０に備わったＡＰＩ（Ａｐｐｌｉｃａｔｉｏｎ Ｐｒｏｇｒａｍ Ｉｎｔｅｒｆａｃｅ）を用いたり、逆にＯＳ部２２０に組み込まれてＡＰＩを提供した上で、ハイパーバイザ部２００がエミュレーションを行う仮想デバイスにアクセスする。さらに、ドライバ部２４０は、オーバーヘッドが顕著なデバイス、例えばネットワークカード、ＲＡＩＤ（Ｒｅｄｕｎｄａｎｔ Ａｒｒａｙｓ ｏｆ Ｉｎｅｘｐｅｎｓｉｖｅ Ｄｉｓｋｓ）等の補助記憶インターフェイス、ビデオボード、ストリーミング映像デバイス等に関しては、準仮想化により物理デバイスへ直接アクセスが可能である。
ドライバ部２４０は、ソースコードがあるドライバをコンパイルした実行ファイルを用いることが可能である。この際に、上述のモデル検査部２３０により認証されたドライバについては、ＩＤ（Ｉｄｅｎｔｉｆｉｃａｔｉｏｎ）を付加したＩ／Ｏコマンドを用いて直接アクセスを行い、システムモニタ部２１０に認識させることができる。また、ドライバ部２４０は、ソースコードがない市販ＯＳ等の、認証されていないドライバを用いることも可能である。
【００２２】
アプリケーション部２５０は、仮想マシン３００上のＯＳ部２２０にて実行される各種のアプリケーション・ソフトウェアである。
このアプリケーション・ソフトウェアは、ＯＳ部２２０のＡＰＩを用いて、ドライバ部２４０により、各種の物理デバイスや仮想デバイスにアクセスできる。
このアプリケーション・ソフトウェアとしては、ドライバ部２４０のソースコードのあるドライバをチェックするモデル検査部２３０と、これと連動するソースコードデバッガ等を含ませることができる。また、アプリケーション・ソフトウェアとして、ソースコードをコンパイル等するｃｃ等のコンパイラやビルドを行うｍａｋｅ等の各種ソフトウェアを含ませることができる。さらに、仮想マシン３００やＯＳ部２２０やドライバ部２４０が停止した際のログ等を閲覧するソフトウェアを用いることもできる。加えて、別の仮想マシン３００が停止して当該仮想マシン３００に切り換えられた際に報知する警報ソフトウェア等を用いることができる。
【００２３】
〔デバイス状態遷移管理処理〕
次に、図２〜図７を参照して、本発明の実施の形態に係るデバイス管理方法に係るデバイス状態遷移管理処理について説明する。
ここで、本発明の実施の形態のハイパーバイザ部２００は、上述したように準仮想化による直接アクセス方式を許容する。このハードウェアの規格に従った物理デバイスへのアクセスを行わないと、物理デバイスが使用不可能になることがある。この場合、当該デバイスをリセットするか、場合によっては、コンピュータ１０自体をリセットする必要がある。
このため、本発明の実施の形態に係るコンピュータ１０は、ハイパーバイザ部２００に加えて、ゲストＯＳのドライバが正確な方法で物理デバイスのハードウェアを管理するかどうかチェックするための機構であるシステムモニタ部２１０を用いる。
これに加えて、本実施形態に係るデバイス状態遷移管理処理では、仮想マシン３００内のドライバ部２４０に対して、モデル検査部２３０により、モデル検査による認証を行う。この上で、この認証されたドライバからの直接アクセスを、システムモニタ部２１０により監視する。
これにより、ゲストＯＳのカーネルによるデバイスのアクセスについて、オーバーヘッドが少ない直接アクセスを用いた場合でも、デバイスが使用不可能になることを防ぐことができる。
以下で、図２のフローチャートを用いて、デバイス状態遷移管理処理の各処理について説明する。
【００２４】
（ステップＳ１０１）
まず、制御部１００は、モデル検査部２３０を用いてドライバ部２４０のドライバ等のソースコードをモデル検査するドライバチェック処理を行う。
このドライバチェック処理では、デバイスへの操作が仕様を満たすかどうかを検査するために、モデル検査を用いる。
具体的には、制御部１００は、デバイスの状態遷移について上述のＣＳＬＳ規約によりオートマトンとして記載されたソースコードをコンパイルし、ステップ実行等を行う。その上で、制御部１００は、デバイスの状態が当該オートマトンに従って正しく遷移するか否かについて判定する。
この際、制御部１００は、モデル検査部２３０により、ゲストＯＳがシステムモニタ部２１０により停止させられないように、実際には直接アクセス方式で物理デバイスにアクセスしないように構成することが好適である。また、逆に、制御部１００は、直接アクセス方式により状態が遷移した物理デバイスの状態や仮想デバイスの状態を、遷移の情報として取得して検証することが可能である。
制御部１００は、所定ステップの間、デバイスが正しく遷移したと考えられる場合、そのドライバのオブジェクトや実行コードに所定のＩＤを付加する「認証」を行う。
これにより、認証されたドライバからの直接アクセスの際には、システムモニタ部２１０が検知してオーバーヘッドを抑える処理を行うことができる。
【００２５】
（ステップＳ１０２）
次に、制御部１００は、システムモニタ部２１０を用いて、仮想マシン３００からの物理デバイスへの直接アクセスを管理するシステムモニタ処理を行う。
この処理では、仮想化レイヤにおいて、ハイパーバイザ部２００が備えるデバイスドライバとは独立に、デバイスへのアクセスを管理する。
具体的には、制御部１００は、ドライバ部２４０からの準仮想化による直接アクセスを検知する。この上で、直接アクセスの際、制御部１００は、不正コマンド等により物理デバイスが不正な状態遷移となる「不正アクセス」がされているかを検知する。そして、制御部１００は、不正アクセスが検知された場合に、仮想マシン３００の停止等を行う。
このような不正アクセスにより、コンピュータ１０自体が動作不良やハングアップする可能性がある。よって、システムモニタ部２１０を用いてチェックすることで信頼性を高めることができる。
また、制御部１００は、物理デバイス自体の状態遷移について、システムモニタ部２１０を用いて検査する。この上で、制御部１００は、上述の認証されたドライバのアクセスにより不正な遷移となった場合、物理デバイスの故障を報知する。
以上により、デバイス状態遷移管理処理を終了する。
【００２６】
〈ドライバチェック処理の詳細〉
次に、図３〜図５を参照して、本発明の実施の形態に係るドライバチェック処理の詳細について説明する。これらの処理は、制御部１００は、モデル検査部２３０を用いて実行する。
以下、図３のフローチャートを基に、各処理の詳細について説明する。
【００２７】
（ステップＳ２０１）
まず、制御部１００は、初期化処理を行う。
この処理では、まず、制御部１００は、モデル検査を行うドライバ等のソースコードが存在するか判断する。
次に、制御部１００は、当該ソースコードにデバイスの状態遷移に関するオートマトンの記載があるか否かを判断する。ここで、ソースコードの全てにオートマトンの記載を行う必要はない。よって、制御部１００は、物理デバイスにアクセスする部分のソースファイル等、一部について記載があれば、記載ありと判断する。
ソースコードにオートマトンの記載があった場合、制御部１００は、このソースコードを、パーサ等を用いて解釈する。この上で、制御部１００は、リスト等のデータ構造を用いて実際のオートマトンのデータを主記憶部１１０に作成する。
なお、制御部１００は、ソースコードがなかったり、ソースコードにオートマトンの記載がなかったりした場合には、エラーとして処理を終了する。
【００２８】
（ステップＳ２０２）
次に、制御部１００は、コンパイル処理を行う。
具体的には、制御部１００は、ソースコードの言語に係るコンパイラを、パイプ等を用いて起動する。
この上で、制御部１００は、上述のドライバのソースコードを読み込ませ、コンパイルさせる。
このコンパイルにおいては、最適化を行わない「デバッグ」モードのシンボルを付加したコンパイルを行うことが好適である。
【００２９】
（ステップＳ２０３）
次に、制御部１００は、モデル遷移チェック処理を行う。
このモデル遷移チェック処理においては、制御部１００は、モデルチェック部は、コンパイルされたドライバについて、ステップ実行等を行う。このステップ実行は、統合開発環境のソースレベルデバッガ等と連動させることができる。
この上で、制御部１００は、ステップ毎にオートマトンの状態を検査する。
このモデル遷移チェック処理の詳細な実行例については後述する。
【００３０】
（ステップＳ２０４）
次に、制御部１００は、オートマトンが正しい遷移を示しているか否か判定する。
Ｙｅｓ、すなわちオートマトンの状態が正しい遷移を示している場合、制御部１００は、処理をステップＳ２０６に進める。
Ｎｏ、すなわちオートマトンの状態が不正な遷移を示している場合は、制御部１００は、処理をステップＳ２０５に進める。
【００３１】
（ステップＳ２０５）
オートマトンが不正な遷移を示していた場合、制御部１００は、エラー処理を行う。
この不正な遷移をした場合、当該デバイスはエラー状態等となり使用不可能となる、すなわちプログラムの不正な箇所（バグ）があると考えられる。よって、デバイスドライバのソースコード自体を変更する必要がある。
このため、制御部１００は、エラーを起こした箇所をソースレベルデバッガ等に報知する。
この際、制御部１００は、当該ソースレベルデバッガ等により、オートマトンの遷移図等と、停止箇所を示す。これにより、ユーザにソースコードの不正箇所を知る手がかりを与えることができる。
その後、制御部１００は、ドライバチェック処理を終了する。
【００３２】
（ステップＳ２０６）
オートマトンが正しい遷移を示していた場合、制御部１００は、ステップ実行が終了したか否かについて判定する。
ここでは、制御部１００は、所定回数のステップ実行したか、ソースコードに様々なパラメータを与えてほぼ全ての状態遷移の実行を終えた場合、ステップ実行の終了と判断する。また、制御部１００は、オートマトンの状態から全ての状態遷移を検査したと判断できた場合等にも、ステップ実行の終了と判断することができる。
Ｙｅｓ、すなわちステップ実行が終了した場合、制御部１００は、処理をステップＳ２０７に進める。
Ｎｏ、すなわちまだステップ実行を行う必要がある場合、制御部１００は、処理をステップＳ２０３に戻してモデル検査を続ける。
【００３３】
（ステップＳ２０７）
ステップ実行が終了した場合、制御部１００は、デバイスドライバ認定処理を行う。
具体的には、制御部１００は、直接アクセスを行っても物理デバイスを停止等させる可能性が少ないドライバであるとして、認証を行う。
この処理においては、制御部１００は、最適化を行った上でデバイスドライバをコンパイルする。この際、制御部１００は、システムモニタ部２１０の公開鍵や秘密鍵等を基に、ハッシュ関数等を用いて、不正な認証ができないようなＩＤを作成して、このＩＤをソースコードやオブジェクトやバイナリ（実行）コード等に埋め込む。また、制御部１００は、モデル検査部２３０がソースコードを解析して作成したオートマトンのデータについても、ＩＤと共に埋め込むことができる。
これにより、認証されたドライバは、物理デバイスへの直接アクセスの際に、このＩＤを用いることができる。これにより、システムモニタ部２１０の管理の負荷を軽減できる。
以上により、ドライバチェック処理を終了する。
【００３４】
〈モデル遷移チェック処理の実施例〉
ここで、モデル遷移チェック処理の具体例について、図４Ａ〜図５を参照して詳細に説明する。
上述したように、このモデル遷移チェック処理では、ＯＳ部２２０のゲストＯＳに、物理デバイスの規定に従った正確な振る舞いを強いるための機構を提供する。
この際、本発明の実施の形態においては、制御部１００が、モデル検査部２３０を用いて、ドライバ部２４０が正確な方法でハードウェアを管理するかどうか検査する。
以下では、仮想マシン３００のドライバ部２４０について、ＲＳ−２３２規格等のシリアル・インターフェイスのドライバを用いてモデル検査を行った実施例について説明する。
この実施例では、仮想マシン３００のドライバ部２４０のシリアルデバイス・ハンドラーのモデル検査を行って、シリアルデバイスがエラー状態にならないように正確な命令動作をすることを確認した。
これにより、ドライバ部２４０が、ハイパーバイザ部２００下の仮想マシン３００によって正確に動作することを確認することができる。
【００３５】
（文字の送信）
まず、図４Ａを参照して、ドライバ部２４０のシリアルデバイスのドライバによる文字の送信について説明する。オートマトン２４５は、このドライバ部２４０の状態遷移を示す。
シリアルライン上の文字を送信するために、制御部１００は、ドライバ部２４０の動作として、以下の工程に従う必要がある。
まず、図４Ａのシリアルドライバの最初の工程（１）として、制御部１００は、ｓｅｎｄ（送信）バッファが空かどうかチェックする。
次に、制御部１００は、送信バッファが空か否かチェックして、空の場合、次の工程（２）に進める。そうでなければ、制御部１００は、送信バッファが空になるまで待つ。
その後、制御部１００は、送信バッファに文字を書き込む。
ここで、バッファがフルのとき、ドライバが文字を書き込むと、オートマトン２４５のデバイスの状態はエラー状態になる。制御部１００は、このエラー状態となったことを検知して、モデル検査部２３０に報知することができる。
【００３６】
上述のシリアルデバイスの状態遷移は、モデル化することができる。
以下に、バッファが空であるか否かをチェックするｓｅｒ＿ｉｓ＿ｒｅａｄｙ＿ｔｏ＿ｓｅｎｄ（）関数の例を示す。このｓｅｒ＿ｉｓ＿ｒｅａｄｙ＿ｔｏ＿ｓｅｎｄ（）関数は、バッファの状態を検知し、送信が準備可能かどうかを返す。
【００３７】
/*@
$ensures((ser_tx_ready == 1) ||
(ser_tx_ready == 0));
*/
int ser_is_ready_to_send(void)
{
int thre = hw_uart_lsr_thre();
if (thre)
ser_tx_ready = 1;
else
ser_tx_ready = 0;
return thre;
}
【００３８】
また、以下は、バッファが空で送信可能な場合、バッファに文字を書き出すｓｅｒ＿ｓｅｎｄ（）関数の例を示す。
ｓｅｒ＿ｓｅｎｄ（）関数は、バッファが空及び送信要求である場合、バッファに文字を書き、そうでなければ、エラーをモデル検査部２３０に返す。
なお、制御部１００は、実際にコンパイル後のドライバがドライバ部２４０やハイパーバイザ部２００に組み込まれた際、このエラーの場合には、ハイパーバイザ部２００が当該仮想マシン３００を停止するように通知することもできる。
【００３９】
/*@
$ensures($old(ser_tx_ready) == 0
==> need_to_kill_vm == 1);
*/
void ser_send(int ch)
{
if (ser_tx_ready == 0)
need_to_kill_vm = 1;
ser_tx_ready = 0;
hw_uart_tx(ch);
}
【００４０】
この例のように、デバイスの状態遷移に関するオートマトンの記載は、Ｃ言語の場合には、上述したＣＳＬＳ規約により、／＊＠ ＊／のようなコメント行を用いて記載することができる。
通常のコンパイラでは、この記載はコメント行として無視されるため、汎用性を高めることができる。
【００４１】
（文字の送信）
次に、図４Ｂを参照して、ドライバ部２４０のシリアルデバイスのドライバによる文字の受信について説明する。オートマトン２４６は、このドライバ部２４０の状態遷移を示す。
文字の受信は、上述の文字の送信と同様の方法でモデル化することができる。
ドライバ部２４０のシリアルドライバは、シリアルライン上の文字を受信するために下記の動作を行う。
まず図４Ｂの最初の工程（１）において、制御部１００は、受信バッファにおいてデータ受信の準備ができているかどうかチェックする。準備ができている場合、次の工程（２）に移る。そうでなければ、制御部１００は、データの準備ができるまで待つ。
この上で、制御部１００は、受信バッファから文字を読み出す。
一方、データがない場合に、受信バッファから文字を読み出すと、制御部１００はエラーをモデル検査部２３０に報知する。
【００４２】
このように、制御部１００は、モデル検査部２３０を用いてプログラムの誤動作を検知できる。
図５は、このモデル検査の結果を示す画面例である。この例では、「Ｐｒｏｇｒａｍ ｉｓ ＳＡＦＥ」即ち、安全なドライバであると検査されている。
このように、仮想化レイヤにおいて、誤操作がいつ行なわれるか実際にモデル検査により確認することができる。
したがって、不正アクセスをしない正確な動作を行うドライバ部２４０を得ることが可能になる。
これにより、信頼性が高く高パフォーマンスの仮想マシンを提供することができる。
【００４３】
なお、制御部１００は、エラー状態の報知について、検証した後のドライバ部２４０により、システムモニタ部２１０やハイパーバイザ部２００に対して報知することもできる。
これにより、万一のエラーの際には、ハイパーバイザ部２００が物理デバイスにアクセスしないように構成することができ、検証されたドライバ部２４０による不正アクセスを防ぐことが可能になる。
このため、本発明の実施の形態に係るコンピュータ１０を、非常に高度の信頼性が求められる生命維持、生産プラント、乗り物の制御といった分野に用いることができる。
【００４４】
〈システムモニタ処理の詳細〉
次に、図６及び図７を参照して、本発明の実施の形態に係るシステムモニタ処理の詳細について説明する。これらの処理は、上述したように、制御部１００が、システムモニタ部２１０を用いて、仮想化レイヤ上で実行する。
以下、図６のフローチャートを用いて、各処理の詳細について説明する。
【００４５】
（ステップＳ３０１）
まず、制御部１００は、ドライバ認証検知処理を行う。
この処理では、仮想マシン３００のドライバ部２４０が、上述のドライバチェック処理により認証されたドライバであるか検知する。
具体的には、制御部１００は、ドライバ部２４０のドライバに認証によるＩＤ等があるか否か、秘密鍵等を用いて検証する。
ここで、ドライバ部２４０のドライバが認証されたものであった場合、制御部１００は、このＩＤを用いた物理デバイスへのアクセスについては、後述するフィルタ処理にて不正アクセスであるかを検知しないか負荷を抑えた「軽い」検知のみ行う。
【００４６】
（ステップＳ３０２）
次に、制御部１００は、Ｉ／Ｏコマンド読み込み処理を行う。
図７を参照して説明すると、制御部１００は、ハイパーバイザ部２００が実行する仮想マシン３００のゲストＯＳのドライバ部２４０から、デバイスへアクセスするＩ／Ｏコマンド（指示信号）があったかどうかを検知する。つまり、制御部１００は、仮想化レイヤにおいて、デバイスドライバとは独立して、デバイスへの操作を管理する。
制御部１００は、デバイスへのアクセスするＩ／Ｏコマンドを検知した場合、ハイパーバイザ部２００に通知する。
このドライバ部２４０からのデバイスへアクセスするＩ／Ｏコマンドは、仮想レイヤへのハイパーバイザコール形式で行うことが好適である。この際、制御部１００は、チップセット１５０に接続された物理デバイスへの指示を行うＩ／Ｏコマンドに加えて、仮想デバイスのコマンドも検知する。また、制御部１００は、ドライバのＩ／Ｏコマンド毎にＩＤを検知することができる。
【００４７】
（ステップＳ３０３）
次に、制御部１００は、デバイスへアクセスするＩ／Ｏコマンドが、直接アクセスのＩ／Ｏコマンドであったか否かについて判定する。
Ｙｅｓの場合、制御部１００は、処理をステップＳ３０４に進める。
Ｎｏの場合、制御部１００は、処理をステップＳ３０７に進める。
【００４８】
（ステップＳ３０４）
次に、制御部１００は、フィルタ処理を行う。
具体的には、制御部１００は、直接アクセスのＩ／Ｏコマンド列が、デバイスの状態遷移を不正にする、不正コマンドである場合、これを不正アクセスとして検知する。
このデバイスの状態遷移については、ハイパーバイザ部２００の物理デバイス用のドライバに対応するオートマトンを用意しておいて、このオートマトンの状態遷移がエラーになるか否かについて検知する。
このオートマトンとしては、上述のモデル検査部２３０が作成したドライバ部２４０のオートマトンを用いることができる。この際、異なるゲストＯＳを備えた仮想マシン３００であっても、同一の物理デバイス／仮想デバイスについては、同一のオートマトンを用いることができる。
このように、オートマトンを用いて不正コマンドを検知するため、ハイパーバイザ部２００が仮想マシン３００を切り換えた際、デバイスの動作タイミング等が原因で各仮想マシン３００からの物理デバイスからのアクセスが不正コマンドになった場合でも対応できる。
また、仮想マシン３００から、複数回、単一のデバイスに対しＩ／Ｏコマンドによるアクセスを行った場合でも対応できる。
このため、不正コマンドによりデバイスが利用不可能になることを防ぐことが可能になる。
【００４９】
ここで、直接アクセスのＩ／Ｏコマンド列が、上述の認証されたドライバ部２４０のドライバからのＩ／Ｏコマンド列であった場合、制御部１００は、例えば、オートマトンの状態遷移の変化を行わないような処理を行うことが可能である。また、例えば、検知のフィルタ自体をスルー（通過）させることもできる。これにより、仮想化のオーバーヘッドを減らし、負荷を抑えて、安全に物理デバイスにアクセスさせることができる。
この場合でも、ドライバ部２４０のドライバ自体がオートマトンを持って状態遷移がエラーになった場合には、システムモニタ部２１０に報知することができるため、安全に物理デバイスにアクセス可能である。
【００５０】
（ステップＳ３０５）
次に、制御部１００は、不正アクセスであるか否かについて判定する。
ここでは、上述なようにオートマトンの状態遷移により、物理デバイスのアクセスに係る不正コマンドを検知した場合、不正アクセスである、すなわちＹｅｓと判断する。それ以外の場合はＮｏと判断する。
Ｙｅｓの場合、制御部１００は、処理をステップＳ３０６に進める。
Ｎｏの場合、制御部１００は、処理をステップＳ３０７に進める。
【００５１】
（ステップＳ３０６）
制御部１００は、不正アクセスであった場合、ゲストＯＳ停止処理を行う。
具体的には、制御部１００は、ハイパーバイザ部２００へ、不正アクセスをした仮想マシン３００を停止するように指示する。
この際、仮想マシン３００を直接停止させるのではなく、仮想マシン３００のドライバ部２４０の当該デバイスドライバに「エラー」の通知を返信することが可能である。この場合でも、当該デバイスドライバが停止しない場合、制御部１００は、ＯＳ部２２０にエラーを報知することができる。これにより、ＯＳ部２２０のエラー対応機能によりドライバ部２４０の当該デバイスドライバを停止させることもできる。しかしながら、この場合でもＯＳ部２２０が反応しない場合、制御部１００は、仮想マシン３００自体を停止することができる。このような構成により、コンピュータ１０の動作の停止時間や再起動の時間等を少なくすることができる。
システムモニタ部２１０は、仮想マシン３００やＯＳ部２２０やドライバ部２４０を停止させた場合には、ハイパーバイザ部２００に通知し、更に表示部や音声入出力部やシリアルデバイス等に警告を報知することができる。そして、制御部１００は、エラーの内容を表示部等やネットワークを介した監視機器等に報知し、ログを作成する。
【００５２】
（ステップＳ３０７）
次に、制御部１００は、物理デバイス遷移検査処理を行う。
この処理においては、制御部１００は、当該物理デバイスの状態を、チップセット１５０を介して取得する。
制御部１００は、この取得について、ハイパーバイザ部２００の情報を取得し、主に直接アクセスのＩ／Ｏコマンド列により物理デバイスを動作させた後に行う。
この上で、制御部１００は、この物理デバイスの状態が、オートマトンにより想定された状態遷移であるか否かを判断する。
制御部１００は、物理デバイスが想定された遷移の状態（ステート）でなかった場合には、不正な遷移をしていると検知する。特に、制御部１００は、認証されたドライバからのアクセスがあったにも関わらず、物理デバイスがエラー状態になっていることを検知した場合、起こり得ないことが起こったとして、デバイスが故障したと検知する。
【００５３】
（ステップＳ３０８）
制御部１００は、物理デバイスが不正な状態遷移をしているか否か判定する。ここでは、制御部１００は、上述の不正な状態遷移であった場合には、Ｙｅｓと判定する。
Ｙｅｓ、すなわち不正な状態遷移があった場合、制御部１００は処理をステップＳ３０９に進める。
Ｎｏ、すなわち物理デバイスの状態遷移が想定していた状態遷移であった場合、制御部１００は処理をステップＳ３０２に戻して、管理を続ける。
【００５４】
（ステップＳ３０９）
制御部１００は、ここでは、故障報知処理を行う。
この処理においては、制御部１００は、ハイパーバイザ部２００、表示部等やネットワークを介した監視機器等に、不正な遷移をした物理デバイスの故障を報知する。この際に、表示部や音声入出力部やシリアルデバイス等に警告を報知することもできる。
なお、不正アクセスでドライバや仮想マシン３００を停止した場合にも、制御部１００は、報知を行って、システムモニタ処理を停止するように構成することもできる。
以上により、システムモニタ処理を終了する。
【００５５】
以上のように構成することで、以下のような効果を得ることができる。
本発明の実施の形態に係るコンピュータ１０は、デバイスへのアクセスを仮想化レイヤのシステムモニタ部２１０でフィルタして、デバイスの状態遷移を管理する。
すなわち、本発明の実施の形態に係るコンピュータ１０は、仮想マシン３００上でゲストＯＳであるＯＳ部２２０を実行する。この上で、ゲストＯＳによるデバイスのアクセスを、仮想化レイヤのシステムモニタ部２１０が監視し、デバイスが利用不可能となる不正な操作を検知したら、ゲストＯＳの停止又はゲストＯＳによるそのデバイスの利用を停止する。具体的には、本実施形態に係るシステムモニタ部２１０は、準仮想化による直接アクセスの際、物理デバイスに不正なＩ／Ｏコマンド列等でアクセスすると、仮想マシン３００又はドライバ部２４０を停止させることができる。
これにより、仮想マシン３００内のソフトウェアからのデバイスへのアクセスにより、当該デバイスが利用不可能になることを防ぐことができる。
また、システムモニタ部２１０は、デバイスドライバからのアクセスのＩ／Ｏコマンド自体を管理するため、ソースコードが入手できない商用（市販）ＯＳにも適用できる。
また、システムモニタ部２１０は、ゲストＯＳから複数回、単一のデバイスに対しアクセスがされた場合でも、そのデバイスの状態遷移を検知する。これにより、不正なＩ／Ｏコマンド列によりデバイスが利用不可能になることを防ぐことができる。
【００５６】
これにより、安定稼働が必要なコンピュータ１０に適用することができる。
すなわち、デバイスが利用不可能となることが被害や損害につながるような機器での利用、例えば、医療機器やインフラ系等のコンピュータに利用できる。
【００５７】
また、本発明の実施の形態に係るシステムモニタ部２１０は、仮想化レイヤに対する直接アクセスに対してだけ、ハードウェアのデバイスの仕様に従ったアクセスであるか管理する。この際、物理デバイスの状態遷移が想定から外れた場合に、ゲストＯＳ又はドライバを稼働停止させられる。
これにより、仮想マシン３００からの物理デバイスへのアクセスにより当該物理デバイスがエラー状態となることを防ぐことができる。よって、コンピュータ１０を安定して稼働することができる。
【００５８】
また、従来技術１は、デバイスドライバそのものを検証することによりデバイスへの操作が正しいことを保証するものであった。このため、従来技術１は、デバイスの共有が起こる仮想化環境に直接適用することができなかった。
これに対して、本発明の実施の形態に係るモデル検査部２３０は、仮想化レイヤに対するアクセスのＩ／Ｏコマンド列に関するモデル検査を行うことで、仮想化された環境でも適用することができる。
【００５９】
また、従来技術１のソースコードの検査では、ホーア論理を用いてドライバの動作の正しさを証明するため非常に手間がかかるという問題があった。つまり、従来技術１では、ユーザが各種パラメータ等を変えてデバイスドライバを検査する必要があった。
これに対して、本発明の実施の形態に係るモデル検査部２３０は、オートマトンの状態遷移を用いてドライバのモデル検査を行うため、自動的にデバイスドライバの検査を行うことができる。これにより、高速に手間が少なくドライバの検査ができる。
【００６０】
また、本発明の実施の形態に係るモデル検査部２３０は、モデル検査を行ったドライバを認証する。
これにより、システムモニタ部２１０は、認証されたドライバからの物理デバイスへのアクセスに際して、負荷を抑えたフィルタリングを行うことができる。
よって、仮想化によるオーバーヘッドを少なくしたまま、コンピュータ１０を安全に稼働させられる。
このため、ネットワークのコントローラ等のパフォーマンスが必要なハードウェア資源のアクセスを高速化できる。つまり、例えば、ネットワークカードに適用した場合、ｉＳＣＳＩ等により接続されたネットワークストレージのアクセススピードを高速化できる。
【００６１】
本発明の実施の形態に係るシステムモニタ部２１０は認証されたドライバが物理デバイスへアクセスをした際に、当該物理デバイスの状態遷移が不正であった場合には、当該物理デバイスの故障と検知することができる。
これにより、不正アクセスの検知と、物理デバイスの故障の検知とを同一環境で行うことができ、コンピュータ１０に問題が起こった場合に、迅速に解決できる。よって、コンピュータ１０の運用コストを低下させることができる。
【００６２】
なお、上記実施の形態の構成及び動作は例であって、本発明の趣旨を逸脱しない範囲で適宜変更して実行することができることは言うまでもない。
【産業上の利用可能性】
【００６３】
本発明の計算機は安全な稼働をさせることができるため、デバイスが利用不可能となることが被害や損害につながるような計算機に用いることができ、産業上に利用することができる。
【符号の説明】
【００６４】
１０ コンピュータ
１００ 制御部
１１０ 主記憶部
１２０ 補助記憶部
１５０ チップセット
２００ ハイパーバイザ部
２１０ システムモニタ部
２２０ ＯＳ部
２３０ モデル検査部
２４０ ドライバ部
２４５、２４６ オートマトン
２５０ アプリケーション部
３００ 仮想マシン
【技術分野】
【０００１】
本発明は、計算機、デバイス管理方法、プログラム、及び記録媒体に係り、特に仮想化環境でデバイスの管理を行う計算機、デバイス管理方法、プログラム、及び記録媒体に関する。
【背景技術】
【０００２】
近年、コンピュータが社会の様々な環境で用いられるようになっている。このため、ソフトウェアのミス（バグ）や悪意あるソフトウェアにより、コンピュータの動作停止を防ぐ技術が重要となっている。
ここで、コンピュータはデバイスドライバ（ドライバ）と呼ばれるソフトウェアを用いて、コンピュータ内部の装置や周辺機器等である各デバイスを制御している。
このデバイスドライバにミスがあり、ハードウェアの仕様に沿わないアクセスを行うと、当該デバイスがエラー状態となり反応しなくなることがある。この場合、コンピュータのシステムをリセット等する必要があり、常に稼働することが必要なコンピュータでは都合が悪い。
【０００３】
このため、従来からデバイスドライバそのものを検証する技術が存在した。このような従来のドライバの検証技術として、非特許文献１を参照すると、ホーア論理を用いてデバイスのアクセスの正しさを証明する技術が記載されている（以下、従来技術１とする。）。
このようなホーア論理を用いてデバイスドライバを行うことで、多くの演算処理が必要なものの、ソースコードのあるデバイスへのアクセスの操作が正しいことを保証することができる。
【０００４】
一方、従来からハードウェア環境を抽象化して実行する仮想化（Ｖｉｒｔｕａｌｉｚａｔｉｏｎ）技術が用いられてきた。
このような仮想化技術により、仮想化されたゲストＯＳ（Ｇｕｅｓｔ Ｏｐｅｒａｔｉｎｇ Ｓｙｓｔｅｍ）を隔離した環境で実行できる。つまり、仮想化技術では、ゲストＯＳからのデバイスへのアクセスについて、各機器をエミュレーションにより管理して実行する。
これにより、コンピュータ全体の停止を防ぐことができる。よって、仮想化技術を用いることで、より動作停止が少ない安全なコンピュータ・システムを構築することができる。
【０００５】
ここで、従来の仮想化技術を用いたデバイスドライバの管理技術として、特許文献１を参照すると、少なくとも一つのデバイスドライバを含むドメインを多数個具備するドメイン部と、デバイスのハードウェアを構成するシステム資源部、及びＤＭＡ（Ｄｉｒｅｃｔ Ｍｅｍｏｒｙ Ａｃｃｅｓｓ）ドライバ、及び仮想化環境で前記システム資源部に対する前記ドメイン部の接近動作を制御する接近制御モジュールを具備する制御部を含む仮想化環境での安全なシステム保護装置の技術が開示されている（以下、従来技術２とする。）。
従来技術２のシステム保護装置によれば、仮想化環境で悪性コード（ｍａｌｗａｒｅ）など悪意のある接近からシステム資源を保護し、システム障害を解決して安全なサービスを保障することができる。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２００８−２６９５８９号公報
【非特許文献】
【０００７】
【非特許文献１】Ｊｉａｎｊｕｎ Ｄｕａｎ、「Ｃｏｒｒｅｃｔｎｅｓｓ Ｐｒｏｏｆｓ ｆｏｒ Ｄｅｖｉｃｅ Ｄｒｉｖｅｒｓ ｉｎ Ｅｍｂｅｄｄｅｄ Ｓｙｓｔｅｍｓ」、ＵＳＥＮＩＸ ｔｈｅ ５ｔｈ ｉｎｔｅｒｎａｔｉｏｎａｌ ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｓｙｓｔｅｍｓ ｓｏｆｔｗａｒｅ ｖｅｒｉｆｉｃａｔｉｏｎ、２０１０年１０月６日、、インターネット〈URL：http://www.usenix.org/event/ssv10/tech/full_papers/Duan.pdf〉
【発明の概要】
【発明が解決しようとする課題】
【０００８】
しかしながら、従来技術１のソースコードの検査では、ソースコードのない市販ＯＳについてのデバイスの管理を行うことができなかった。
また、従来技術２のシステム保護装置においては、仮想化環境でシステム資源に対して仮想マシンであるドメインの接近動作を制御する接近制御モジュールを備えていた。しかしながら、この接近制御モジュールは、安全なドメインがハードウェア資源に接近することを許容する（段落［００３０］等を参照）だけで、当該ハードウェア資源であるデバイスの状態が不正になるか否かについて判断することはできなかった。このため、安全と判断されたドメインにおけるドライバのバグ等により不正なアクセスがあった場合の安全性を保証できなかった。
【０００９】
本発明は、このような状況に鑑みてなされたものであり、上述の課題を解消することを課題とする。
【課題を解決するための手段】
【００１０】
本発明の計算機は、仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ部と、デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ部に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ部とを備えることを特徴とする。
本発明の計算機は、前記ゲストＯＳの前記デバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行うかを、オートマトンの状態遷移により検査して認証するモデル検査部を備えることを特徴とする。
本発明の計算機は、前記システムモニタ部は、前記モデル検査部で認証されたデバイスドライバからの直接アクセスがあった場合、負荷を抑えて前記デバイスにアクセスさせることを特徴とする。
本発明の計算機は、前記システムモニタ部は、前記モデル検査部で用いた前記オートマトンにより、前記ハードウェアの仕様に従ったアクセスを行うか否かフィルタリングすることを特徴とする。
本発明の計算機は、前記システムモニタ部は、前記認証されたデバイスドライバが前記デバイスのアクセスをした際に、前記デバイスの状態遷移が不正であった場合には、前記デバイスの故障と検知することを特徴とする。
本発明の計算機デバイス管理方法は、コンピュータのデバイスの状態遷移を管理するデバイス管理方法において、前記コンピュータは、仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、仮想化レイヤにて前記デバイスの管理を行うシステムモニタ手段とを備え、前記システムモニタ手段により、前記デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知することを特徴とする。
本発明のプログラムは、コンピュータを、仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段として機能させるためのプログラムであることを特徴とする。
本発明の記録媒体は、コンピュータを、仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段として機能させるためのプログラムを記録したコンピュータ読み取り可能な記録媒体であることを特徴とする。
【発明の効果】
【００１１】
本発明によれば、デバイスのアクセスを仮想化レイヤで管理することで、ソースコードのない市販ＯＳでも、デバイスの状態遷移を管理するコンピュータを提供することができる。
また、本発明によれば、デバイスドライバがデバイスのハードウェアの仕様に従ったアクセスを行うかシステムモニタで管理することで、仮想マシンからのデバイスへのアクセスの安全性を保証するコンピュータを提供することができる。
【図面の簡単な説明】
【００１２】
【図１】本発明の実施の形態に係るコンピュータ１０の制御構成を示すブロック図である。
【図２】本発明の実施の形態に係るデバイス状態遷移管理処理のフローチャートである。
【図３】本発明の実施の形態に係るドライバチェック処理のフローチャートである。
【図４Ａ】本発明の実施の形態に係るシリアルドライバの送信時のモデル検査の概念図である。
【図４Ｂ】本発明の実施の形態に係るシリアルドライバの受信時のモデル検査の概念図である。
【図５】本発明の実施の形態に係るモデル検査処理の画面例である。
【図６】本発明の実施の形態に係るシステムモニタ処理の概念図である。
【図７】本発明の実施の形態に係るシステムモニタ処理のフローチャートである。
【発明を実施するための形態】
【００１３】
＜実施の形態＞
〔コンピュータ１０の構成〕
図１を参照して、本発明の実施の形態に係るコンピュータ１０（計算機）の構成について説明する。
コンピュータ１０は、主にＭＡＣ規格機やＰＣ／ＡＴ互換機等のＰＣ（Ｐｅｒｓｏｎａｌ Ｃｏｍｐｕｔｅｒ）、サーバ、汎用機、携帯電話、スマートフォン、ＰＤＡ（Ｐｅｒｓｏｎａｌ Ｄａｔａ Ａｓｓｉｓｔａｎｔ）、モバイル端末、セットトップボックス、ネットワーク接続機能付きテレビジョン、デジタル画像・音声再生用のメディアプレーヤー、ゲーム機等であり、ＯＳ（Ｏｐｅｒａｔｉｎｇ Ｓｙｓｔｅｍ）の機能を用いて各種プログラムを実行可能である。
また、コンピュータ１０は、本実施形態に係るデバイス状態遷移管理処理を実行するためのハードウェア資源である。このため、コンピュータ１０は、制御部１００と、主記憶部１１０と、補助記憶部１２０と、チップセット１５０とを備えている。
制御部１００は、ＣＰＵ（Ｃｅｎｔｒａｌ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ、中央処理装置）やＧＰＵ（Ｇｒａｐｈｉｃ Ｐｒｏｃｅｓｓｉｎｇ Ｕｎｉｔ）やＤＳＰ（Ｄｉｇｉｔａｌ Ｓｉｇｎａｌ Ｐｒｏｃｅｓｓｏｒ）等の制御手段である。制御部１００は、インテル社製のインテル・バーチャライゼーション・テクノロジー（Ｉｎｔｅｌ ＶＴ）又はＡＭＤ社製のＡＭＤ−Ｖのような、仮想化支援機構を備えていてもよい。また、制御部１００は、ＤＲＡＭのインターフェイス等を備えて、主記憶部１１０に直接アクセスするような構成を用いることが可能である。
主記憶部１１０は、ＤＲＡＭ（Ｄｙｎａｍｉｃ Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ）、ＤＤＲ２／３／４−ＳＤＲＡＭ、ＸＤ−ＲＡＭ、ＳＲＡＭ（Ｓｔａｔｉｃ ＲＡＭ）等の主記憶手段である。
補助記憶部１２０は、ＨＤＤ（Ｈａｒｄ Ｄｉｓｋ Ｄｒｉｖｅ）やフラッシュメモリや光学ドライブ等の補助記憶手段である。
チップセット１５０は、コンピュータ１０の各部位と、他の周辺機器やネットワーク等のデバイスとを接続するためのバスアービタや各種Ｉ／Ｏチップ等を備える周辺機器接続インターフェイス手段である。チップセット１５０が接続する周辺機器としては、表示部と、音声入出力部と、入力部とを含む。表示部は、ＬＥＤ（Ｌｉｇｈｔ Ｅｍｉｔｔｉｎｇ Ｄｉｏｄｅ）、ＬＣＤ（Ｌｉｑｕｉｄ Ｃｒｙｓｔａｌ Ｄｉｓｐｌａｙ）、ＰＤＰ（ＰＰｌａｓｍａ Ｄｉｓｐｌａｙ Ｐａｎｅｌ）、プロジェクタ等を用いることができる。入力部は、キーボード、トラックボール、タッチパネル、マウス等のポインティングデバイスを含む。チップセット１５０が接続するネットワークとしては、ＬＡＮ（Ｌｏｃａｌ Ａｒｅａ Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ Ａｒｅａ Ｎｅｔｗｏｒｋ）、携帯網や無線ＬＡＮ等の各種無線ネットワークを含む。
【００１４】
また、補助記憶部１２０は、ハイパーバイザ部２００（ハイパーバイザ手段）、システムモニタ部２１０（システムモニタ手段）、ＯＳ部２２０（ゲストＯＳ）、モデル検査部２３０（モデル検査手段）、ドライバ部２４０（デバイスドライバ、ドライバ）、及びアプリケーション部２５０（アプリケーション手段）を記憶している。これらの部位は、適宜、制御部１００により主記憶部１１０に読み出されて実行される。また、ＯＳ部２２０、モデル検査部２３０、ドライバ部２４０、及びアプリケーション部２５０は、ハイパーバイザ部２００により実行される仮想マシン３００を構成している。
なお、補助記憶部１２０は、ＨＤＤ等に記憶された上述の各部位の他に、コンピュータ１０のファームウェアやＢＩＯＳ（Ｂａｓｉｃ Ｉｎｐｕｔ／Ｏｕｔｐｕｔ Ｓｙｓｔｅｍ）等を含んでいる。これらについても、適宜、制御部１００により主記憶部１１０に読み出されて実行される。
【００１５】
ハイパーバイザ部２００は、コンピュータの仮想化技術のひとつであるバーチャルマシン（仮想機械）を実現するためのバーチャリゼーション（仮想化）レイヤ（Ｌａｙｅｒ）を構成する仮想化モニタ等の制御プログラムの部位である。すなわち、ハイパーバイザ部２００は、制御部１００に、ゲストＯＳであるＯＳ部２２０を含む仮想マシン３００を実行させるハイパーバイザである。ハイパーバイザ部２００は、複数の仮想マシン３００に、制御部１００の演算資源、メモリ資源等を効率的にスケジューリングし、ハードウェア割り込み等を用いてデバイスにアクセスする。
ハイパーバイザ部２００は、ホストＯＳを必要とせず、コンピュータ１０の主記憶部１１０に読み出されて、ハードウェア資源を用いて直接実行されるＴｙｐｅ １（ネイティブ、Ｎａｔｉｖｅ、ベアメタル、Ｂａｒｅ Ｍｅｔａｌ）方式を用いることができる。
また、ハイパーバイザ部２００は、仮想マシンのエミュレーションにより仮想化されたデバイス（以下、仮想デバイスという。）のデバイスドライバや、チップセット１５０に接続された物理的なデバイス（以下、物理デバイスという。）用のデバイスドライバを備えることができる。ハイパーバイザ部２００は、仮想マシン３００内のドライバ部２４０に対し、仮想デバイスへのアクセスに加えて、準仮想化されたデバイスへのアクセスを行わせることができる。ここで、準仮想化とは、「パラレル（平行）アクセス」又はベアメタル等と呼ばれる「直接アクセス方式」を用いて、物理デバイスにマッピングされたデバイスのメモリやＩ／Ｏに対して直接アクセスを行うことをいう。この準仮想化により、デバイスのエミュレーションのオーバーヘッド（処理遅延）を抑えることができ、リアルタイム（実時間）処理が必要なネットワーク処理やレンダリング処理等に用いることができる。
なお、ハイパーバイザ部２００として、ホストＯＳ上で動作するＴｙｐｅ ２方式の仮想化のハイパーバイザについても用いることもできる。
【００１６】
システムモニタ部２１０は、ハイパーバイザ部２２０と協同して、仮想化レイヤ上で動作するコマンド列のフィルタ等のプログラムの部位である。
システムモニタ部２１０は、仮想化レイヤにおいて、デバイスドライバとは独立に、デバイスへの操作を管理する。つまり、システムモニタ部２１０は、ＯＳ部２２０であるゲストＯＳによるデバイスの状態の遷移を仮想化レイヤにて監視し、デバイスが利用不可能となるような不正なＩ／Ｏコマンド列等（以下、不正コマンドという。）を検知する。システムモニタ部２１０は、不正コマンドの検知が行われた場合、ＯＳ部２２０の当該ゲストＯＳの停止又は当該ゲストＯＳによるそのデバイスの利用を停止する。これにより、システムモニタ部２１０は、デバイスが利用不可能となることを防ぐことができる。このように、システムモニタ部２１０は、デバイスドライバ自体を検証の対象としないため、ソースコードが入手できない商用（市販）ＯＳであるゲストＯＳにも適用することができる。また、システムモニタ部２１０は、ＯＳ部２２０のゲストＯＳのカーネルが、複数回単一のデバイスに対し操作を行った場合でも、不正な操作によりデバイスが利用不可能になることを防ぐことができる。
また、システムモニタ部２１０は、モデル検査部２３０にて動作の認証を行ったドライバ部２４０からの直接アクセスについては、Ｉ／Ｏコマンド列等の監視を行わないか、負荷を抑えた監視を行うように構成することができる。
また、システムモニタ部２１０は、このデバイスの状態の遷移について、上述したデバイスドライバのソースコードを基に、不正コマンドの監視ができる。また、システムモニタ部２１０は、チップセット１５０を介してデバイスの状態を直接監視することも可能である。この際、システムモニタ部２１０は、デバイスが正常なＩ／Ｏコマンド列により正常でない状態に遷移したことを検知して、デバイスの故障や不具合を認識することもできる。
【００１７】
モデル検査部２３０は、ソースコード等のソフトウェアのプログラムを読み、実行経路をすべて調査し、規定されたプロパティ（条件）が満たされるかどうかソフトウェアモデル（以下、モデルという。）のチェック（検査）を行うプログラムやデータの部位である。
モデル検査部は、主にゲストＯＳであるＯＳ部２２０に用いるドライバ部２４０のソースコードを用いて、このモデル検査（チェック）を行う。具体的には、モデル検査部２３０は、ドライバ部２４０のデバイスドライバのソースコードに記載されたオートマトン形式で記載されたデバイスの状態遷移の記載を基に、ソースコードとの整合性がとれているかどうかを検証するモデル検査を行う。このデバイスの状態遷移の記載については、例えば、ＣＳＬＳ（Ｃ Ｓｐｅｃｉｆｉｃａｔｉｏｎ Ｌａｎｇｕａｇｅ ｆｏｒ Ｓｙｓｔｅｍｓ ｓｏｆｔｗａｒｅ）規約を用いることができる。加えて、モデル検査部２３０は、ハイパーバイザ部２００本体が備えるデバイスドライバのモデル検査を行うこともできる。
モデル検査部２３０は、このモデル検査により、仮想化されたソフトウェア層の正確な動作を確認することに対する検証技術を提供することができる。つまり、モデル検査部２３０は、ハイパーバイザ部２００の仮想化レイヤのデバイス・ハンドラーが、ゲストＯＳがデバイスをエラー状態に導かないようにするための、正確なＩ／Ｏコマンドの順番制御（オーダー）を行う動作認証を行うことができる。このように、モデル検査部２３０により動作認証したソースコードは、最適化等したコンパイルを行い、ＯＳ部２２０のドライバ部２４０や、ハイパーバイザ部２００のデバイスドライバとしてに組み込むことができる。そして、モデル検査部２３０で動作認証されたドライバ部２４０は、直接アクセス方式のＩ／Ｏコマンドについて、システムモニタ部２１０にて検証を少なくした監視を行わせることができる。
また、モデル検査部２３０は、特に仮想化レイヤ自体の分離と、デバイスの正確な動作を保証するために、カーネル構築時やドライバ部２４０の更新時に最初に実行することが望ましい。
また、モデル検査部２３０は、ＯＳ部２２０を用いて実行されるアプリケーション・ソフトウェアとして実装することができる。つまり、モデル検査部２３０は、ＯＳ部２２０の仮想マシン内の他のアプリケーションと連動させて実行することができる。
【００１８】
なお、モデル検査部２３０は、ハイパーバイザ部２００と同様の仮想化レイヤで実行されるように構成することもできる。この場合、モデル検査部２３０は、仮想化レイヤで実行されるため、直接アクセスのＩ／Ｏコマンド列を容易に検知して、このオートマトンの状態によりモデル検査を行うことができる。
また、モデル検査部２３０は、ハイパーバイザ部２００やシステムモニタ部２１０と同じモジュールや構成部位として備えられていてもよい。この場合でも、モデル検査部２３０は、ハイパーバイザ部２００やシステムモニタ部２１０と同時並行的には動作させないで検証のみ行うことで、動作を軽くすることができる。
また、モデル検査部２３０は、ドライバ部２４０のドライバのソースコードをチェックするだけでなく、オートマトンによる状態遷移であれば、任意のものを検査可能である。つまり、モデル検査部２３０は、アプリケーション部２５０の通常のウェブブラウザや計算ソフトウェア等の各種アプリケーションのソースコードに状態遷移を記載して、動作のチェックをさせることもできる。
また、ソースコードが存在しない市販ＯＳの場合には、このモデル検査部２３０を用いない構成も可能である。
【００１９】
仮想マシン３００は、エミュレートされた仮想のコンピュータ、すなわち仮想マシン（Ｖｉｒｔｕａｌ Ｍａｃｈｉｎｅ、仮想機械）環境である。仮想マシン３００は、１つ又は複数の仮想マシンを用いることができる。各仮想マシンは、ハイパーバイザ部２００により自動的に制御部１００のＣＰＵコア等に動的に割り当られ、同時又は切り換えられて実行される。
仮想マシン３００は、ＨＤＤ等の同一のパーティション又は複数のパーティションや複数の物理的な補助記憶装置を用いて構成することができる。また、仮想マシン３００は、ｉＳＣＳＩ等を用いて、ネットワーク上のストレージ上のイメージとして構成することもできる。さらに、仮想マシン３００は、仮想ＨＤＤイメージ形式等を用いて、別のＯＳのパーティションにファイルとして含ませることもできる。
【００２０】
ＯＳ部２２０は、ハイパーバイザ部２００により仮想化されて実行される１つ又は複数のゲストＯＳを含む部位である。ＯＳ部２２０は、仮想マシン３００毎に用意することができる。また、ＯＳ部２２０は、ハイパーバイザ部２００がホストＯＳにより実行されるＴｙｐｅ ２方式の仮想化のハイパーバイザであった場合、このホストＯＳも含む。
ＯＳ部２２０は、ＵＮＩＸ（登録商標）、Ｌｉｎｕｘ（登録商標）、ＦｒｅｅＢＳＤ（登録商標）等の、ソースコードを基にカーネルやドライバ等をビルド（再構成）が可能な各種ＯＳをゲストＯＳとして用いることができる。さらに、ＯＳ部２２０は、ＭＡＣ（登録商標）ＯＳ、ウィンドウズ（登録商標）等の、通常はソースコードによりビルドしない市販ＯＳを用いることもできる。
【００２１】
ドライバ部２４０は、周辺機器、ネットワーク等のデバイス（機器）と接続の制御プログラムであるデバイスドライバ（以下、ドライバという。）の部位である。ドライバ部２４０は、ＯＳ部２２０に備わったＡＰＩ（Ａｐｐｌｉｃａｔｉｏｎ Ｐｒｏｇｒａｍ Ｉｎｔｅｒｆａｃｅ）を用いたり、逆にＯＳ部２２０に組み込まれてＡＰＩを提供した上で、ハイパーバイザ部２００がエミュレーションを行う仮想デバイスにアクセスする。さらに、ドライバ部２４０は、オーバーヘッドが顕著なデバイス、例えばネットワークカード、ＲＡＩＤ（Ｒｅｄｕｎｄａｎｔ Ａｒｒａｙｓ ｏｆ Ｉｎｅｘｐｅｎｓｉｖｅ Ｄｉｓｋｓ）等の補助記憶インターフェイス、ビデオボード、ストリーミング映像デバイス等に関しては、準仮想化により物理デバイスへ直接アクセスが可能である。
ドライバ部２４０は、ソースコードがあるドライバをコンパイルした実行ファイルを用いることが可能である。この際に、上述のモデル検査部２３０により認証されたドライバについては、ＩＤ（Ｉｄｅｎｔｉｆｉｃａｔｉｏｎ）を付加したＩ／Ｏコマンドを用いて直接アクセスを行い、システムモニタ部２１０に認識させることができる。また、ドライバ部２４０は、ソースコードがない市販ＯＳ等の、認証されていないドライバを用いることも可能である。
【００２２】
アプリケーション部２５０は、仮想マシン３００上のＯＳ部２２０にて実行される各種のアプリケーション・ソフトウェアである。
このアプリケーション・ソフトウェアは、ＯＳ部２２０のＡＰＩを用いて、ドライバ部２４０により、各種の物理デバイスや仮想デバイスにアクセスできる。
このアプリケーション・ソフトウェアとしては、ドライバ部２４０のソースコードのあるドライバをチェックするモデル検査部２３０と、これと連動するソースコードデバッガ等を含ませることができる。また、アプリケーション・ソフトウェアとして、ソースコードをコンパイル等するｃｃ等のコンパイラやビルドを行うｍａｋｅ等の各種ソフトウェアを含ませることができる。さらに、仮想マシン３００やＯＳ部２２０やドライバ部２４０が停止した際のログ等を閲覧するソフトウェアを用いることもできる。加えて、別の仮想マシン３００が停止して当該仮想マシン３００に切り換えられた際に報知する警報ソフトウェア等を用いることができる。
【００２３】
〔デバイス状態遷移管理処理〕
次に、図２〜図７を参照して、本発明の実施の形態に係るデバイス管理方法に係るデバイス状態遷移管理処理について説明する。
ここで、本発明の実施の形態のハイパーバイザ部２００は、上述したように準仮想化による直接アクセス方式を許容する。このハードウェアの規格に従った物理デバイスへのアクセスを行わないと、物理デバイスが使用不可能になることがある。この場合、当該デバイスをリセットするか、場合によっては、コンピュータ１０自体をリセットする必要がある。
このため、本発明の実施の形態に係るコンピュータ１０は、ハイパーバイザ部２００に加えて、ゲストＯＳのドライバが正確な方法で物理デバイスのハードウェアを管理するかどうかチェックするための機構であるシステムモニタ部２１０を用いる。
これに加えて、本実施形態に係るデバイス状態遷移管理処理では、仮想マシン３００内のドライバ部２４０に対して、モデル検査部２３０により、モデル検査による認証を行う。この上で、この認証されたドライバからの直接アクセスを、システムモニタ部２１０により監視する。
これにより、ゲストＯＳのカーネルによるデバイスのアクセスについて、オーバーヘッドが少ない直接アクセスを用いた場合でも、デバイスが使用不可能になることを防ぐことができる。
以下で、図２のフローチャートを用いて、デバイス状態遷移管理処理の各処理について説明する。
【００２４】
（ステップＳ１０１）
まず、制御部１００は、モデル検査部２３０を用いてドライバ部２４０のドライバ等のソースコードをモデル検査するドライバチェック処理を行う。
このドライバチェック処理では、デバイスへの操作が仕様を満たすかどうかを検査するために、モデル検査を用いる。
具体的には、制御部１００は、デバイスの状態遷移について上述のＣＳＬＳ規約によりオートマトンとして記載されたソースコードをコンパイルし、ステップ実行等を行う。その上で、制御部１００は、デバイスの状態が当該オートマトンに従って正しく遷移するか否かについて判定する。
この際、制御部１００は、モデル検査部２３０により、ゲストＯＳがシステムモニタ部２１０により停止させられないように、実際には直接アクセス方式で物理デバイスにアクセスしないように構成することが好適である。また、逆に、制御部１００は、直接アクセス方式により状態が遷移した物理デバイスの状態や仮想デバイスの状態を、遷移の情報として取得して検証することが可能である。
制御部１００は、所定ステップの間、デバイスが正しく遷移したと考えられる場合、そのドライバのオブジェクトや実行コードに所定のＩＤを付加する「認証」を行う。
これにより、認証されたドライバからの直接アクセスの際には、システムモニタ部２１０が検知してオーバーヘッドを抑える処理を行うことができる。
【００２５】
（ステップＳ１０２）
次に、制御部１００は、システムモニタ部２１０を用いて、仮想マシン３００からの物理デバイスへの直接アクセスを管理するシステムモニタ処理を行う。
この処理では、仮想化レイヤにおいて、ハイパーバイザ部２００が備えるデバイスドライバとは独立に、デバイスへのアクセスを管理する。
具体的には、制御部１００は、ドライバ部２４０からの準仮想化による直接アクセスを検知する。この上で、直接アクセスの際、制御部１００は、不正コマンド等により物理デバイスが不正な状態遷移となる「不正アクセス」がされているかを検知する。そして、制御部１００は、不正アクセスが検知された場合に、仮想マシン３００の停止等を行う。
このような不正アクセスにより、コンピュータ１０自体が動作不良やハングアップする可能性がある。よって、システムモニタ部２１０を用いてチェックすることで信頼性を高めることができる。
また、制御部１００は、物理デバイス自体の状態遷移について、システムモニタ部２１０を用いて検査する。この上で、制御部１００は、上述の認証されたドライバのアクセスにより不正な遷移となった場合、物理デバイスの故障を報知する。
以上により、デバイス状態遷移管理処理を終了する。
【００２６】
〈ドライバチェック処理の詳細〉
次に、図３〜図５を参照して、本発明の実施の形態に係るドライバチェック処理の詳細について説明する。これらの処理は、制御部１００は、モデル検査部２３０を用いて実行する。
以下、図３のフローチャートを基に、各処理の詳細について説明する。
【００２７】
（ステップＳ２０１）
まず、制御部１００は、初期化処理を行う。
この処理では、まず、制御部１００は、モデル検査を行うドライバ等のソースコードが存在するか判断する。
次に、制御部１００は、当該ソースコードにデバイスの状態遷移に関するオートマトンの記載があるか否かを判断する。ここで、ソースコードの全てにオートマトンの記載を行う必要はない。よって、制御部１００は、物理デバイスにアクセスする部分のソースファイル等、一部について記載があれば、記載ありと判断する。
ソースコードにオートマトンの記載があった場合、制御部１００は、このソースコードを、パーサ等を用いて解釈する。この上で、制御部１００は、リスト等のデータ構造を用いて実際のオートマトンのデータを主記憶部１１０に作成する。
なお、制御部１００は、ソースコードがなかったり、ソースコードにオートマトンの記載がなかったりした場合には、エラーとして処理を終了する。
【００２８】
（ステップＳ２０２）
次に、制御部１００は、コンパイル処理を行う。
具体的には、制御部１００は、ソースコードの言語に係るコンパイラを、パイプ等を用いて起動する。
この上で、制御部１００は、上述のドライバのソースコードを読み込ませ、コンパイルさせる。
このコンパイルにおいては、最適化を行わない「デバッグ」モードのシンボルを付加したコンパイルを行うことが好適である。
【００２９】
（ステップＳ２０３）
次に、制御部１００は、モデル遷移チェック処理を行う。
このモデル遷移チェック処理においては、制御部１００は、モデルチェック部は、コンパイルされたドライバについて、ステップ実行等を行う。このステップ実行は、統合開発環境のソースレベルデバッガ等と連動させることができる。
この上で、制御部１００は、ステップ毎にオートマトンの状態を検査する。
このモデル遷移チェック処理の詳細な実行例については後述する。
【００３０】
（ステップＳ２０４）
次に、制御部１００は、オートマトンが正しい遷移を示しているか否か判定する。
Ｙｅｓ、すなわちオートマトンの状態が正しい遷移を示している場合、制御部１００は、処理をステップＳ２０６に進める。
Ｎｏ、すなわちオートマトンの状態が不正な遷移を示している場合は、制御部１００は、処理をステップＳ２０５に進める。
【００３１】
（ステップＳ２０５）
オートマトンが不正な遷移を示していた場合、制御部１００は、エラー処理を行う。
この不正な遷移をした場合、当該デバイスはエラー状態等となり使用不可能となる、すなわちプログラムの不正な箇所（バグ）があると考えられる。よって、デバイスドライバのソースコード自体を変更する必要がある。
このため、制御部１００は、エラーを起こした箇所をソースレベルデバッガ等に報知する。
この際、制御部１００は、当該ソースレベルデバッガ等により、オートマトンの遷移図等と、停止箇所を示す。これにより、ユーザにソースコードの不正箇所を知る手がかりを与えることができる。
その後、制御部１００は、ドライバチェック処理を終了する。
【００３２】
（ステップＳ２０６）
オートマトンが正しい遷移を示していた場合、制御部１００は、ステップ実行が終了したか否かについて判定する。
ここでは、制御部１００は、所定回数のステップ実行したか、ソースコードに様々なパラメータを与えてほぼ全ての状態遷移の実行を終えた場合、ステップ実行の終了と判断する。また、制御部１００は、オートマトンの状態から全ての状態遷移を検査したと判断できた場合等にも、ステップ実行の終了と判断することができる。
Ｙｅｓ、すなわちステップ実行が終了した場合、制御部１００は、処理をステップＳ２０７に進める。
Ｎｏ、すなわちまだステップ実行を行う必要がある場合、制御部１００は、処理をステップＳ２０３に戻してモデル検査を続ける。
【００３３】
（ステップＳ２０７）
ステップ実行が終了した場合、制御部１００は、デバイスドライバ認定処理を行う。
具体的には、制御部１００は、直接アクセスを行っても物理デバイスを停止等させる可能性が少ないドライバであるとして、認証を行う。
この処理においては、制御部１００は、最適化を行った上でデバイスドライバをコンパイルする。この際、制御部１００は、システムモニタ部２１０の公開鍵や秘密鍵等を基に、ハッシュ関数等を用いて、不正な認証ができないようなＩＤを作成して、このＩＤをソースコードやオブジェクトやバイナリ（実行）コード等に埋め込む。また、制御部１００は、モデル検査部２３０がソースコードを解析して作成したオートマトンのデータについても、ＩＤと共に埋め込むことができる。
これにより、認証されたドライバは、物理デバイスへの直接アクセスの際に、このＩＤを用いることができる。これにより、システムモニタ部２１０の管理の負荷を軽減できる。
以上により、ドライバチェック処理を終了する。
【００３４】
〈モデル遷移チェック処理の実施例〉
ここで、モデル遷移チェック処理の具体例について、図４Ａ〜図５を参照して詳細に説明する。
上述したように、このモデル遷移チェック処理では、ＯＳ部２２０のゲストＯＳに、物理デバイスの規定に従った正確な振る舞いを強いるための機構を提供する。
この際、本発明の実施の形態においては、制御部１００が、モデル検査部２３０を用いて、ドライバ部２４０が正確な方法でハードウェアを管理するかどうか検査する。
以下では、仮想マシン３００のドライバ部２４０について、ＲＳ−２３２規格等のシリアル・インターフェイスのドライバを用いてモデル検査を行った実施例について説明する。
この実施例では、仮想マシン３００のドライバ部２４０のシリアルデバイス・ハンドラーのモデル検査を行って、シリアルデバイスがエラー状態にならないように正確な命令動作をすることを確認した。
これにより、ドライバ部２４０が、ハイパーバイザ部２００下の仮想マシン３００によって正確に動作することを確認することができる。
【００３５】
（文字の送信）
まず、図４Ａを参照して、ドライバ部２４０のシリアルデバイスのドライバによる文字の送信について説明する。オートマトン２４５は、このドライバ部２４０の状態遷移を示す。
シリアルライン上の文字を送信するために、制御部１００は、ドライバ部２４０の動作として、以下の工程に従う必要がある。
まず、図４Ａのシリアルドライバの最初の工程（１）として、制御部１００は、ｓｅｎｄ（送信）バッファが空かどうかチェックする。
次に、制御部１００は、送信バッファが空か否かチェックして、空の場合、次の工程（２）に進める。そうでなければ、制御部１００は、送信バッファが空になるまで待つ。
その後、制御部１００は、送信バッファに文字を書き込む。
ここで、バッファがフルのとき、ドライバが文字を書き込むと、オートマトン２４５のデバイスの状態はエラー状態になる。制御部１００は、このエラー状態となったことを検知して、モデル検査部２３０に報知することができる。
【００３６】
上述のシリアルデバイスの状態遷移は、モデル化することができる。
以下に、バッファが空であるか否かをチェックするｓｅｒ＿ｉｓ＿ｒｅａｄｙ＿ｔｏ＿ｓｅｎｄ（）関数の例を示す。このｓｅｒ＿ｉｓ＿ｒｅａｄｙ＿ｔｏ＿ｓｅｎｄ（）関数は、バッファの状態を検知し、送信が準備可能かどうかを返す。
【００３７】
/*@
$ensures((ser_tx_ready == 1) ||
(ser_tx_ready == 0));
*/
int ser_is_ready_to_send(void)
{
int thre = hw_uart_lsr_thre();
if (thre)
ser_tx_ready = 1;
else
ser_tx_ready = 0;
return thre;
}
【００３８】
また、以下は、バッファが空で送信可能な場合、バッファに文字を書き出すｓｅｒ＿ｓｅｎｄ（）関数の例を示す。
ｓｅｒ＿ｓｅｎｄ（）関数は、バッファが空及び送信要求である場合、バッファに文字を書き、そうでなければ、エラーをモデル検査部２３０に返す。
なお、制御部１００は、実際にコンパイル後のドライバがドライバ部２４０やハイパーバイザ部２００に組み込まれた際、このエラーの場合には、ハイパーバイザ部２００が当該仮想マシン３００を停止するように通知することもできる。
【００３９】
/*@
$ensures($old(ser_tx_ready) == 0
==> need_to_kill_vm == 1);
*/
void ser_send(int ch)
{
if (ser_tx_ready == 0)
need_to_kill_vm = 1;
ser_tx_ready = 0;
hw_uart_tx(ch);
}
【００４０】
この例のように、デバイスの状態遷移に関するオートマトンの記載は、Ｃ言語の場合には、上述したＣＳＬＳ規約により、／＊＠ ＊／のようなコメント行を用いて記載することができる。
通常のコンパイラでは、この記載はコメント行として無視されるため、汎用性を高めることができる。
【００４１】
（文字の送信）
次に、図４Ｂを参照して、ドライバ部２４０のシリアルデバイスのドライバによる文字の受信について説明する。オートマトン２４６は、このドライバ部２４０の状態遷移を示す。
文字の受信は、上述の文字の送信と同様の方法でモデル化することができる。
ドライバ部２４０のシリアルドライバは、シリアルライン上の文字を受信するために下記の動作を行う。
まず図４Ｂの最初の工程（１）において、制御部１００は、受信バッファにおいてデータ受信の準備ができているかどうかチェックする。準備ができている場合、次の工程（２）に移る。そうでなければ、制御部１００は、データの準備ができるまで待つ。
この上で、制御部１００は、受信バッファから文字を読み出す。
一方、データがない場合に、受信バッファから文字を読み出すと、制御部１００はエラーをモデル検査部２３０に報知する。
【００４２】
このように、制御部１００は、モデル検査部２３０を用いてプログラムの誤動作を検知できる。
図５は、このモデル検査の結果を示す画面例である。この例では、「Ｐｒｏｇｒａｍ ｉｓ ＳＡＦＥ」即ち、安全なドライバであると検査されている。
このように、仮想化レイヤにおいて、誤操作がいつ行なわれるか実際にモデル検査により確認することができる。
したがって、不正アクセスをしない正確な動作を行うドライバ部２４０を得ることが可能になる。
これにより、信頼性が高く高パフォーマンスの仮想マシンを提供することができる。
【００４３】
なお、制御部１００は、エラー状態の報知について、検証した後のドライバ部２４０により、システムモニタ部２１０やハイパーバイザ部２００に対して報知することもできる。
これにより、万一のエラーの際には、ハイパーバイザ部２００が物理デバイスにアクセスしないように構成することができ、検証されたドライバ部２４０による不正アクセスを防ぐことが可能になる。
このため、本発明の実施の形態に係るコンピュータ１０を、非常に高度の信頼性が求められる生命維持、生産プラント、乗り物の制御といった分野に用いることができる。
【００４４】
〈システムモニタ処理の詳細〉
次に、図６及び図７を参照して、本発明の実施の形態に係るシステムモニタ処理の詳細について説明する。これらの処理は、上述したように、制御部１００が、システムモニタ部２１０を用いて、仮想化レイヤ上で実行する。
以下、図６のフローチャートを用いて、各処理の詳細について説明する。
【００４５】
（ステップＳ３０１）
まず、制御部１００は、ドライバ認証検知処理を行う。
この処理では、仮想マシン３００のドライバ部２４０が、上述のドライバチェック処理により認証されたドライバであるか検知する。
具体的には、制御部１００は、ドライバ部２４０のドライバに認証によるＩＤ等があるか否か、秘密鍵等を用いて検証する。
ここで、ドライバ部２４０のドライバが認証されたものであった場合、制御部１００は、このＩＤを用いた物理デバイスへのアクセスについては、後述するフィルタ処理にて不正アクセスであるかを検知しないか負荷を抑えた「軽い」検知のみ行う。
【００４６】
（ステップＳ３０２）
次に、制御部１００は、Ｉ／Ｏコマンド読み込み処理を行う。
図７を参照して説明すると、制御部１００は、ハイパーバイザ部２００が実行する仮想マシン３００のゲストＯＳのドライバ部２４０から、デバイスへアクセスするＩ／Ｏコマンド（指示信号）があったかどうかを検知する。つまり、制御部１００は、仮想化レイヤにおいて、デバイスドライバとは独立して、デバイスへの操作を管理する。
制御部１００は、デバイスへのアクセスするＩ／Ｏコマンドを検知した場合、ハイパーバイザ部２００に通知する。
このドライバ部２４０からのデバイスへアクセスするＩ／Ｏコマンドは、仮想レイヤへのハイパーバイザコール形式で行うことが好適である。この際、制御部１００は、チップセット１５０に接続された物理デバイスへの指示を行うＩ／Ｏコマンドに加えて、仮想デバイスのコマンドも検知する。また、制御部１００は、ドライバのＩ／Ｏコマンド毎にＩＤを検知することができる。
【００４７】
（ステップＳ３０３）
次に、制御部１００は、デバイスへアクセスするＩ／Ｏコマンドが、直接アクセスのＩ／Ｏコマンドであったか否かについて判定する。
Ｙｅｓの場合、制御部１００は、処理をステップＳ３０４に進める。
Ｎｏの場合、制御部１００は、処理をステップＳ３０７に進める。
【００４８】
（ステップＳ３０４）
次に、制御部１００は、フィルタ処理を行う。
具体的には、制御部１００は、直接アクセスのＩ／Ｏコマンド列が、デバイスの状態遷移を不正にする、不正コマンドである場合、これを不正アクセスとして検知する。
このデバイスの状態遷移については、ハイパーバイザ部２００の物理デバイス用のドライバに対応するオートマトンを用意しておいて、このオートマトンの状態遷移がエラーになるか否かについて検知する。
このオートマトンとしては、上述のモデル検査部２３０が作成したドライバ部２４０のオートマトンを用いることができる。この際、異なるゲストＯＳを備えた仮想マシン３００であっても、同一の物理デバイス／仮想デバイスについては、同一のオートマトンを用いることができる。
このように、オートマトンを用いて不正コマンドを検知するため、ハイパーバイザ部２００が仮想マシン３００を切り換えた際、デバイスの動作タイミング等が原因で各仮想マシン３００からの物理デバイスからのアクセスが不正コマンドになった場合でも対応できる。
また、仮想マシン３００から、複数回、単一のデバイスに対しＩ／Ｏコマンドによるアクセスを行った場合でも対応できる。
このため、不正コマンドによりデバイスが利用不可能になることを防ぐことが可能になる。
【００４９】
ここで、直接アクセスのＩ／Ｏコマンド列が、上述の認証されたドライバ部２４０のドライバからのＩ／Ｏコマンド列であった場合、制御部１００は、例えば、オートマトンの状態遷移の変化を行わないような処理を行うことが可能である。また、例えば、検知のフィルタ自体をスルー（通過）させることもできる。これにより、仮想化のオーバーヘッドを減らし、負荷を抑えて、安全に物理デバイスにアクセスさせることができる。
この場合でも、ドライバ部２４０のドライバ自体がオートマトンを持って状態遷移がエラーになった場合には、システムモニタ部２１０に報知することができるため、安全に物理デバイスにアクセス可能である。
【００５０】
（ステップＳ３０５）
次に、制御部１００は、不正アクセスであるか否かについて判定する。
ここでは、上述なようにオートマトンの状態遷移により、物理デバイスのアクセスに係る不正コマンドを検知した場合、不正アクセスである、すなわちＹｅｓと判断する。それ以外の場合はＮｏと判断する。
Ｙｅｓの場合、制御部１００は、処理をステップＳ３０６に進める。
Ｎｏの場合、制御部１００は、処理をステップＳ３０７に進める。
【００５１】
（ステップＳ３０６）
制御部１００は、不正アクセスであった場合、ゲストＯＳ停止処理を行う。
具体的には、制御部１００は、ハイパーバイザ部２００へ、不正アクセスをした仮想マシン３００を停止するように指示する。
この際、仮想マシン３００を直接停止させるのではなく、仮想マシン３００のドライバ部２４０の当該デバイスドライバに「エラー」の通知を返信することが可能である。この場合でも、当該デバイスドライバが停止しない場合、制御部１００は、ＯＳ部２２０にエラーを報知することができる。これにより、ＯＳ部２２０のエラー対応機能によりドライバ部２４０の当該デバイスドライバを停止させることもできる。しかしながら、この場合でもＯＳ部２２０が反応しない場合、制御部１００は、仮想マシン３００自体を停止することができる。このような構成により、コンピュータ１０の動作の停止時間や再起動の時間等を少なくすることができる。
システムモニタ部２１０は、仮想マシン３００やＯＳ部２２０やドライバ部２４０を停止させた場合には、ハイパーバイザ部２００に通知し、更に表示部や音声入出力部やシリアルデバイス等に警告を報知することができる。そして、制御部１００は、エラーの内容を表示部等やネットワークを介した監視機器等に報知し、ログを作成する。
【００５２】
（ステップＳ３０７）
次に、制御部１００は、物理デバイス遷移検査処理を行う。
この処理においては、制御部１００は、当該物理デバイスの状態を、チップセット１５０を介して取得する。
制御部１００は、この取得について、ハイパーバイザ部２００の情報を取得し、主に直接アクセスのＩ／Ｏコマンド列により物理デバイスを動作させた後に行う。
この上で、制御部１００は、この物理デバイスの状態が、オートマトンにより想定された状態遷移であるか否かを判断する。
制御部１００は、物理デバイスが想定された遷移の状態（ステート）でなかった場合には、不正な遷移をしていると検知する。特に、制御部１００は、認証されたドライバからのアクセスがあったにも関わらず、物理デバイスがエラー状態になっていることを検知した場合、起こり得ないことが起こったとして、デバイスが故障したと検知する。
【００５３】
（ステップＳ３０８）
制御部１００は、物理デバイスが不正な状態遷移をしているか否か判定する。ここでは、制御部１００は、上述の不正な状態遷移であった場合には、Ｙｅｓと判定する。
Ｙｅｓ、すなわち不正な状態遷移があった場合、制御部１００は処理をステップＳ３０９に進める。
Ｎｏ、すなわち物理デバイスの状態遷移が想定していた状態遷移であった場合、制御部１００は処理をステップＳ３０２に戻して、管理を続ける。
【００５４】
（ステップＳ３０９）
制御部１００は、ここでは、故障報知処理を行う。
この処理においては、制御部１００は、ハイパーバイザ部２００、表示部等やネットワークを介した監視機器等に、不正な遷移をした物理デバイスの故障を報知する。この際に、表示部や音声入出力部やシリアルデバイス等に警告を報知することもできる。
なお、不正アクセスでドライバや仮想マシン３００を停止した場合にも、制御部１００は、報知を行って、システムモニタ処理を停止するように構成することもできる。
以上により、システムモニタ処理を終了する。
【００５５】
以上のように構成することで、以下のような効果を得ることができる。
本発明の実施の形態に係るコンピュータ１０は、デバイスへのアクセスを仮想化レイヤのシステムモニタ部２１０でフィルタして、デバイスの状態遷移を管理する。
すなわち、本発明の実施の形態に係るコンピュータ１０は、仮想マシン３００上でゲストＯＳであるＯＳ部２２０を実行する。この上で、ゲストＯＳによるデバイスのアクセスを、仮想化レイヤのシステムモニタ部２１０が監視し、デバイスが利用不可能となる不正な操作を検知したら、ゲストＯＳの停止又はゲストＯＳによるそのデバイスの利用を停止する。具体的には、本実施形態に係るシステムモニタ部２１０は、準仮想化による直接アクセスの際、物理デバイスに不正なＩ／Ｏコマンド列等でアクセスすると、仮想マシン３００又はドライバ部２４０を停止させることができる。
これにより、仮想マシン３００内のソフトウェアからのデバイスへのアクセスにより、当該デバイスが利用不可能になることを防ぐことができる。
また、システムモニタ部２１０は、デバイスドライバからのアクセスのＩ／Ｏコマンド自体を管理するため、ソースコードが入手できない商用（市販）ＯＳにも適用できる。
また、システムモニタ部２１０は、ゲストＯＳから複数回、単一のデバイスに対しアクセスがされた場合でも、そのデバイスの状態遷移を検知する。これにより、不正なＩ／Ｏコマンド列によりデバイスが利用不可能になることを防ぐことができる。
【００５６】
これにより、安定稼働が必要なコンピュータ１０に適用することができる。
すなわち、デバイスが利用不可能となることが被害や損害につながるような機器での利用、例えば、医療機器やインフラ系等のコンピュータに利用できる。
【００５７】
また、本発明の実施の形態に係るシステムモニタ部２１０は、仮想化レイヤに対する直接アクセスに対してだけ、ハードウェアのデバイスの仕様に従ったアクセスであるか管理する。この際、物理デバイスの状態遷移が想定から外れた場合に、ゲストＯＳ又はドライバを稼働停止させられる。
これにより、仮想マシン３００からの物理デバイスへのアクセスにより当該物理デバイスがエラー状態となることを防ぐことができる。よって、コンピュータ１０を安定して稼働することができる。
【００５８】
また、従来技術１は、デバイスドライバそのものを検証することによりデバイスへの操作が正しいことを保証するものであった。このため、従来技術１は、デバイスの共有が起こる仮想化環境に直接適用することができなかった。
これに対して、本発明の実施の形態に係るモデル検査部２３０は、仮想化レイヤに対するアクセスのＩ／Ｏコマンド列に関するモデル検査を行うことで、仮想化された環境でも適用することができる。
【００５９】
また、従来技術１のソースコードの検査では、ホーア論理を用いてドライバの動作の正しさを証明するため非常に手間がかかるという問題があった。つまり、従来技術１では、ユーザが各種パラメータ等を変えてデバイスドライバを検査する必要があった。
これに対して、本発明の実施の形態に係るモデル検査部２３０は、オートマトンの状態遷移を用いてドライバのモデル検査を行うため、自動的にデバイスドライバの検査を行うことができる。これにより、高速に手間が少なくドライバの検査ができる。
【００６０】
また、本発明の実施の形態に係るモデル検査部２３０は、モデル検査を行ったドライバを認証する。
これにより、システムモニタ部２１０は、認証されたドライバからの物理デバイスへのアクセスに際して、負荷を抑えたフィルタリングを行うことができる。
よって、仮想化によるオーバーヘッドを少なくしたまま、コンピュータ１０を安全に稼働させられる。
このため、ネットワークのコントローラ等のパフォーマンスが必要なハードウェア資源のアクセスを高速化できる。つまり、例えば、ネットワークカードに適用した場合、ｉＳＣＳＩ等により接続されたネットワークストレージのアクセススピードを高速化できる。
【００６１】
本発明の実施の形態に係るシステムモニタ部２１０は認証されたドライバが物理デバイスへアクセスをした際に、当該物理デバイスの状態遷移が不正であった場合には、当該物理デバイスの故障と検知することができる。
これにより、不正アクセスの検知と、物理デバイスの故障の検知とを同一環境で行うことができ、コンピュータ１０に問題が起こった場合に、迅速に解決できる。よって、コンピュータ１０の運用コストを低下させることができる。
【００６２】
なお、上記実施の形態の構成及び動作は例であって、本発明の趣旨を逸脱しない範囲で適宜変更して実行することができることは言うまでもない。
【産業上の利用可能性】
【００６３】
本発明の計算機は安全な稼働をさせることができるため、デバイスが利用不可能となることが被害や損害につながるような計算機に用いることができ、産業上に利用することができる。
【符号の説明】
【００６４】
１０ コンピュータ
１００ 制御部
１１０ 主記憶部
１２０ 補助記憶部
１５０ チップセット
２００ ハイパーバイザ部
２１０ システムモニタ部
２２０ ＯＳ部
２３０ モデル検査部
２４０ ドライバ部
２４５、２４６ オートマトン
２５０ アプリケーション部
３００ 仮想マシン
【特許請求の範囲】
【請求項１】
仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ部と、
デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ部に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ部とを備える
ことを特徴とする計算機。
【請求項２】
前記ゲストＯＳの前記デバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行うかを、オートマトンの状態遷移により検査して認証するモデル検査部を備える
ことを特徴とする請求項１に記載の計算機。
【請求項３】
前記システムモニタ部は、前記モデル検査部で認証されたデバイスドライバからの直接アクセスがあった場合、負荷を抑えて前記デバイスにアクセスさせる
ことを特徴とする請求項２に記載の計算機。
【請求項４】
前記システムモニタ部は、前記モデル検査部で用いた前記オートマトンにより、前記ハードウェアの仕様に従ったアクセスを行うか否かフィルタリングする
ことを特徴とする請求項２又は３に記載の計算機。
【請求項５】
前記システムモニタ部は、前記認証されたデバイスドライバが前記デバイスのアクセスをした際に、前記デバイスの状態遷移が不正であった場合には、前記デバイスの故障と検知する
ことを特徴とする請求項２乃至４のいずれか１項に記載の計算機。
【請求項６】
コンピュータのデバイスの状態遷移を管理するデバイス管理方法において、
前記コンピュータは、仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、仮想化レイヤにて前記デバイスの管理を行うシステムモニタ手段とを備え、
前記システムモニタ手段により、前記デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知する
ことを特徴とするデバイス管理方法。
【請求項７】
コンピュータを、
仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、
デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段
として機能させるためのプログラム。
【請求項８】
コンピュータを、
仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、
デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段
として機能させるためのプログラムを記録したコンピュータ読み取り可能な記録媒体。
【請求項１】
仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ部と、
デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ部に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ部とを備える
ことを特徴とする計算機。
【請求項２】
前記ゲストＯＳの前記デバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行うかを、オートマトンの状態遷移により検査して認証するモデル検査部を備える
ことを特徴とする請求項１に記載の計算機。
【請求項３】
前記システムモニタ部は、前記モデル検査部で認証されたデバイスドライバからの直接アクセスがあった場合、負荷を抑えて前記デバイスにアクセスさせる
ことを特徴とする請求項２に記載の計算機。
【請求項４】
前記システムモニタ部は、前記モデル検査部で用いた前記オートマトンにより、前記ハードウェアの仕様に従ったアクセスを行うか否かフィルタリングする
ことを特徴とする請求項２又は３に記載の計算機。
【請求項５】
前記システムモニタ部は、前記認証されたデバイスドライバが前記デバイスのアクセスをした際に、前記デバイスの状態遷移が不正であった場合には、前記デバイスの故障と検知する
ことを特徴とする請求項２乃至４のいずれか１項に記載の計算機。
【請求項６】
コンピュータのデバイスの状態遷移を管理するデバイス管理方法において、
前記コンピュータは、仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、仮想化レイヤにて前記デバイスの管理を行うシステムモニタ手段とを備え、
前記システムモニタ手段により、前記デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知する
ことを特徴とするデバイス管理方法。
【請求項７】
コンピュータを、
仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、
デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段
として機能させるためのプログラム。
【請求項８】
コンピュータを、
仮想化レイヤにてゲストＯＳを動作させるハイパーバイザ手段と、
デバイスの状態遷移を管理し、前記ゲストＯＳのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段
として機能させるためのプログラムを記録したコンピュータ読み取り可能な記録媒体。
【図１】
【図２】
【図３】
【図４Ａ】
【図４Ｂ】
【図５】
【図６】
【図７】
【図２】
【図３】
【図４Ａ】
【図４Ｂ】
【図５】
【図６】
【図７】
【公開番号】特開２０１３−８１８８（Ｐ２０１３−８１８８Ａ）
【公開日】平成２５年１月１０日（２０１３．１．１０）
【国際特許分類】
【出願番号】特願２０１１−１４０２６４（Ｐ２０１１−１４０２６４）
【出願日】平成２３年６月２４日（２０１１．６．２４）
【国等の委託研究の成果に係る記載事項】（出願人による申告）平成２２年度、平成２３年度、独立行政法人科学技術振興機構、戦略的創造研究推進事業、産業技術力強化法第１９条の適用を受ける特許出願
【出願人】（５０４１７１１３４）国立大学法人 筑波大学 (510)
【公開日】平成２５年１月１０日（２０１３．１．１０）
【国際特許分類】
【出願日】平成２３年６月２４日（２０１１．６．２４）
【国等の委託研究の成果に係る記載事項】（出願人による申告）平成２２年度、平成２３年度、独立行政法人科学技術振興機構、戦略的創造研究推進事業、産業技術力強化法第１９条の適用を受ける特許出願
【出願人】（５０４１７１１３４）国立大学法人 筑波大学 (510)
[ Back to top ]