推論規則生成方法およびプログラム
【課題】ユーザが定義するセキュリティポリシから、一階述語論理における推論規則を導出する一般的な方法を明示する推論規則生成方法およびプログラムを提供する。
【解決手段】安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定し、安全性ポリシを満たすプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する。また、安全性ポリシを満たさないプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する。そして、１つの状態遷移規則に対して、１つの推論規則を生成する。
【解決手段】安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定し、安全性ポリシを満たすプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する。また、安全性ポリシを満たさないプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する。そして、１つの状態遷移規則に対して、１つの推論規則を生成する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、状態遷移図を用いて、ユーザが定義するセキュリティポリシから、一階述語論理における推論規則を導出する推論規則生成方法およびプログラムに関する。
【背景技術】
【０００２】
従来より、プログラムの安全な実行を担保するために様々な技術が提案されている。そのうち、図４にその概念図を示すＰＣＣ（Ｐｒｏｏｆ Ｃａｒｒｙｉｎｇ Ｃｏｄｅ）では、プログラム開発者が証明生成器を用いて、プログラムから安全性ポリシに基づく安全性証明を生成し、プログラムとともに、プログラム利用者に送付を行う。プログラム利用者は、証明生成器を用いて、安全性ポリシおよびプログラムに基づいて、プログラムの安全性証明を検証する。そして、安全性証明が正しく検証できたときに、プログラム利用者が安全にそのプログラムを実行できるというものである（例えば、非特許文献１参照。）。
【０００３】
また、類似の技術としては、プログラムの安全な実行を暗号学的な手段を用いて実現するものもある。例えば、デジタル署名を用いて、プログラム開発者を認証する方法である。しかしながら、この方法は、悪意のあるプログラム開発者が作成したプログラムの実行を防止することができるものの、正当なプログラム開発者が開発した人為的なミスによる脆弱性を含むプログラムの実行を防止することができない。
【０００４】
また、Ｊａｖａ（登録商標）仮想機械においても、クラスファイルを実行する際に、当該クラスファイルの検証を行うが、この検証処理は、実行ごとに行う必要があり、効率的ではない。さらに、この方式では、任意の安全性ポリシに基づく柔軟なクラスファイル検証を行うことができない。
【非特許文献１】Ｎｅｃｕｌａ、“Ｐｒｏｏｆ−Ｃａｒｒｙｉｎｇ Ｃｏｄｅ、ｂｙ Ｇｅｏｒｇｅ Ｎｅｃｕｌａ、”Ｐｒｏｃ．ｏｆ Ｓｙｍｐｏｓｉｕｍ ｏｎ Ｐｒｉｎｃｉｐｌｅｓ ｏｆ Ｐｒｏｇｒａｍｍｉｎｇ Ｌａｎｇｕａｇｅｓ（ＰＯＰＬ‘９７）、１９９７．
【発明の開示】
【発明が解決しようとする課題】
【０００５】
非特許文献１においては、安全性ポリシは一階述語論理における推論規則で記述される。プログラムの初期状態（ＰＲＥ）から、これらの推論規則、および各機械語命令から生成されるＶｅｒｉｆｉｃａｔｉｏｎ Ｃｏｎｄｉｔｉｏｎ（ＶＣ）を用いて、正しいプログラムの最終状態（ＰＯＳＴ）が導出されるとき、このプログラムは安全であると判断され、命題の列ＰＲＥ，Ｐ１，Ｐ２，・・・，Ｐｎ，ＰＯＳＴがこのプログラムに対する安全性証明となる。ただし、Ｐ１，Ｐ２，・・・，Ｐ１ｎは推論の過程で導出される命題である。すなわち、非特許文献１に記載の技術では、安全性ポリシから一階述語論理における推論規則を導出することが必要であるが、非特許文献１には、その一般的な手法が定義されていないという問題がある。
【０００６】
そこで、本発明は、上述の課題に鑑みてなされたものであり、ユーザが定義するセキュリティポリシから、一階述語論理における推論規則を導出する一般的な方法を明示する推論規則生成方法およびプログラムを提供することを目的とする。
【課題を解決するための手段】
【０００７】
本発明は、上記の課題を解決するために、以下の事項を提案している。
（１）本発明は、安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定する第１のステップと、安全性ポリシを満たすプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する第２のステップと、安全性ポリシを満たさないプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する第３のステップと、１つの状態遷移規則に対して、１つの推論規則を生成する第４のステップと、を備えた推論規則生成方法を提案している。
【０００８】
この発明によれば、安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定し、安全性ポリシを満たすプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する。また、安全性ポリシを満たさないプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する。そして、１つの状態遷移規則に対して、１つの推論規則を生成する。したがって、安全性ポリシから状態遷移図を構成し、この状態遷移図に基づいて、一階述語論理における推論規則を導出する。
【０００９】
（２）本発明は、コンピュータに、安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定する第１のステップと、安全性ポリシを満たすプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する第２のステップと、安全性ポリシを満たさないプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する第３のステップと、１つの状態遷移規則に対して、１つの推論規則を生成する第４のステップと、を実行させるためのプログラムを提案している。
【００１０】
この発明によれば、安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定し、安全性ポリシを満たすプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する。また、安全性ポリシを満たさないプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する。そして、１つの状態遷移規則に対して、１つの推論規則を生成する。したがって、安全性ポリシから状態遷移図を構成し、この状態遷移図に基づいて、一階述語論理における推論規則を導出する。
【発明の効果】
【００１１】
本発明によれば、安全性ポリシから状態遷移図を構成し、この状態遷移図に基づいて、一階述語論理における推論規則を導出することができるという効果がある。
【発明を実施するための最良の形態】
【００１２】
以下、本発明の実施形態について、図面を用いて、詳細に説明する。
なお、本実施形態における構成要素は適宜、既存の構成要素等との置き換えが可能であり、また、他の既存の構成要素との組合せを含む様々なバリエーションが可能である。したがって、本実施形態の記載をもって、特許請求の範囲に記載された発明の内容を限定するものではない。
【００１３】
図１から図３を用いて、本実施形態について説明する。
なお、本発明においては、安全性ポリシを満たさないプログラム、もしくは、安全性ポリシを満たすプログラムの動作を、状態遷移図で規定する。そして、ここで得られた状態遷移図において、初期状態を推論規則における初期条件に対応させ、受理状態以外の状態を推論規則における最終状態に対応させる。また、１つの状態遷移規則に対し、１つの推論規則を生成する。以下、図１を用いて、詳細な手順を説明する。
【００１４】
まず、安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定する（ステップＳ１０１）。次に、安全性ポリシを満たすプログラムか否かを判断し（ステップＳ１０２）、安全性ポリシを満たすプログラムについては（ステップＳ１０２の「Ｙｅｓ」）、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する（ステップＳ１０３）。
【００１５】
一方、安全性ポリシを満たさないプログラムについては（ステップＳ１０２の「Ｎｏ」）、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する（ステップＳ１０４）。
【００１６】
そして、状態遷移規則σ（ｑ１、ｘ）＝ｑ２（状態ｑ１に入力ｘが入ったら、ｑ２になるという状態遷移を意味する）に対して、推論規則（（ｑ１，ｉ）、∨Ｃｉ∈ｘ）／（ｑ２、ｉ＋１）を生成する。なお、特に、状態ｑ２が受理状態ｑｆである場合は、状態遷移規則σ（ｑ１、ｘ）＝ｑｆから生成される推論規則は、（（ｑ１，ｉ）、∨Ｃｉ∈ｘ）／ｑｆとする。
【００１７】
したがって、本実施形態によれば、安全性ポリシから状態遷移図を構成し、この状態遷移図に基づいて、一階述語論理における推論規則を導出することができる。
【００１８】
＜実施例＞
いま、実施例として、安全性ポリシを「メモリアドレス５０番地のデータは読み出し禁止」とした場合の推論規則の導出手法を考える。まず、はじめに、安全性をみたさないプログラム、すなわち、メモリアドレス５０番地のデータの読み出しを行なうプログラムの動作を状態遷移図で規定する。ここで生成される状態遷移図を図２に示す。
【００１９】
図２において、ｑ０、ｑ１、ｑｆは状態を示し、各状態間を結ぶ線は、状態遷移規則を示している。例えば、状態ｑ０から状態ｑ１に向かう線（状態遷移規則）は、状態がＩ１０であれば、ｑ０からｑ１に遷移することを示している。
【００２０】
図２の状態遷移図から導出される一階述語論理の推論規則は、図３のようになる。
図３において、ＰＲＥ＝（ｑ０、０）は初期条件を示している。また、本実施例は、「メモリアドレス５０番地のデータは読み出し禁止」という安全性ポリシに対して、メモリアドレス５０番地のデータの読み出しを行なうプログラムの動作を状態遷移図で規定したものであるから、最終条件は、ＰＯＳＴ＝¬ｑｆとなる。
【００２１】
また、図２中、（１）の状態遷移規則は、図３の推論規則（（ｑ０，ｉ）、∨Ｃｉ∈Ｉ００）／（ｑ０、ｉ＋１）に対応し、図２中、（２）の状態遷移規則は、図３の推論規則（（ｑ０，ｉ）、∨Ｃｉ∈Ｉ０１）／（ｑ１、ｉ＋１）に対応し、図２中、（３）の状態遷移規則は、図３の推論規則（（ｑ１，ｉ）、∨Ｃｉ∈Ｉ１０）／（ｑ０、ｉ＋１）に対応し、図２中、（４）の状態遷移規則は、図３の推論規則（（ｑ１，ｉ）、∨Ｃｉ∈Ｉ１１）／（ｑ１、ｉ＋１）に対応し、図２中、（５）の状態遷移規則は、図３の推論規則（（ｑ１，ｉ）、∨Ｃｉ∈Ｉ１ｆ）／ｑｆに対応する。
【００２２】
なお、推論規則生成方法の処理をコンピュータ読み取り可能な記録媒体に記録し、この記録媒体に記録されたプログラムを装置に読み込ませ、実行することによって本発明の推論規則生成方法を実現することができる。ここでいうコンピュータシステムとは、ＯＳや周辺装置等のハードウェアを含む。
【００２３】
また、「コンピュータシステム」は、ＷＷＷ（Ｗｏｒｌｄ Ｗｉｄｅ Ｗｅｂ）システムを利用している場合であれば、ホームページ提供環境（あるいは表示環境）も含むものとする。また、上記プログラムは、このプログラムを記憶装置等に格納したコンピュータシステムから、伝送媒体を介して、あるいは、伝送媒体中の伝送波により他のコンピュータシステムに伝送されても良い。ここで、プログラムを伝送する「伝送媒体」は、インターネット等のネットワーク（通信網）や電話回線等の通信回線（通信線）のように情報を伝送する機能を有する媒体のことをいう。
【００２４】
また、上記プログラムは、前述した機能の一部を実現するためのものであっても良い。さらに、前述した機能をコンピュータシステムにすでに記録されているプログラムとの組合せで実現できるもの、いわゆる差分ファイル（差分プログラム）であっても良い。
【００２５】
以上、この発明の実施形態につき、図面を参照して詳述してきたが、具体的な構成はこの実施形態に限られるものではなく、この発明の要旨を逸脱しない範囲の設計等も含まれる。
【図面の簡単な説明】
【００２６】
【図１】本実施形態に係る処理フローである。
【図２】状態遷移図の一例を示した図である。
【図３】状態遷移図から生成される推論規則の一例を示した図である。
【図４】ＰＣＣの概念図である。
【技術分野】
【０００１】
本発明は、状態遷移図を用いて、ユーザが定義するセキュリティポリシから、一階述語論理における推論規則を導出する推論規則生成方法およびプログラムに関する。
【背景技術】
【０００２】
従来より、プログラムの安全な実行を担保するために様々な技術が提案されている。そのうち、図４にその概念図を示すＰＣＣ（Ｐｒｏｏｆ Ｃａｒｒｙｉｎｇ Ｃｏｄｅ）では、プログラム開発者が証明生成器を用いて、プログラムから安全性ポリシに基づく安全性証明を生成し、プログラムとともに、プログラム利用者に送付を行う。プログラム利用者は、証明生成器を用いて、安全性ポリシおよびプログラムに基づいて、プログラムの安全性証明を検証する。そして、安全性証明が正しく検証できたときに、プログラム利用者が安全にそのプログラムを実行できるというものである（例えば、非特許文献１参照。）。
【０００３】
また、類似の技術としては、プログラムの安全な実行を暗号学的な手段を用いて実現するものもある。例えば、デジタル署名を用いて、プログラム開発者を認証する方法である。しかしながら、この方法は、悪意のあるプログラム開発者が作成したプログラムの実行を防止することができるものの、正当なプログラム開発者が開発した人為的なミスによる脆弱性を含むプログラムの実行を防止することができない。
【０００４】
また、Ｊａｖａ（登録商標）仮想機械においても、クラスファイルを実行する際に、当該クラスファイルの検証を行うが、この検証処理は、実行ごとに行う必要があり、効率的ではない。さらに、この方式では、任意の安全性ポリシに基づく柔軟なクラスファイル検証を行うことができない。
【非特許文献１】Ｎｅｃｕｌａ、“Ｐｒｏｏｆ−Ｃａｒｒｙｉｎｇ Ｃｏｄｅ、ｂｙ Ｇｅｏｒｇｅ Ｎｅｃｕｌａ、”Ｐｒｏｃ．ｏｆ Ｓｙｍｐｏｓｉｕｍ ｏｎ Ｐｒｉｎｃｉｐｌｅｓ ｏｆ Ｐｒｏｇｒａｍｍｉｎｇ Ｌａｎｇｕａｇｅｓ（ＰＯＰＬ‘９７）、１９９７．
【発明の開示】
【発明が解決しようとする課題】
【０００５】
非特許文献１においては、安全性ポリシは一階述語論理における推論規則で記述される。プログラムの初期状態（ＰＲＥ）から、これらの推論規則、および各機械語命令から生成されるＶｅｒｉｆｉｃａｔｉｏｎ Ｃｏｎｄｉｔｉｏｎ（ＶＣ）を用いて、正しいプログラムの最終状態（ＰＯＳＴ）が導出されるとき、このプログラムは安全であると判断され、命題の列ＰＲＥ，Ｐ１，Ｐ２，・・・，Ｐｎ，ＰＯＳＴがこのプログラムに対する安全性証明となる。ただし、Ｐ１，Ｐ２，・・・，Ｐ１ｎは推論の過程で導出される命題である。すなわち、非特許文献１に記載の技術では、安全性ポリシから一階述語論理における推論規則を導出することが必要であるが、非特許文献１には、その一般的な手法が定義されていないという問題がある。
【０００６】
そこで、本発明は、上述の課題に鑑みてなされたものであり、ユーザが定義するセキュリティポリシから、一階述語論理における推論規則を導出する一般的な方法を明示する推論規則生成方法およびプログラムを提供することを目的とする。
【課題を解決するための手段】
【０００７】
本発明は、上記の課題を解決するために、以下の事項を提案している。
（１）本発明は、安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定する第１のステップと、安全性ポリシを満たすプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する第２のステップと、安全性ポリシを満たさないプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する第３のステップと、１つの状態遷移規則に対して、１つの推論規則を生成する第４のステップと、を備えた推論規則生成方法を提案している。
【０００８】
この発明によれば、安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定し、安全性ポリシを満たすプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する。また、安全性ポリシを満たさないプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する。そして、１つの状態遷移規則に対して、１つの推論規則を生成する。したがって、安全性ポリシから状態遷移図を構成し、この状態遷移図に基づいて、一階述語論理における推論規則を導出する。
【０００９】
（２）本発明は、コンピュータに、安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定する第１のステップと、安全性ポリシを満たすプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する第２のステップと、安全性ポリシを満たさないプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する第３のステップと、１つの状態遷移規則に対して、１つの推論規則を生成する第４のステップと、を実行させるためのプログラムを提案している。
【００１０】
この発明によれば、安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定し、安全性ポリシを満たすプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する。また、安全性ポリシを満たさないプログラムについて、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する。そして、１つの状態遷移規則に対して、１つの推論規則を生成する。したがって、安全性ポリシから状態遷移図を構成し、この状態遷移図に基づいて、一階述語論理における推論規則を導出する。
【発明の効果】
【００１１】
本発明によれば、安全性ポリシから状態遷移図を構成し、この状態遷移図に基づいて、一階述語論理における推論規則を導出することができるという効果がある。
【発明を実施するための最良の形態】
【００１２】
以下、本発明の実施形態について、図面を用いて、詳細に説明する。
なお、本実施形態における構成要素は適宜、既存の構成要素等との置き換えが可能であり、また、他の既存の構成要素との組合せを含む様々なバリエーションが可能である。したがって、本実施形態の記載をもって、特許請求の範囲に記載された発明の内容を限定するものではない。
【００１３】
図１から図３を用いて、本実施形態について説明する。
なお、本発明においては、安全性ポリシを満たさないプログラム、もしくは、安全性ポリシを満たすプログラムの動作を、状態遷移図で規定する。そして、ここで得られた状態遷移図において、初期状態を推論規則における初期条件に対応させ、受理状態以外の状態を推論規則における最終状態に対応させる。また、１つの状態遷移規則に対し、１つの推論規則を生成する。以下、図１を用いて、詳細な手順を説明する。
【００１４】
まず、安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定する（ステップＳ１０１）。次に、安全性ポリシを満たすプログラムか否かを判断し（ステップＳ１０２）、安全性ポリシを満たすプログラムについては（ステップＳ１０２の「Ｙｅｓ」）、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する（ステップＳ１０３）。
【００１５】
一方、安全性ポリシを満たさないプログラムについては（ステップＳ１０２の「Ｎｏ」）、状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する（ステップＳ１０４）。
【００１６】
そして、状態遷移規則σ（ｑ１、ｘ）＝ｑ２（状態ｑ１に入力ｘが入ったら、ｑ２になるという状態遷移を意味する）に対して、推論規則（（ｑ１，ｉ）、∨Ｃｉ∈ｘ）／（ｑ２、ｉ＋１）を生成する。なお、特に、状態ｑ２が受理状態ｑｆである場合は、状態遷移規則σ（ｑ１、ｘ）＝ｑｆから生成される推論規則は、（（ｑ１，ｉ）、∨Ｃｉ∈ｘ）／ｑｆとする。
【００１７】
したがって、本実施形態によれば、安全性ポリシから状態遷移図を構成し、この状態遷移図に基づいて、一階述語論理における推論規則を導出することができる。
【００１８】
＜実施例＞
いま、実施例として、安全性ポリシを「メモリアドレス５０番地のデータは読み出し禁止」とした場合の推論規則の導出手法を考える。まず、はじめに、安全性をみたさないプログラム、すなわち、メモリアドレス５０番地のデータの読み出しを行なうプログラムの動作を状態遷移図で規定する。ここで生成される状態遷移図を図２に示す。
【００１９】
図２において、ｑ０、ｑ１、ｑｆは状態を示し、各状態間を結ぶ線は、状態遷移規則を示している。例えば、状態ｑ０から状態ｑ１に向かう線（状態遷移規則）は、状態がＩ１０であれば、ｑ０からｑ１に遷移することを示している。
【００２０】
図２の状態遷移図から導出される一階述語論理の推論規則は、図３のようになる。
図３において、ＰＲＥ＝（ｑ０、０）は初期条件を示している。また、本実施例は、「メモリアドレス５０番地のデータは読み出し禁止」という安全性ポリシに対して、メモリアドレス５０番地のデータの読み出しを行なうプログラムの動作を状態遷移図で規定したものであるから、最終条件は、ＰＯＳＴ＝¬ｑｆとなる。
【００２１】
また、図２中、（１）の状態遷移規則は、図３の推論規則（（ｑ０，ｉ）、∨Ｃｉ∈Ｉ００）／（ｑ０、ｉ＋１）に対応し、図２中、（２）の状態遷移規則は、図３の推論規則（（ｑ０，ｉ）、∨Ｃｉ∈Ｉ０１）／（ｑ１、ｉ＋１）に対応し、図２中、（３）の状態遷移規則は、図３の推論規則（（ｑ１，ｉ）、∨Ｃｉ∈Ｉ１０）／（ｑ０、ｉ＋１）に対応し、図２中、（４）の状態遷移規則は、図３の推論規則（（ｑ１，ｉ）、∨Ｃｉ∈Ｉ１１）／（ｑ１、ｉ＋１）に対応し、図２中、（５）の状態遷移規則は、図３の推論規則（（ｑ１，ｉ）、∨Ｃｉ∈Ｉ１ｆ）／ｑｆに対応する。
【００２２】
なお、推論規則生成方法の処理をコンピュータ読み取り可能な記録媒体に記録し、この記録媒体に記録されたプログラムを装置に読み込ませ、実行することによって本発明の推論規則生成方法を実現することができる。ここでいうコンピュータシステムとは、ＯＳや周辺装置等のハードウェアを含む。
【００２３】
また、「コンピュータシステム」は、ＷＷＷ（Ｗｏｒｌｄ Ｗｉｄｅ Ｗｅｂ）システムを利用している場合であれば、ホームページ提供環境（あるいは表示環境）も含むものとする。また、上記プログラムは、このプログラムを記憶装置等に格納したコンピュータシステムから、伝送媒体を介して、あるいは、伝送媒体中の伝送波により他のコンピュータシステムに伝送されても良い。ここで、プログラムを伝送する「伝送媒体」は、インターネット等のネットワーク（通信網）や電話回線等の通信回線（通信線）のように情報を伝送する機能を有する媒体のことをいう。
【００２４】
また、上記プログラムは、前述した機能の一部を実現するためのものであっても良い。さらに、前述した機能をコンピュータシステムにすでに記録されているプログラムとの組合せで実現できるもの、いわゆる差分ファイル（差分プログラム）であっても良い。
【００２５】
以上、この発明の実施形態につき、図面を参照して詳述してきたが、具体的な構成はこの実施形態に限られるものではなく、この発明の要旨を逸脱しない範囲の設計等も含まれる。
【図面の簡単な説明】
【００２６】
【図１】本実施形態に係る処理フローである。
【図２】状態遷移図の一例を示した図である。
【図３】状態遷移図から生成される推論規則の一例を示した図である。
【図４】ＰＣＣの概念図である。
【特許請求の範囲】
【請求項１】
安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定する第１のステップと、
安全性ポリシを満たすプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する第２のステップと、
安全性ポリシを満たさないプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する第３のステップと、
１つの状態遷移規則に対して、１つの推論規則を生成する第４のステップと、
を備えた推論規則生成方法。
【請求項２】
コンピュータに、
安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定する第１のステップと、
安全性ポリシを満たすプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する第２のステップと、
安全性ポリシを満たさないプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する第３のステップと、
１つの状態遷移規則に対して、１つの推論規則を生成する第４のステップと、
を実行させるためのプログラム。
【請求項１】
安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定する第１のステップと、
安全性ポリシを満たすプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する第２のステップと、
安全性ポリシを満たさないプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する第３のステップと、
１つの状態遷移規則に対して、１つの推論規則を生成する第４のステップと、
を備えた推論規則生成方法。
【請求項２】
コンピュータに、
安全性ポリシを満たすプログラムまたは安全性ポリシを満たさないプログラムの動作を状態遷移図で規定する第１のステップと、
安全性ポリシを満たすプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝ｑｆを定義する第２のステップと、
安全性ポリシを満たさないプログラムについて、前記状態遷移図の初期状態ｑ０、受理状態ｑｆに対して、初期条件ＰＲＥ＝（ｑ０、０）、最終条件ＰＯＳＴ＝¬ｑｆを定義する第３のステップと、
１つの状態遷移規則に対して、１つの推論規則を生成する第４のステップと、
を実行させるためのプログラム。
【図１】
【図２】
【図３】
【図４】
【図２】
【図３】
【図４】
【公開番号】特開２００９−６４１４２（Ｐ２００９−６４１４２Ａ）
【公開日】平成２１年３月２６日（２００９．３．２６）
【国際特許分類】
【出願番号】特願２００７−２２９９９９（Ｐ２００７−２２９９９９）
【出願日】平成１９年９月５日（２００７．９．５）
【出願人】（０００２０８８９１）ＫＤＤＩ株式会社 (2,700)
【Ｆターム（参考）】
【公開日】平成２１年３月２６日（２００９．３．２６）
【国際特許分類】
【出願日】平成１９年９月５日（２００７．９．５）
【出願人】（０００２０８８９１）ＫＤＤＩ株式会社 (2,700)
【Ｆターム（参考）】
[ Back to top ]