仮想化レイヤにてゲストOSを動作させるハイパーバイザ部と、デバイスの状態遷移を管理し、前記ゲストOSのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ部に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ部とを備えることを特徴とする計算機。前記ゲストOSの前記デバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行うかを、オートマトンの状態遷移により検査して認証するモデル検査部を備えることを特徴とする請求項1に記載の計算機。前記システムモニタ部は、前記モデル検査部で認証されたデバイスドライバからの直接アクセスがあった場合、負荷を抑えて前記デバイスにアクセスさせることを特徴とする請求項2に記載の計算機。前記システムモニタ部は、前記モデル検査部で用いた前記オートマトンにより、前記ハードウェアの仕様に従ったアクセスを行うか否かフィルタリングすることを特徴とする請求項2又は3に記載の計算機。前記システムモニタ部は、前記認証されたデバイスドライバが前記デバイスのアクセスをした際に、前記デバイスの状態遷移が不正であった場合には、前記デバイスの故障と検知することを特徴とする請求項2乃至4のいずれか1項に記載の計算機。コンピュータのデバイスの状態遷移を管理するデバイス管理方法において、前記コンピュータは、仮想化レイヤにてゲストOSを動作させるハイパーバイザ手段と、仮想化レイヤにて前記デバイスの管理を行うシステムモニタ手段とを備え、前記システムモニタ手段により、前記デバイスの状態遷移を管理し、前記ゲストOSのデバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知することを特徴とするデバイス管理方法。コンピュータを、仮想化レイヤにてゲストOSを動作させるハイパーバイザ手段と、デバイスの状態遷移を管理し、前記ゲストOSのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段として機能させるためのプログラム。コンピュータを、仮想化レイヤにてゲストOSを動作させるハイパーバイザ手段と、デバイスの状態遷移を管理し、前記ゲストOSのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段として機能させるためのプログラムを記録したコンピュータ読み取り可能な記録媒体。しかしながら、従来技術1のソースコードの検査では、ソースコードのない市販OSについてのデバイスの管理を行うことができなかった。また、従来技術2のシステム保護装置においては、仮想化環境でシステム資源に対して仮想マシンであるドメインの接近動作を制御する接近制御モジュールを備えていた。しかしながら、この接近制御モジュールは、安全なドメインがハードウェア資源に接近することを許容する段落[0030]等を参照だけで、当該ハードウェア資源であるデバイスの状態が不正になるか否かについて判断することはできなかった。このため、安全と判断されたドメインにおけるドライバのバグ等により不正なアクセスがあった場合の安全性を保証できなかった。本発明は、このような状況に鑑みてなされたものであり、上述の課題を解消することを課題とする。本発明の計算機は、仮想化レイヤにてゲストOSを動作させるハイパーバイザ部と、デバイスの状態遷移を管理し、前記ゲストOSのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ部に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ部とを備えることを特徴とする。本発明の計算機は、前記ゲストOSの前記デバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行うかを、オートマトンの状態遷移により検査して認証するモデル検査部を備えることを特徴とする。本発明の計算機は、前記システムモニタ部は、前記モデル検査部で認証されたデバイスドライバからの直接アクセスがあった場合、負荷を抑えて前記デバイスにアクセスさせることを特徴とする。本発明の計算機は、前記システムモニタ部は、前記モデル検査部で用いた前記オートマトンにより、前記ハードウェアの仕様に従ったアクセスを行うか否かフィルタリングすることを特徴とする。本発明の計算機は、前記システムモニタ部は、前記認証されたデバイスドライバが前記デバイスのアクセスをした際に、前記デバイスの状態遷移が不正であった場合には、前記デバイスの故障と検知することを特徴とする。本発明の計算機デバイス管理方法は、コンピュータのデバイスの状態遷移を管理するデバイス管理方法において、前記コンピュータは、仮想化レイヤにてゲストOSを動作させるハイパーバイザ手段と、仮想化レイヤにて前記デバイスの管理を行うシステムモニタ手段とを備え、前記システムモニタ手段により、前記デバイスの状態遷移を管理し、前記ゲストOSのデバイスドライバが前記デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知することを特徴とする。本発明のプログラムは、コンピュータを、仮想化レイヤにてゲストOSを動作させるハイパーバイザ手段と、デバイスの状態遷移を管理し、前記ゲストOSのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段として機能させるためのプログラムであることを特徴とする。本発明の記録媒体は、コンピュータを、仮想化レイヤにてゲストOSを動作させるハイパーバイザ手段と、デバイスの状態遷移を管理し、前記ゲストOSのデバイスドライバが該デバイスのハードウェアの仕様に従ったアクセスを行わない場合、前記ハイパーバイザ手段に報知し、仮想化レイヤにて該デバイスの管理を行うシステムモニタ手段として機能させるためのプログラムを記録したコンピュータ読み取り可能な記録媒体であることを特徴とする。本発明によれば、デバイスのアクセスを仮想化レイヤで管理することで、ソースコードのない市販OSでも、デバイスの状態遷移を管理するコンピュータを提供することができる。また、本発明によれば、デバイスドライバがデバイスのハードウェアの仕様に従ったアクセスを行うかシステムモニタで管理することで、仮想マシンからのデバイスへのアクセスの安全性を保証するコンピュータを提供することができる。<実施の形態>コンピュータ10の構成図1を参照して、本発明の実施の形態に係るコンピュータ10計算機の構成について説明する。コンピュータ10は、主にMAC規格機やPC/AT互換機等のPCPersonalComputer、サーバ、汎用機、携帯電話、スマートフォン、PDAPersonalDataAssistant、モバイル端末、セットトップボックス、ネットワーク接続機能付きテレビジョン、デジタル画像音声再生用のメディアプレーヤー、ゲーム機等であり、OSOperatingSystemの機能を用いて各種プログラムを実行可能である。また、コンピュータ10は、本実施形態に係るデバイス状態遷移管理処理を実行するためのハードウェア資源である。このため、コンピュータ10は、制御部100と、主記憶部110と、補助記憶部120と、チップセット150とを備えている。制御部100は、CPUCentralProcessingUnit、中央処理装置やGPUGraphicProcessingUnitやDSPDigitalSignalProcessor等の制御手段である。制御部100は、インテル社製のインテルバーチャライゼーションテクノロジーIntelVT又はAMD社製のAMD-Vのような、仮想化支援機構を備えていてもよい。また、制御部100は、DRAMのインターフェイス等を備えて、主記憶部110に直接アクセスするような構成を用いることが可能である。主記憶部110は、DRAMDynamicRandomAccessMemory、DDR2/3/4-SDRAM、XD-RAM、SRAMStaticRAM等の主記憶手段である。補助記憶部120は、HDDHardDiskDriveやフラッシュメモリや光学ドライブ等の補助記憶手段である。チップセット150は、コンピュータ10の各部位と、他の周辺機器やネットワーク等のデバイスとを接続するためのバスアービタや各種I/Oチップ等を備える周辺機器接続インターフェイス手段である。チップセット150が接続する周辺機器としては、表示部と、音声入出力部と、入力部とを含む。表示部は、LEDLightEmittingDiode、LCDLiquidCrystalDisplay、PDPPPlasmaDisplayPanel、プロジェクタ等を用いることができる。入力部は、キーボード、トラックボール、タッチパネル、マウス等のポインティングデバイスを含む。チップセット150が接続するネットワークとしては、LANLocalAreaNetwork、WANWideAreaNetwork、携帯網や無線LAN等の各種無線ネットワークを含む。また、補助記憶部120は、ハイパーバイザ部200ハイパーバイザ手段、システムモニタ部210システムモニタ手段、OS部220ゲストOS、モデル検査部230モデル検査手段、ドライバ部240デバイスドライバ、ドライバ、及びアプリケーション部250アプリケーション手段を記憶している。これらの部位は、適宜、制御部100により主記憶部110に読み出されて実行される。また、OS部220、モデル検査部230、ドライバ部240、及びアプリケーション部250は、ハイパーバイザ部200により実行される仮想マシン300を構成している。なお、補助記憶部120は、HDD等に記憶された上述の各部位の他に、コンピュータ10のファームウェアやBIOSBasicInput/OutputSystem等を含んでいる。これらについても、適宜、制御部100により主記憶部110に読み出されて実行される。ハイパーバイザ部200は、コンピュータの仮想化技術のひとつであるバーチャルマシン仮想機械を実現するためのバーチャリゼーション仮想化レイヤLayerを構成する仮想化モニタ等の制御プログラムの部位である。すなわち、ハイパーバイザ部200は、制御部100に、ゲストOSであるOS部220を含む仮想マシン300を実行させるハイパーバイザである。ハイパーバイザ部200は、複数の仮想マシン300に、制御部100の演算資源、メモリ資源等を効率的にスケジューリングし、ハードウェア割り込み等を用いてデバイスにアクセスする。ハイパーバイザ部200は、ホストOSを必要とせず、コンピュータ10の主記憶部110に読み出されて、ハードウェア資源を用いて直接実行されるType1ネイティブ、Native、ベアメタル、BareMetal方式を用いることができる。また、ハイパーバイザ部200は、仮想マシンのエミュレーションにより仮想化されたデバイス以下、仮想デバイスという。のデバイスドライバや、チップセット150に接続された物理的なデバイス以下、物理デバイスという。用のデバイスドライバを備えることができる。ハイパーバイザ部200は、仮想マシン300内のドライバ部240に対し、仮想デバイスへのアクセスに加えて、準仮想化されたデバイスへのアクセスを行わせることができる。ここで、準仮想化とは、パラレル平行アクセス又はベアメタル等と呼ばれる直接アクセス方式を用いて、物理デバイスにマッピングされたデバイスのメモリやI/Oに対して直接アクセスを行うことをいう。この準仮想化により、デバイスのエミュレーションのオーバーヘッド処理遅延を抑えることができ、リアルタイム実時間処理が必要なネットワーク処理やレンダリング処理等に用いることができる。なお、ハイパーバイザ部200として、ホストOS上で動作するType2方式の仮想化のハイパーバイザについても用いることもできる。システムモニタ部210は、ハイパーバイザ部220と協同して、仮想化レイヤ上で動作するコマンド列のフィルタ等のプログラムの部位である。システムモニタ部210は、仮想化レイヤにおいて、デバイスドライバとは独立に、デバイスへの操作を管理する。つまり、システムモニタ部210は、OS部220であるゲストOSによるデバイスの状態の遷移を仮想化レイヤにて監視し、デバイスが利用不可能となるような不正なI/Oコマンド列等以下、不正コマンドという。を検知する。システムモニタ部210は、不正コマンドの検知が行われた場合、OS部220の当該ゲストOSの停止又は当該ゲストOSによるそのデバイスの利用を停止する。これにより、システムモニタ部210は、デバイスが利用不可能となることを防ぐことができる。このように、システムモニタ部210は、デバイスドライバ自体を検証の対象としないため、ソースコードが入手できない商用市販OSであるゲストOSにも適用することができる。また、システムモニタ部210は、OS部220のゲストOSのカーネルが、複数回単一のデバイスに対し操作を行った場合でも、不正な操作によりデバイスが利用不可能になることを防ぐことができる。また、システムモニタ部210は、モデル検査部230にて動作の認証を行ったドライバ部240からの直接アクセスについては、I/Oコマンド列等の監視を行わないか、負荷を抑えた監視を行うように構成することができる。また、システムモニタ部210は、このデバイスの状態の遷移について、上述したデバイスドライバのソースコードを基に、不正コマンドの監視ができる。また、システムモニタ部210は、チップセット150を介してデバイスの状態を直接監視することも可能である。この際、システムモニタ部210は、デバイスが正常なI/Oコマンド列により正常でない状態に遷移したことを検知して、デバイスの故障や不具合を認識することもできる。モデル検査部230は、ソースコード等のソフトウェアのプログラムを読み、実行経路をすべて調査し、規定されたプロパティ条件が満たされるかどうかソフトウェアモデル以下、モデルという。のチェック検査を行うプログラムやデータの部位である。モデル検査部は、主にゲストOSであるOS部220に用いるドライバ部240のソースコードを用いて、このモデル検査チェックを行う。具体的には、モデル検査部230は、ドライバ部240のデバイスドライバのソースコードに記載されたオートマトン形式で記載されたデバイスの状態遷移の記載を基に、ソースコードとの整合性がとれているかどうかを検証するモデル検査を行う。このデバイスの状態遷移の記載については、例えば、CSLSCSpecificationLanguageforSystemssoftware規約を用いることができる。加えて、モデル検査部230は、ハイパーバイザ部200本体が備えるデバイスドライバのモデル検査を行うこともできる。モデル検査部230は、このモデル検査により、仮想化されたソフトウェア層の正確な動作を確認することに対する検証技術を提供することができる。つまり、モデル検査部230は、ハイパーバイザ部200の仮想化レイヤのデバイスハンドラーが、ゲストOSがデバイスをエラー状態に導かないようにするための、正確なI/Oコマンドの順番制御オーダーを行う動作認証を行うことができる。このように、モデル検査部230により動作認証したソースコードは、最適化等したコンパイルを行い、OS部220のドライバ部240や、ハイパーバイザ部200のデバイスドライバとしてに組み込むことができる。そして、モデル検査部230で動作認証されたドライバ部240は、直接アクセス方式のI/Oコマンドについて、システムモニタ部210にて検証を少なくした監視を行わせることができる。また、モデル検査部230は、特に仮想化レイヤ自体の分離と、デバイスの正確な動作を保証するために、カーネル構築時やドライバ部240の更新時に最初に実行することが望ましい。また、モデル検査部230は、OS部220を用いて実行されるアプリケーションソフトウェアとして実装することができる。つまり、モデル検査部230は、OS部220の仮想マシン内の他のアプリケーションと連動させて実行することができる。なお、モデル検査部230は、ハイパーバイザ部200と同様の仮想化レイヤで実行されるように構成することもできる。この場合、モデル検査部230は、仮想化レイヤで実行されるため、直接アクセスのI/Oコマンド列を容易に検知して、このオートマトンの状態によりモデル検査を行うことができる。また、モデル検査部230は、ハイパーバイザ部200やシステムモニタ部210と同じモジュールや構成部位として備えられていてもよい。この場合でも、モデル検査部230は、ハイパーバイザ部200やシステムモニタ部210と同時並行的には動作させないで検証のみ行うことで、動作を軽くすることができる。また、モデル検査部230は、ドライバ部240のドライバのソースコードをチェックするだけでなく、オートマトンによる状態遷移であれば、任意のものを検査可能である。つまり、モデル検査部230は、アプリケーション部250の通常のウェブブラウザや計算ソフトウェア等の各種アプリケーションのソースコードに状態遷移を記載して、動作のチェックをさせることもできる。また、ソースコードが存在しない市販OSの場合には、このモデル検査部230を用いない構成も可能である。仮想マシン300は、エミュレートされた仮想のコンピュータ、すなわち仮想マシンVirtualMachine、仮想機械環境である。仮想マシン300は、1つ又は複数の仮想マシンを用いることができる。各仮想マシンは、ハイパーバイザ部200により自動的に制御部100のCPUコア等に動的に割り当られ、同時又は切り換えられて実行される。仮想マシン300は、HDD等の同一のパーティション又は複数のパーティションや複数の物理的な補助記憶装置を用いて構成することができる。また、仮想マシン300は、iSCSI等を用いて、ネットワーク上のストレージ上のイメージとして構成することもできる。さらに、仮想マシン300は、仮想HDDイメージ形式等を用いて、別のOSのパーティションにファイルとして含ませることもできる。OS部220は、ハイパーバイザ部200により仮想化されて実行される1つ又は複数のゲストOSを含む部位である。OS部220は、仮想マシン300毎に用意することができる。また、OS部220は、ハイパーバイザ部200がホストOSにより実行されるType2方式の仮想化のハイパーバイザであった場合、このホストOSも含む。OS部220は、UNIX登録商標、Linux登録商標、FreeBSD登録商標等の、ソースコードを基にカーネルやドライバ等をビルド再構成が可能な各種OSをゲストOSとして用いることができる。さらに、OS部220は、MAC登録商標OS、ウィンドウズ登録商標等の、通常はソースコードによりビルドしない市販OSを用いることもできる。ドライバ部240は、周辺機器、ネットワーク等のデバイス機器と接続の制御プログラムであるデバイスドライバ以下、ドライバという。の部位である。ドライバ部240は、OS部220に備わったAPIApplicationProgramInterfaceを用いたり、逆にOS部220に組み込まれてAPIを提供した上で、ハイパーバイザ部200がエミュレーションを行う仮想デバイスにアクセスする。さらに、ドライバ部240は、オーバーヘッドが顕著なデバイス、例えばネットワークカード、RAIDRedundantArraysofInexpensiveDisks等の補助記憶インターフェイス、ビデオボード、ストリーミング映像デバイス等に関しては、準仮想化により物理デバイスへ直接アクセスが可能である。ドライバ部240は、ソースコードがあるドライバをコンパイルした実行ファイルを用いることが可能である。この際に、上述のモデル検査部230により認証されたドライバについては、IDIdentificationを付加したI/Oコマンドを用いて直接アクセスを行い、システムモニタ部210に認識させることができる。また、ドライバ部240は、ソースコードがない市販OS等の、認証されていないドライバを用いることも可能である。アプリケーション部250は、仮想マシン300上のOS部220にて実行される各種のアプリケーションソフトウェアである。このアプリケーションソフトウェアは、OS部220のAPIを用いて、ドライバ部240により、各種の物理デバイスや仮想デバイスにアクセスできる。このアプリケーションソフトウェアとしては、ドライバ部240のソースコードのあるドライバをチェックするモデル検査部230と、これと連動するソースコードデバッガ等を含ませることができる。また、アプリケーションソフトウェアとして、ソースコードをコンパイル等するcc等のコンパイラやビルドを行うmake等の各種ソフトウェアを含ませることができる。さらに、仮想マシン300やOS部220やドライバ部240が停止した際のログ等を閲覧するソフトウェアを用いることもできる。加えて、別の仮想マシン300が停止して当該仮想マシン300に切り換えられた際に報知する警報ソフトウェア等を用いることができる。デバイス状態遷移管理処理次に、図2~図7を参照して、本発明の実施の形態に係るデバイス管理方法に係るデバイス状態遷移管理処理について説明する。ここで、本発明の実施の形態のハイパーバイザ部200は、上述したように準仮想化による直接アクセス方式を許容する。このハードウェアの規格に従った物理デバイスへのアクセスを行わないと、物理デバイスが使用不可能になることがある。この場合、当該デバイスをリセットするか、場合によっては、コンピュータ10自体をリセットする必要がある。このため、本発明の実施の形態に係るコンピュータ10は、ハイパーバイザ部200に加えて、ゲストOSのドライバが正確な方法で物理デバイスのハードウェアを管理するかどうかチェックするための機構であるシステムモニタ部210を用いる。これに加えて、本実施形態に係るデバイス状態遷移管理処理では、仮想マシン300内のドライバ部240に対して、モデル検査部230により、モデル検査による認証を行う。この上で、この認証されたドライバからの直接アクセスを、システムモニタ部210により監視する。これにより、ゲストOSのカーネルによるデバイスのアクセスについて、オーバーヘッドが少ない直接アクセスを用いた場合でも、デバイスが使用不可能になることを防ぐことができる。以下で、図2のフローチャートを用いて、デバイス状態遷移管理処理の各処理について説明する。ステップS101まず、制御部100は、モデル検査部230を用いてドライバ部240のドライバ等のソースコードをモデル検査するドライバチェック処理を行う。このドライバチェック処理では、デバイスへの操作が仕様を満たすかどうかを検査するために、モデル検査を用いる。具体的には、制御部100は、デバイスの状態遷移について上述のCSLS規約によりオートマトンとして記載されたソースコードをコンパイルし、ステップ実行等を行う。その上で、制御部100は、デバイスの状態が当該オートマトンに従って正しく遷移するか否かについて判定する。この際、制御部100は、モデル検査部230により、ゲストOSがシステムモニタ部210により停止させられないように、実際には直接アクセス方式で物理デバイスにアクセスしないように構成することが好適である。また、逆に、制御部100は、直接アクセス方式により状態が遷移した物理デバイスの状態や仮想デバイスの状態を、遷移の情報として取得して検証することが可能である。制御部100は、所定ステップの間、デバイスが正しく遷移したと考えられる場合、そのドライバのオブジェクトや実行コードに所定のIDを付加する認証を行う。これにより、認証されたドライバからの直接アクセスの際には、システムモニタ部210が検知してオーバーヘッドを抑える処理を行うことができる。ステップS102次に、制御部100は、システムモニタ部210を用いて、仮想マシン300からの物理デバイスへの直接アクセスを管理するシステムモニタ処理を行う。この処理では、仮想化レイヤにおいて、ハイパーバイザ部200が備えるデバイスドライバとは独立に、デバイスへのアクセスを管理する。具体的には、制御部100は、ドライバ部240からの準仮想化による直接アクセスを検知する。この上で、直接アクセスの際、制御部100は、不正コマンド等により物理デバイスが不正な状態遷移となる不正アクセスがされているかを検知する。そして、制御部100は、不正アクセスが検知された場合に、仮想マシン300の停止等を行う。このような不正アクセスにより、コンピュータ10自体が動作不良やハングアップする可能性がある。よって、システムモニタ部210を用いてチェックすることで信頼性を高めることができる。また、制御部100は、物理デバイス自体の状態遷移について、システムモニタ部210を用いて検査する。この上で、制御部100は、上述の認証されたドライバのアクセスにより不正な遷移となった場合、物理デバイスの故障を報知する。以上により、デバイス状態遷移管理処理を終了する。ドライバチェック処理の詳細次に、図3~図5を参照して、本発明の実施の形態に係るドライバチェック処理の詳細について説明する。これらの処理は、制御部100は、モデル検査部230を用いて実行する。以下、図3のフローチャートを基に、各処理の詳細について説明する。ステップS201まず、制御部100は、初期化処理を行う。この処理では、まず、制御部100は、モデル検査を行うドライバ等のソースコードが存在するか判断する。次に、制御部100は、当該ソースコードにデバイスの状態遷移に関するオートマトンの記載があるか否かを判断する。ここで、ソースコードの全てにオートマトンの記載を行う必要はない。よって、制御部100は、物理デバイスにアクセスする部分のソースファイル等、一部について記載があれば、記載ありと判断する。ソースコードにオートマトンの記載があった場合、制御部100は、このソースコードを、パーサ等を用いて解釈する。この上で、制御部100は、リスト等のデータ構造を用いて実際のオートマトンのデータを主記憶部110に作成する。なお、制御部100は、ソースコードがなかったり、ソースコードにオートマトンの記載がなかったりした場合には、エラーとして処理を終了する。ステップS202次に、制御部100は、コンパイル処理を行う。具体的には、制御部100は、ソースコードの言語に係るコンパイラを、パイプ等を用いて起動する。この上で、制御部100は、上述のドライバのソースコードを読み込ませ、コンパイルさせる。このコンパイルにおいては、最適化を行わないデバッグモードのシンボルを付加したコンパイルを行うことが好適である。ステップS203次に、制御部100は、モデル遷移チェック処理を行う。このモデル遷移チェック処理においては、制御部100は、モデルチェック部は、コンパイルされたドライバについて、ステップ実行等を行う。このステップ実行は、統合開発環境のソースレベルデバッガ等と連動させることができる。この上で、制御部100は、ステップ毎にオートマトンの状態を検査する。このモデル遷移チェック処理の詳細な実行例については後述する。ステップS204次に、制御部100は、オートマトンが正しい遷移を示しているか否か判定する。Yes、すなわちオートマトンの状態が正しい遷移を示している場合、制御部100は、処理をステップS206に進める。No、すなわちオートマトンの状態が不正な遷移を示している場合は、制御部100は、処理をステップS205に進める。ステップS205オートマトンが不正な遷移を示していた場合、制御部100は、エラー処理を行う。この不正な遷移をした場合、当該デバイスはエラー状態等となり使用不可能となる、すなわちプログラムの不正な箇所バグがあると考えられる。よって、デバイスドライバのソースコード自体を変更する必要がある。このため、制御部100は、エラーを起こした箇所をソースレベルデバッガ等に報知する。この際、制御部100は、当該ソースレベルデバッガ等により、オートマトンの遷移図等と、停止箇所を示す。これにより、ユーザにソースコードの不正箇所を知る手がかりを与えることができる。その後、制御部100は、ドライバチェック処理を終了する。ステップS206オートマトンが正しい遷移を示していた場合、制御部100は、ステップ実行が終了したか否かについて判定する。ここでは、制御部100は、所定回数のステップ実行したか、ソースコードに様々なパラメータを与えてほぼ全ての状態遷移の実行を終えた場合、ステップ実行の終了と判断する。また、制御部100は、オートマトンの状態から全ての状態遷移を検査したと判断できた場合等にも、ステップ実行の終了と判断することができる。Yes、すなわちステップ実行が終了した場合、制御部100は、処理をステップS207に進める。No、すなわちまだステップ実行を行う必要がある場合、制御部100は、処理をステップS203に戻してモデル検査を続ける。ステップS207ステップ実行が終了した場合、制御部100は、デバイスドライバ認定処理を行う。具体的には、制御部100は、直接アクセスを行っても物理デバイスを停止等させる可能性が少ないドライバであるとして、認証を行う。この処理においては、制御部100は、最適化を行った上でデバイスドライバをコンパイルする。この際、制御部100は、システムモニタ部210の公開鍵や秘密鍵等を基に、ハッシュ関数等を用いて、不正な認証ができないようなIDを作成して、このIDをソースコードやオブジェクトやバイナリ実行コード等に埋め込む。また、制御部100は、モデル検査部230がソースコードを解析して作成したオートマトンのデータについても、IDと共に埋め込むことができる。これにより、認証されたドライバは、物理デバイスへの直接アクセスの際に、このIDを用いることができる。これにより、システムモニタ部210の管理の負荷を軽減できる。以上により、ドライバチェック処理を終了する。モデル遷移チェック処理の実施例ここで、モデル遷移チェック処理の具体例について、図4A~図5を参照して詳細に説明する。上述したように、このモデル遷移チェック処理では、OS部220のゲストOSに、物理デバイスの規定に従った正確な振る舞いを強いるための機構を提供する。この際、本発明の実施の形態においては、制御部100が、モデル検査部230を用いて、ドライバ部240が正確な方法でハードウェアを管理するかどうか検査する。以下では、仮想マシン300のドライバ部240について、RS-232規格等のシリアルインターフェイスのドライバを用いてモデル検査を行った実施例について説明する。この実施例では、仮想マシン300のドライバ部240のシリアルデバイスハンドラーのモデル検査を行って、シリアルデバイスがエラー状態にならないように正確な命令動作をすることを確認した。これにより、ドライバ部240が、ハイパーバイザ部200下の仮想マシン300によって正確に動作することを確認することができる。文字の送信まず、図4Aを参照して、ドライバ部240のシリアルデバイスのドライバによる文字の送信について説明する。オートマトン245は、このドライバ部240の状態遷移を示す。シリアルライン上の文字を送信するために、制御部100は、ドライバ部240の動作として、以下の工程に従う必要がある。まず、図4Aのシリアルドライバの最初の工程1として、制御部100は、send送信バッファが空かどうかチェックする。次に、制御部100は、送信バッファが空か否かチェックして、空の場合、次の工程2に進める。そうでなければ、制御部100は、送信バッファが空になるまで待つ。その後、制御部100は、送信バッファに文字を書き込む。ここで、バッファがフルのとき、ドライバが文字を書き込むと、オートマトン245のデバイスの状態はエラー状態になる。制御部100は、このエラー状態となったことを検知して、モデル検査部230に報知することができる。上述のシリアルデバイスの状態遷移は、モデル化することができる。以下に、バッファが空であるか否かをチェックするser_is_ready_to_send関数の例を示す。このser_is_ready_to_send関数は、バッファの状態を検知し、送信が準備可能かどうかを返す。ensuresintserisreadytosendintthrehwuartlsrthreifsertxready1elsesertxready0returnthreまた、以下は、バッファが空で送信可能な場合、バッファに文字を書き出すser_send関数の例を示す。ser_send関数は、バッファが空及び送信要求である場合、バッファに文字を書き、そうでなければ、エラーをモデル検査部230に返す。なお、制御部100は、実際にコンパイル後のドライバがドライバ部240やハイパーバイザ部200に組み込まれた際、このエラーの場合には、ハイパーバイザ部200が当該仮想マシン300を停止するように通知することもできる。ensures0needtokillvm1voidsersendifneedtokillvm1sertxready0hwuarttxこの例のように、デバイスの状態遷移に関するオートマトンの記載は、C言語の場合には、上述したCSLS規約により、//のようなコメント行を用いて記載することができる。通常のコンパイラでは、この記載はコメント行として無視されるため、汎用性を高めることができる。文字の送信次に、図4Bを参照して、ドライバ部240のシリアルデバイスのドライバによる文字の受信について説明する。オートマトン246は、このドライバ部240の状態遷移を示す。文字の受信は、上述の文字の送信と同様の方法でモデル化することができる。ドライバ部240のシリアルドライバは、シリアルライン上の文字を受信するために下記の動作を行う。まず図4Bの最初の工程1において、制御部100は、受信バッファにおいてデータ受信の準備ができているかどうかチェックする。準備ができている場合、次の工程2に移る。そうでなければ、制御部100は、データの準備ができるまで待つ。この上で、制御部100は、受信バッファから文字を読み出す。一方、データがない場合に、受信バッファから文字を読み出すと、制御部100はエラーをモデル検査部230に報知する。このように、制御部100は、モデル検査部230を用いてプログラムの誤動作を検知できる。図5は、このモデル検査の結果を示す画面例である。この例では、ProgramisSAFE即ち、安全なドライバであると検査されている。このように、仮想化レイヤにおいて、誤操作がいつ行なわれるか実際にモデル検査により確認することができる。したがって、不正アクセスをしない正確な動作を行うドライバ部240を得ることが可能になる。これにより、信頼性が高く高パフォーマンスの仮想マシンを提供することができる。なお、制御部100は、エラー状態の報知について、検証した後のドライバ部240により、システムモニタ部210やハイパーバイザ部200に対して報知することもできる。これにより、万一のエラーの際には、ハイパーバイザ部200が物理デバイスにアクセスしないように構成することができ、検証されたドライバ部240による不正アクセスを防ぐことが可能になる。このため、本発明の実施の形態に係るコンピュータ10を、非常に高度の信頼性が求められる生命維持、生産プラント、乗り物の制御といった分野に用いることができる。システムモニタ処理の詳細次に、図6及び図7を参照して、本発明の実施の形態に係るシステムモニタ処理の詳細について説明する。これらの処理は、上述したように、制御部100が、システムモニタ部210を用いて、仮想化レイヤ上で実行する。以下、図6のフローチャートを用いて、各処理の詳細について説明する。ステップS301まず、制御部100は、ドライバ認証検知処理を行う。この処理では、仮想マシン300のドライバ部240が、上述のドライバチェック処理により認証されたドライバであるか検知する。具体的には、制御部100は、ドライバ部240のドライバに認証によるID等があるか否か、秘密鍵等を用いて検証する。ここで、ドライバ部240のドライバが認証されたものであった場合、制御部100は、このIDを用いた物理デバイスへのアクセスについては、後述するフィルタ処理にて不正アクセスであるかを検知しないか負荷を抑えた軽い検知のみ行う。ステップS302次に、制御部100は、I/Oコマンド読み込み処理を行う。図7を参照して説明すると、制御部100は、ハイパーバイザ部200が実行する仮想マシン300のゲストOSのドライバ部240から、デバイスへアクセスするI/Oコマンド指示信号があったかどうかを検知する。つまり、制御部100は、仮想化レイヤにおいて、デバイスドライバとは独立して、デバイスへの操作を管理する。制御部100は、デバイスへのアクセスするI/Oコマンドを検知した場合、ハイパーバイザ部200に通知する。このドライバ部240からのデバイスへアクセスするI/Oコマンドは、仮想レイヤへのハイパーバイザコール形式で行うことが好適である。この際、制御部100は、チップセット150に接続された物理デバイスへの指示を行うI/Oコマンドに加えて、仮想デバイスのコマンドも検知する。また、制御部100は、ドライバのI/Oコマンド毎にIDを検知することができる。ステップS303次に、制御部100は、デバイスへアクセスするI/Oコマンドが、直接アクセスのI/Oコマンドであったか否かについて判定する。Yesの場合、制御部100は、処理をステップS304に進める。Noの場合、制御部100は、処理をステップS307に進める。ステップS304次に、制御部100は、フィルタ処理を行う。具体的には、制御部100は、直接アクセスのI/Oコマンド列が、デバイスの状態遷移を不正にする、不正コマンドである場合、これを不正アクセスとして検知する。このデバイスの状態遷移については、ハイパーバイザ部200の物理デバイス用のドライバに対応するオートマトンを用意しておいて、このオートマトンの状態遷移がエラーになるか否かについて検知する。このオートマトンとしては、上述のモデル検査部230が作成したドライバ部240のオートマトンを用いることができる。この際、異なるゲストOSを備えた仮想マシン300であっても、同一の物理デバイス/仮想デバイスについては、同一のオートマトンを用いることができる。このように、オートマトンを用いて不正コマンドを検知するため、ハイパーバイザ部200が仮想マシン300を切り換えた際、デバイスの動作タイミング等が原因で各仮想マシン300からの物理デバイスからのアクセスが不正コマンドになった場合でも対応できる。また、仮想マシン300から、複数回、単一のデバイスに対しI/Oコマンドによるアクセスを行った場合でも対応できる。このため、不正コマンドによりデバイスが利用不可能になることを防ぐことが可能になる。ここで、直接アクセスのI/Oコマンド列が、上述の認証されたドライバ部240のドライバからのI/Oコマンド列であった場合、制御部100は、例えば、オートマトンの状態遷移の変化を行わないような処理を行うことが可能である。また、例えば、検知のフィルタ自体をスルー通過させることもできる。これにより、仮想化のオーバーヘッドを減らし、負荷を抑えて、安全に物理デバイスにアクセスさせることができる。この場合でも、ドライバ部240のドライバ自体がオートマトンを持って状態遷移がエラーになった場合には、システムモニタ部210に報知することができるため、安全に物理デバイスにアクセス可能である。ステップS305次に、制御部100は、不正アクセスであるか否かについて判定する。ここでは、上述なようにオートマトンの状態遷移により、物理デバイスのアクセスに係る不正コマンドを検知した場合、不正アクセスである、すなわちYesと判断する。それ以外の場合はNoと判断する。Yesの場合、制御部100は、処理をステップS306に進める。Noの場合、制御部100は、処理をステップS307に進める。ステップS306制御部100は、不正アクセスであった場合、ゲストOS停止処理を行う。具体的には、制御部100は、ハイパーバイザ部200へ、不正アクセスをした仮想マシン300を停止するように指示する。この際、仮想マシン300を直接停止させるのではなく、仮想マシン300のドライバ部240の当該デバイスドライバにエラーの通知を返信することが可能である。この場合でも、当該デバイスドライバが停止しない場合、制御部100は、OS部220にエラーを報知することができる。これにより、OS部220のエラー対応機能によりドライバ部240の当該デバイスドライバを停止させることもできる。しかしながら、この場合でもOS部220が反応しない場合、制御部100は、仮想マシン300自体を停止することができる。このような構成により、コンピュータ10の動作の停止時間や再起動の時間等を少なくすることができる。システムモニタ部210は、仮想マシン300やOS部220やドライバ部240を停止させた場合には、ハイパーバイザ部200に通知し、更に表示部や音声入出力部やシリアルデバイス等に警告を報知することができる。そして、制御部100は、エラーの内容を表示部等やネットワークを介した監視機器等に報知し、ログを作成する。ステップS307次に、制御部100は、物理デバイス遷移検査処理を行う。この処理においては、制御部100は、当該物理デバイスの状態を、チップセット150を介して取得する。制御部100は、この取得について、ハイパーバイザ部200の情報を取得し、主に直接アクセスのI/Oコマンド列により物理デバイスを動作させた後に行う。この上で、制御部100は、この物理デバイスの状態が、オートマトンにより想定された状態遷移であるか否かを判断する。制御部100は、物理デバイスが想定された遷移の状態ステートでなかった場合には、不正な遷移をしていると検知する。特に、制御部100は、認証されたドライバからのアクセスがあったにも関わらず、物理デバイスがエラー状態になっていることを検知した場合、起こり得ないことが起こったとして、デバイスが故障したと検知する。ステップS308制御部100は、物理デバイスが不正な状態遷移をしているか否か判定する。ここでは、制御部100は、上述の不正な状態遷移であった場合には、Yesと判定する。Yes、すなわち不正な状態遷移があった場合、制御部100は処理をステップS309に進める。No、すなわち物理デバイスの状態遷移が想定していた状態遷移であった場合、制御部100は処理をステップS302に戻して、管理を続ける。ステップS309制御部100は、ここでは、故障報知処理を行う。この処理においては、制御部100は、ハイパーバイザ部200、表示部等やネットワークを介した監視機器等に、不正な遷移をした物理デバイスの故障を報知する。この際に、表示部や音声入出力部やシリアルデバイス等に警告を報知することもできる。なお、不正アクセスでドライバや仮想マシン300を停止した場合にも、制御部100は、報知を行って、システムモニタ処理を停止するように構成することもできる。以上により、システムモニタ処理を終了する。以上のように構成することで、以下のような効果を得ることができる。本発明の実施の形態に係るコンピュータ10は、デバイスへのアクセスを仮想化レイヤのシステムモニタ部210でフィルタして、デバイスの状態遷移を管理する。すなわち、本発明の実施の形態に係るコンピュータ10は、仮想マシン300上でゲストOSであるOS部220を実行する。この上で、ゲストOSによるデバイスのアクセスを、仮想化レイヤのシステムモニタ部210が監視し、デバイスが利用不可能となる不正な操作を検知したら、ゲストOSの停止又はゲストOSによるそのデバイスの利用を停止する。具体的には、本実施形態に係るシステムモニタ部210は、準仮想化による直接アクセスの際、物理デバイスに不正なI/Oコマンド列等でアクセスすると、仮想マシン300又はドライバ部240を停止させることができる。これにより、仮想マシン300内のソフトウェアからのデバイスへのアクセスにより、当該デバイスが利用不可能になることを防ぐことができる。また、システムモニタ部210は、デバイスドライバからのアクセスのI/Oコマンド自体を管理するため、ソースコードが入手できない商用市販OSにも適用できる。また、システムモニタ部210は、ゲストOSから複数回、単一のデバイスに対しアクセスがされた場合でも、そのデバイスの状態遷移を検知する。これにより、不正なI/Oコマンド列によりデバイスが利用不可能になることを防ぐことができる。これにより、安定稼働が必要なコンピュータ10に適用することができる。すなわち、デバイスが利用不可能となることが被害や損害につながるような機器での利用、例えば、医療機器やインフラ系等のコンピュータに利用できる。また、本発明の実施の形態に係るシステムモニタ部210は、仮想化レイヤに対する直接アクセスに対してだけ、ハードウェアのデバイスの仕様に従ったアクセスであるか管理する。この際、物理デバイスの状態遷移が想定から外れた場合に、ゲストOS又はドライバを稼働停止させられる。これにより、仮想マシン300からの物理デバイスへのアクセスにより当該物理デバイスがエラー状態となることを防ぐことができる。よって、コンピュータ10を安定して稼働することができる。また、従来技術1は、デバイスドライバそのものを検証することによりデバイスへの操作が正しいことを保証するものであった。このため、従来技術1は、デバイスの共有が起こる仮想化環境に直接適用することができなかった。これに対して、本発明の実施の形態に係るモデル検査部230は、仮想化レイヤに対するアクセスのI/Oコマンド列に関するモデル検査を行うことで、仮想化された環境でも適用することができる。また、従来技術1のソースコードの検査では、ホーア論理を用いてドライバの動作の正しさを証明するため非常に手間がかかるという問題があった。つまり、従来技術1では、ユーザが各種パラメータ等を変えてデバイスドライバを検査する必要があった。これに対して、本発明の実施の形態に係るモデル検査部230は、オートマトンの状態遷移を用いてドライバのモデル検査を行うため、自動的にデバイスドライバの検査を行うことができる。これにより、高速に手間が少なくドライバの検査ができる。また、本発明の実施の形態に係るモデル検査部230は、モデル検査を行ったドライバを認証する。これにより、システムモニタ部210は、認証されたドライバからの物理デバイスへのアクセスに際して、負荷を抑えたフィルタリングを行うことができる。よって、仮想化によるオーバーヘッドを少なくしたまま、コンピュータ10を安全に稼働させられる。このため、ネットワークのコントローラ等のパフォーマンスが必要なハードウェア資源のアクセスを高速化できる。つまり、例えば、ネットワークカードに適用した場合、iSCSI等により接続されたネットワークストレージのアクセススピードを高速化できる。本発明の実施の形態に係るシステムモニタ部210は認証されたドライバが物理デバイスへアクセスをした際に、当該物理デバイスの状態遷移が不正であった場合には、当該物理デバイスの故障と検知することができる。これにより、不正アクセスの検知と、物理デバイスの故障の検知とを同一環境で行うことができ、コンピュータ10に問題が起こった場合に、迅速に解決できる。よって、コンピュータ10の運用コストを低下させることができる。なお、上記実施の形態の構成及び動作は例であって、本発明の趣旨を逸脱しない範囲で適宜変更して実行することができることは言うまでもない。