JP4887985B2 - ポリシ検査システム、方法、及び、プログラム - Google Patents

Description

本発明は、ポリシ検査システム、方法、及び、プログラムに関し、更に詳しくは、管理対象システムへの適用に問題があるポリシ記述を検査するポリシ検査システム、方法、及び、プログラムに関する。

ポリシを用いて管理対象システムの制御を行う技術がある（ポリシベースの管理システムについては、例えば特許文献１参照）。また、このような技術で用いるポリシについて、ポリシの検査を行うポリシ検査システムがある。従来のポリシ検査システムについては、非特許文献１、非特許文献２に記載されている。図１２は、非特許文献１に記載のポリシ検査システムの構成を示している。この従来のポリシ検査システム９００は、入力装置９１１、同時発火検査手段９１２、衝突検査手段９１３、出力装置９１４、及び、記憶装置９１７を有する。記憶装置９１７は、ポリシ記憶部９１５と、衝突ルール記憶部９１６とを含む。

入力装置９１１は、特許文献１に記載されるようなポリシ管理システムに登録しようとしているポリシ記述を受け付ける。ポリシ記述は、if-then型のルールを記述したものであり、一般に、いつポリシを実行するかを示す発火条件を記述した部分と、発火条件が満たされたときに実行される管理対象への操作を記述した部分とを含む。この従来のポリシ検査システム９００では、これらに加え、ポリシ記述に、管理対象への操作が管理対象に与える作用を表現した、∧結合された述語論理式（以下、便宜的に事後条件と呼ぶ）を含めている。

入力装置９１１は、検査対象のポリシ記述を受け付けると、同時発火検査手段９１２に、ポリシを渡す。同時発火検査手段９１２は、ポリシ記憶部９１５に既に登録されているポリシ記述を全て読み出し、読み出したポリシ記述のうちで、入力装置９１１から渡された検査対象のポリシ記述の発火条件と記号的に同一の発火条件を持つポリシ記述、つまりは同時に発火する可能性があるポリシ記述を検索し、その集合を作成する。同時発火検査手段９１２は、検査対象のポリシ記述と同時に発火する可能性があるポリシ記述の集合を作成すると、作成したポリシ記述の集合と、検査対象のポリシ記述とを、衝突検査手段９１３に渡す。

衝突検査手段９１３は、ポリシ記述の集合と、検査対象のポリシ記述とを受け取ると、衝突ルール記憶部９１６から、衝突ルールの一覧を読み込む。衝突ルールは、述語のリストである。衝突検査手段９１３は、ポリシ記述の集合と、検査対象のポリシ記述とにおける事後条件を∧結合すると、読み込んだ各衝突ルールのそれぞれに対して、作成した事後条件の論理式により真になる述語が、当該衝突ルールの中に２つ以上あるか否かを調べる。調査の結果、２つ以上あった場合には、出力装置９１４を用いて、受け付けたポリシ記述に問題がある可能性があることを出力する。

次に、非特許文献２に記載のポリシ検査システムについて説明する。図１３は、非特許文献２に記載されたポリシ検査システムの構成を示している。ポリシ検査システム９０１は、入力装置９２１、検査手段９２２、充足判定手段９２３、出力装置９２４、及び、記憶装置９２５を備える。記憶装置９２５は、ポリシ記憶部９２６を含む。入力装置９２１は、検査対象であるポリシ記述を受け付けると、検査手段９２２に、受け付けたポリシ記述を受け渡す。

検査手段９２２は、検査対象のポリシ記述を受け取ると、ポリシ記憶部９２６に既に登録されているポリシ記述を全て読み込む。検査手段９２２は、読み込んだポリシ記述のそれぞれについて、入力装置９２１から受け取った検査対象のポリシ記述と衝突するか否かを検査する。この検査には、充足判定手段９２３を用いる。検査手段９２２は、まず、ポリシの発火条件が充足可能であるか否か、つまりは、同時発火を起こすポリシ記述であるか否かを、充足判定手段９２３を用いて検査する。その後、同時発火を起こすポリシについて、ポリシ記述の操作が同時実行可能か否かを、充足判定手段９２３を用いて判断する。発火条件及び操作方法は、述語論理によって記述されており、充足判定手段９２３は、それら述語論理が充足可能であるか否かを判断する。検査手段９２２は、同時発火するポリシ記述について、操作方法の述語論理が充足不可能と判断されると、ポリシ記述が衝突すると判定し、出力装置９２４に、その結果を出力させる。

例えば、あるコンピュータシステムの設定ファイルの属性名をｘとする。このときに、ｘ＝１０（属性ｘの値を１０にする）という操作が定義されたポリシ記述と、ｘ＝２０（属性ｘの値を２０にする）という操作が定義された別のポリシ記述との衝突を判定する場合を考える。ポリシ検査システム９０１は、与えられたポリシ記述のそれぞれの操作の∧結合の論理式、つまりｘ＝１０ ∧ ｘ＝２０の充足可能性（ｘのドメインを整数とする）を判定し、論理式が充足不可能である、すなわち与えられた論理式を満たすような変数の組み合わせが存在しないことを発見すると、与えられたポリシの組み合わせが整合しない（衝突する）と判定する。

特開２００２−１１１７２９号公報 シェタン・シバ・シャンカ（Chetan Shiva Shankar）、他 著、「アン・イーシーエー―ピー・ポリシーベースド・フレームワーク・フォー・マネージング・ユビキタス・コンピューティング・エンバイロメンツ（An ECA-P Policy-based Framework for Managing Ubiquitous Computing Environments）、モビキタス（Mobiquitous）2005議事録、米国 ダクシ・アグラワル（Dakshi Agrawal）、他 著「ポリシー・ラティフィケーション（Policy Ratification）」、ポリシー（Policy）2005議事録、米国

非特許文献１では、ポリシ記述に事後条件を与え、更に、不適切な事後条件の組み合わせを示す衝突ルールを与えることにより、ポリシ記述間の不整合を検出する。非特許文献１では、事前に、人間が、あらかじめ考え得る全ての不適切なポリシ記述の組み合わせを事前に想定してポリシ検査システムに与える必要があり、作成者の作業負担が大きいという問題がある。また、全ての不適切な組み合わせを用意することは困難であり、衝突ルールの不足によって問題があるポリシ記述を見逃す可能性が高くなる。

非特許文献２では、非特許文献１とは異なり、充足判定により、衝突ルールを人間が与えることなしに、衝突を検査することが可能である。しかしながら、非特許文献２では、管理対象システム上で成立する条件を考慮していない。このため、管理対象システムの性質を適切に反映したポリシ検査を行うことができず、ポリシの衝突を見逃して、本来は衝突するはずのポリシ記述の組み合わせを、衝突しないと判定する場合があるという問題がある。

非特許文献２における問題点について、具体例を挙げて説明する。あるポリシにａ→ｂ（ａならばｂ）という定義があり、別のポリシにａ→¬ｂ（ａならばｂでない）という定義があったとする。ａ、ｂは、例えばｘ＞０やｙ＝４などの真偽値を示す原始論理式とする。また、充足判定手段９２３における衝突判定では、充足不可能な場合にポリシは衝突すると判定するものとする。

上記２つのポリシの定義を∧結合した（ａ→ｂ）∧（ａ→¬ｂ）は、¬ａ（ａではない）を仮定することで真になるため、前記ポリシ検査システムでは衝突しないと判断される。しかし、実際の管理対象システムが、「ａ」が常に成立するという性質を備えていた場合、¬ａは成立しないため、先のポリシは衝突すると判断されなければならない。このように、非特許文献２に記載の従来のポリシ検査システムでは、管理対象システムにおいて成立する条件を考慮していないため、ポリシの衝突を見逃す可能性が高くなる。

また、非特許文献２では、論理式中の束縛変数が示す対象の等価性を何ら考慮していない。このため、充足可能性判定によりポリシの衝突を検査する場合に、論理式中に登場する束縛変数が、同一の管理対象を指している可能性を考慮した制約が含まれないことで、ポリシの衝突を見逃す可能性があるという問題もある。

本発明は、充足可能性判定により問題のあるポリシ記述を検査する際に、管理対象システムの性質に基づいて、ポリシ記述を検査できるポリシ検査システムを提供することを目的とする。

また、本発明は、上記目的を達成した上で、充足可能性判定により問題のあるポリシ記述を検査する際に、論理式中に登場する束縛変数が示す対象の等価性に関する制約を与えることができるポリシ検査システム、方法、及び、プログラムを提供することを目的とする。

上記目的を達成するために、本発明のポリシ検査システムは、
検査対象のポリシ記述を検査するポリシ検査システムであって、
前記検査対象のポリシ記述を受け付ける入力装置と、
管理対象システムの状態について常に成立する条件を一階述語論理により記述した不変条件を記憶した不変条件記憶部と、
登録済みのポリシ記述を記憶するポリシ記憶部と、
前記入力装置により受け付けられた前記ポリシ記述中で定義されている操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した所定の論理式で表される事後条件と前記不変条件記憶部に記憶されている前記不変条件とに基づいて、前記入力装置により受け付けられた前記検査対象のポリシ記述の検査を行う検査手段と、を有し、
前記検査手段が、
論理式の充足判定を行う充足判定手段と、
前記不変条件記憶部に記憶された不変条件及び前記ポリシ記憶部に記憶された登録済みのポリシ記述を参照し、前記入力装置により受け付けられた前記検査対象のポリシ記述に含まれる事後条件と前記登録済みポリシ記述に含まれる事後条件と前記不変条件とを∧結合した論理式を生成する論理式生成手段と、
前記論理式生成手段が生成した論理式の充足可能性を、前記充足判定手段を用いて判定するポリシ整合性検査手段と、
前記管理対象システムの状態を表現したインスタンスの属性のうち、管理対象システムのクラスに関し、同一クラス間で常に唯一の値をとるＫｅｙ属性の情報を記憶するＫｅｙ属性記憶部と、
を有し、
前記ポリシ整合性検査手段による判定に先立って、前記不変条件記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を、前記充足判定手段を用いて判定する不正ポリシ検査手段を更に備え、
前記管理対象システムの状態はインスタンスによって表現され、
前記不正ポリシ検査手段は、
前記充足判定手段による充足性判定に先立って、前記Ｋｅｙ属性記憶部を参照し、前記管理対象システムの状態を表現したインスタンスのうち充足性判定の対象となる論理式に登場する束縛変数に対応付けられたインスタンスが等しいことを条件とする等価性制約を当該論理式に制約として加え、
前記充足性判定の対象となる論理式に登場する２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、
ことを特徴とする。

本発明のポリシ検査方法は、検査対象のポリシ記述を受け付ける入力装置と、管理対象システムの状態について常に成立する条件を一階述語論理により記述した不変条件を記憶した不変条件記憶部と、登録済みのポリシ記述を記憶するポリシ記憶部と、前記入力装置により受け付けられた前記ポリシ記述中で定義されている操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した所定の論理式で表される事後条件と前記不変条件記憶部に記憶されている前記不変条件とに基づいて、前記入力装置に受け付けられた前記検査対象のポリシ記述の検査を行う検査手段と、を有するコンピュータを用いて、検査対象のポリシ記述を検査するポリシ検査方法であって、
前記コンピュータが、前記不変条件記憶部に記憶している不変条件と、前記入力装置により入力された前記ポリシ記述に定義された操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した論理式とに基づいて、前記検査対象のポリシ記述の検査を検査手段により行うステップを有し、
前記ポリシ記述が、ポリシ記述に定義された操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した事後条件及びポリシ発火条件を一階述語論理で記述した事前条件を含んでおり、
前記ポリシ記述の検査を行うステップが、
前記コンピュータが、前記不変条件を記憶する前記不変条件記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と前記不変条件とを∧結合した論理式を生成するステップと、
生成した論理式の充足可能性を判定する不正ポリシ検査ステップと、
前記不正ポリシ検査ステップで充足すると判定すると、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事前条件と前記登録済みポリシ記述に含まれる事前条件と前記不変条件とを∧結合した論理式を生成するステップと、
生成した論理式の充足可能性を判定するステップと、
該判定するステップにおいて充足すると判定すると、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と前記登録済みポリシ記述に含まれる事後条件と前記不変条件とを∧結合した論理式を生成するステップと、
生成した論理式の充足可能性を判定するポリシ整合性検査ステップと、
を有し、
前記ポリシ整合性検査ステップによる判定に先立って、前記不変条件記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を判定する不正ポリシ検査ステップを更に備え、
前記不正ポリシ検査ステップが、前記論理式の充足性判定に先立って、前記コンピュータが、前記管理対象システムの状態を表現したインスタンスの属性のうち、同一クラス間で常に唯一の値をとるＫｅｙ属性の情報を記憶するＫｅｙ属性記憶部を参照し、充足性判定の対象となる論理式に登場する束縛変数に対応付けられたインスタンスが等しいことを条件とする等価性制約を当該論理式に制約として加えるステップを含み、
前記制約を加えるステップでは、前記充足性判定の対象となる論理式に登場する２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、
ことを特徴とする。

本発明のプログラムは、コンピュータに、検査対象のポリシ記述を検査する処理を実行させるプログラムであって、
コンピュータを、検査対象のポリシ記述を受け付ける入力装置と、管理対象システムの状態について常に成立する条件を一階述語論理により記述した不変条件を記憶した不変条件記憶部と、登録済みのポリシ記述を記憶するポリシ記憶部と、前記入力装置により受け付けられた前記ポリシ記述中で定義されている操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した所定の論理式で表される事後条件と前記不変条件記憶部に記憶されている前記不変条件とに基づいて、前記入力装置で受け付けられた前記検査対象のポリシ記述の検査を行う検査手段と、として機能させ、
前記コンピュータに、
管理対象システムの状態について常に成立する条件を一階述語論理により記述した不変条件と、前記入力装置により入力された前記ポリシ記述に定義された操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した論理式とに基づいて、前記検査対象のポリシ記述の検査を前記検査手段により行うステップを実行させるプログラムであって、
前記ポリシ記述が、ポリシ記述に定義された操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した事後条件及びポリシ発火条件を一階述語論理で記述した事前条件を含んでおり、
前記ポリシ記述の検査を行うステップが、
前記不変条件記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と、前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を判定する不正ポリシ検査ステップと、
前記不正ポリシ検査ステップで充足すると判定すると、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事前条件と、前記登録済みポリシ記述に含まれる事前条件と、前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を判定し、該判定において充足すると判定すると、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と、前記登録済みポリシ記述に含まれる事後条件と、前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を判定するポリシ整合性検査ステップとを実行させ、
前記不正ポリシ検査ステップが、
前記論理式の充足性判定に先立って、前記管理対象システムの状態を表現したインスタンスの属性のうち、同一クラス間で常に唯一の値をとるＫｅｙ属性の情報を記憶するＫｅｙ属性記憶部を参照し、充足性判定の対象となる論理式に登場する束縛変数に対応付けられたインスタンスが等しいことを条件とする等価性制約を当該論理式に制約として加えるステップを含み、
前記制約を加えるステップでは、前記充足性判定の対象となる論理式に登場する２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、
ことを特徴とする。

以下、図面を参照し、本発明の実施の形態を詳細に説明する。図１は、本発明の第１実施形態のポリシ検査システムの構成を示している。ポリシ検査システム１０は、第１の検査手段１１、第２の検査手段１２、充足判定手段１３、入力装置１４、出力装置１５、及び、記憶装置１６を有する。ポリシ検査システム１０は、プログラム動作により動作するコンピュータシステムとして構成される。記憶装置１６は、ハードディスク装置等の記憶装置であり、管理対象システムの状態について常に成立すべき条件を一階述語論理式で表現した不変条件を記憶する不変条件記憶部１６１と、既に受理されてポリシ管理システムに登録されているポリシ記述を記憶するポリシ記憶部１６２とを有する。

入力装置１４は、検査対象であるポリシ記述を受け付けるコンピュータの入力用デバイスである。第１の検査手段（不正ポリシ検査手段）１１は、検査対象のポリシ記述が、管理対象システムに対して不正な作用を持つか否かを判定する。第２の検査手段（ポリシ整合性検査手段）１２は、検査対象のポリシ記述が既に登録されているポリシ記述と整合するか否かを判定する。充足判定手段１３は、第１の検査手段１１及び第２の検査手段１２が検査を行う際に利用され、述語論理式の充足可能性を判定する。出力装置１５は、ディスプレイやファイルなどの外部出力装置であり、第１の検査手段１１及び第２の検査手段１２が検査結果を出力する際に利用される。

図２は、ポリシ記述の構成を示している。ポリシ記述７１は、ポリシ本体と、ポリシ仕様とから構成される。ポリシ本体は、ポリシ管理システムで利用されるif-then型のルールを記述した部分である。ポリシ仕様は、ポリシ本体の振る舞いを表現したものである。図３に、ポリシ仕様の構成を示す。ポリシ仕様７２は、事前条件と事後条件とを含む。事前条件は、ポリシ本体の発火条件を、一階述語条件により表現したものである。事後条件は、ポリシ本体に定義された操作の直後に、管理対象システムの状態について成立すべき条件を表現したものである。

なお、ポリシ記述において、ポリシ本体の内容とポリシ仕様の内容とが重複する場合には、ポリシ本体に記載される情報をポリシ仕様として利用し、ポリシ仕様には重複する情報を含めなくてよい。例えば、ポリシ本体の発火条件が述語論理により記述される場合には、その論理式を事前条件として扱い、ポリシ仕様には事前条件を含めなくてよい。

第１の検査手段１１は、入力装置１４によって入力された検査対象のポリシ記述を受け取る。第１の検査手段１１は、ポリシ記述を受け取ると、不変条件記憶部１６１から、管理対象システムの状態について常に成立すべき条件を表現した不変条件を読み込み、ポリシ記述と読み込んだ不変条件との充足可能性を、充足判定手段１３を用いて判定する。第１の検査手段１１は、充足判定手段１３が充足可能と判定すると、検査対象のポリシ記述を第２の検査手段１２に受け渡す。第２の検査手段１２は、ポリシ記述を受け取ると、ポリシ記憶部１６２から、既に登録されているポリシ記述を全て読み込み、読み込んだ各ポリシ記述と、検査対象のポリシ記述とが整合するか否かを、充足判定手段１３を用いて判定する。

充足判定手段１３は、与えられた一階述語論理式の充足可能性を判定する機能を備えている。充足可能性の判定方法は、例えば、「デイビッド・デトレフ（DAVID DETLEFS）、他 著、「シンプリファイ：ア・セオレム・プルーバー・フォー・プログラム・チェッキング（Simplify: A Theorem Prover for Program Checking）、ジャーナル・オブ・エーシーエム（Journal of the ACM）,米国、 第５２巻、３号、２００５年５月、３６５−４７３頁」に記載されている。

図４は、ポリシ検査システム１０の全体の動作の概略手順を示している。入力装置１４により、検査対象のポリシ記述を受け付ける（ステップＡ１０）。第１の検査手段１１は、入力装置１４から検査対象のポリシ記述を受け取り、そのポリシ記述が管理対象システムに対して不正な作用を与えるか否かを検査する（ステップＡ２０）。第１の検査手段１１による検査の結果、問題がないことが確認されると、第２の検査手段１２は、検査対象のポリシ記述が、既に登録されている他のポリシ記述との間で不整合を起こすか否かを検査し（ステップＡ３０）、その検査結果を出力装置１５に出力する。

図５は、図４のステップＡ２０における第１の検査手段１１による検査の動作手順を示している。第１の検査手段１１は、入力装置１４から検査対象のポリシ記述を受け取ると、不変条件記憶部１６１から、一階述語論理で記述された不変条件を読み込む。第１の検査手段１１は、不変条件を読み込むと、検査対象のポリシ記述のポリシ仕様における事後条件（図３）と、読み込んだ不変条件とを∧によって結合した論理式を作成する（ステップＢ１０）。論理式の作成後、第１の検査手段１１は、作成した論理式を、充足判定手段１３が検査可能な形に変換する（ステップＢ２０）。例えば、上記した文献に記載の充足可能性判定ツールであるシンプリファイ（simplify）は、論理式がＳ式である必要があり、ステップＢ２０では、作成した論理式をこのような形式に変換する。

第１の検査手段１１は、論理式の変換後、検査対象のポリシ記述における事後条件と不変条件とから構成される論理式が充足可能であるか否かを、充足判定手段１３を用いて判定する（ステップＢ３０）。第１の検査手段１１は、充足判定手段１３により、充足可能と判定されたか否かを判断する（ステップＢ４０）。第１の検査手段１１は、論理式が充足不可能であると判定されたときには、検査対象のポリシ記述は管理対象システムに対して不正な作用を持つと判断し、出力装置１５に、ポリシ記述に問題がある旨のエラーを出力して（ステップＢ５０）、全体の処理を終了する。第１の検査手段１１は、論理式が充足可能であると判定されたときには、検査対象のポリシ記述は管理対象システムに対して不正な作用を持たないと判断し、ポリシ記述及び不変条件を第２の検査手段１２に受け渡して、ステップＡ３０（図４）の検査を実行させる。

図６は、図４のステップＡ３０における第２の検査手段１２による検査の動作手順を示している。第２の検査手段１２は、図５に示す手順で、不変条件と同時に充足可能であることが確認されたポリシ記述と、不変条件とを第１の検査手段１１から受け取る。第２の検査手段１２は、ポリシ記述と不変条件とを受け取ると、ポリシ記憶部１６２から、登録済みのポリシ記述に含まれるポリシ仕様を全て読み込み（ステップＣ１０）、ポリシ記述の検査を開始する。第２の検査手段１２は、読み込んだポリシ仕様の全てについて検査を終了したか否かを判断し（ステップＣ２０）、まだ終了していない場合には、未検査のポリシ仕様の中から１つを選択する（ステップＣ３０）。

第２の検査手段１２は、第１の検査手段１１から受け取った検査対象のポリシ記述が、ステップＣ３０で選択したポリシ仕様と同時に発火する可能性があるか否かを判断する（ステップＣ４０）。ステップＣ４０で同時発火する可能性があると判断されるということは、管理対象システムで満たされるべき条件下において、検査対象のポリシ記述と、ステップＣ３０で選択されたポリシ記述とが同時に適用される可能性があるということを意味している。同時に発火する可能性がない場合には、２つのポリシ記述は同時に適用されることがないので、ステップＣ２０へ戻り、検査を行っていないポリシ仕様がまだ残っているか否かを判断して次のポリシ仕様を選択する。第２の検査手段１２は、同時発火が可能であると判断すると、検査対象のポリシ記述と、ステップＣ３０で選択したポリシ仕様とが、同時に実行可能か否かを判定する（ステップＣ５０）。

第２の検査手段１２は、ステップＣ５０で同時実行が不可能であると判断すると、ポリシ記述に問題がある旨を、出力装置１５を用いて出力し（ステップＣ６０）、全体の処理を終える。同時実行が可能であると判断した場合には、ステップＣ２０に戻り、未検査のポリシ記述が残っているか否かを判断する。第２の検査手段１２は、ステップＣ３０からステップＣ５０までの検査を、ステップＣ２０で未検査のポリシ仕様がないと判断されるまで行う。第２の検査手段１２は、検査の結果、ステップＣ５０で、検査対象のポリシ記述と同時実行が不可能と判定されるポリシ仕様が存在しないときには、検査対象のポリシ記述には問題がないと判断し、検査対象のポリシ記述を、ポリシ記憶部１６２に登録し（ステップＣ７０）、検査を終了する。

図７は、同時発火の可能性を判断するステップＣ４０（図６）の動作手順の詳細を示している。ステップＣ４０では、第２の検査手段１２は、まず、検査対象のポリシ記述に含まれる事前条件と、不変条件と、ステップＣ３０で選択されたポリシ仕様の事前条件とを∧で結合した論理式を作成する（ステップＤ１０）。次いで、作成した論理式を、充足判定手段１３が検査可能な形に変換する（ステップＤ２０）。その後、ステップＤ１０で作成した論理式が充足可能か否かを、充足判定手段１３を用いて判定する（ステップＤ３０）。

第２の検査手段１２は、ステップＤ３０の判定で、充足可能と判定されたか否かを判断する（ステップＤ４０）。論理式が充足可能と判定された場合には、検査対象のポリシ記述と、ステップＣ３０（図６）で選択されたポリシ仕様に対応付けられるポリシ記述とが同時に発火する可能性があるため、同時発火可能と判定する（ステップＤ５０）。この場合には、ステップＣ４０からステップＣ５０へ進んで、同時実行可能か否かの検査を行う。一方、論理式が充足不可能と判断された場合には、検査対象のポリシ記述と、選択されたポリシ仕様に対応するポリシ記述とが同時に発火する可能性がないため、同時発火なしと判定する（ステップＤ６０）。同時発火しない場合には、当該組み合わせについては、ポリシ記述間に不整合は発生しないものと判定し、次のポリシ仕様を選択するために、ステップＣ４０からステップＣ２０に戻る。

図８は、実行可能か否かを判定するステップＣ５０（図６）の動作手順の詳細を示している。ステップＣ５０では、第２の検査手段１２は、まず、検査対象のポリシ記述に含まれる事後条件と、不変条件と、ステップＣ３０で選択されたポリシ仕様の事後条件とを∧で結合した論理式を作成する（ステップＥ１０）。次いで、作成した論理式を、充足判定手段１３が検査可能な形に変換する（ステップＥ２０）。その後、ステップＥ１０で作成した論理式が充足可能か否かを、充足判定手段１３を用いて判定する（ステップＥ３０）。

第２の検査手段１２は、ステップＥ３０の判定で、充足可能と判定されたか否かを判断する（ステップＥ４０）。論理式が充足可能と判定された場合には、検査対象のポリシ記述と、ステップＣ３０（図６）で選択されたポリシ仕様に対応するポリシ記述とを同時に実行しても問題が発生しないため、同時実行可能と判定する（ステップＥ５０）。この場合には、ステップＣ５０からステップＣ２０に戻って、次の組み合わせでの検査を行う。一方、論理式が充足不可能と判断された場合には、検査対象のポリシ記述と、選択されたポリシ仕様に対応するポリシ記述とを同時に実行することは不可能であると判定する（ステップＥ６０）。このようなポリシ記述の組み合わせは不正であり、ステップＣ５０からステップＣ６０へ進んで、検査対象のポリシに問題がある旨を出力する。

本実施形態では、ポリシ記述に対応した述語論理式の充足可能性により、２つのポリシ記述間の整合性を検査する際に、検査対象のポリシ記述に対応する論理式と、既に登録済みのポリシ記述に対応する論理式とを∧結合した論理式に、管理対象システムの状態に対して常に成立する不変条件を更に∧結合した論理式を作成し、その論理式に対して、充足可能性を判断する。このように、管理対象システムの性質を、検査時の制約として加えることにより、ポリシ記述が適用される環境が、より正確に論理式として表現されることになり、その結果、より正確にポリシ記述の問題を検査することができるようになる。

次に、本発明の第２実施形態について説明する。図９は、本発明の第２実施形態のポリシ検査システムの構成を示している。本実施形態のポリシ検査システム１０ａは、記憶装置１６ａがＫｅｙ属性記憶部１６３を備える点で、図１に示す第１実施形態のポリシ検査システム１０と相違する。本実施形態では、管理対象システムがオブジェクト指向型の情報モデルで表現されており、その情報モデルに登場するクラスや属性名を用いて条件を記述する際に、束縛変数で示されたインスタンスが同一である場合を論理式中に制約として含める。管理対象システムを表現する情報モデルの一例としては、「“シー・アイ・エム コア モデル ホワイトペーパー（CIM Core Model White Paper）ver2.4”２０００年８月３０日［online］［平成１７年３月８日検索］、ディストリビューティッド・マネージメント・タスクフォース(Distributed Management Task Force)、インターネット ＜URL http://www.dmtf.org/standards/documents/CIM/DSP0111.pdf＞」に示されるシー・アイ・エム（ＣＩＭ）がある。

管理対象システムを構成する各管理対象物は、ある特定の性質を持ったクラスのインスタンスとして表現される。以下、本実施形態における条件検査システムの説明に先立って、そのような管理対象システムの状態に対する条件の一例を示す。管理対象システムであるコンピュータで稼動するプロセスであって、特に外部に特定のサービスを提供するプロセスの状態は、Ｓｅｒｖｉｃｅクラスのインスタンスとして表現されているとする。このとき、Ｓｅｒｖｉｃｅクラスは、状態を表現する属性として、ＮａｍｅとＳｔａｔｕｓとを持つ。Ｎａｍｅはサービスの名前であり、Ｓｔａｔｕｓはサービスの稼働状況を示す。

上記Ｓｅｒｖｉｃｅクラスに関する条件としては、下記の条件が考えられる。
∃s∈Service , s.Name=“mysql” ∧ s.Status=“running” （論理式Ａ）
上記条件（論理式Ａ）は、Ｓｅｒｖｉｃｅクラスのインスタンスであって、Ｎａｍｅ属性がｍｙｓｑｌであり、かつ、Ｓｔａｔｕｓ属性がｒｕｎｎｉｎｇであるインスタンスが存在することを示している。このような論理式は、例えば、ＭｙＳＱＬサービスが稼動状態になったら発火するポリシ記述の事前条件や、ＭｙＳＱＬサービスを稼動状態にするポリシ記述の事後条件などとして与えられることが考えられる。

次に、問題を説明するために、上記の論理式Ａとは別に、
∃t∈Service , t.Name=“mysql” ∧ t.Status =“stopped” （論理式Ｂ）
という条件（論理式Ｂ）を考える。この論理式Ｂは、先に説明した論理式Ａとは、Ｓｔａｔｕｓ属性の値が異なっている。これら２つの論理式Ａ及び論理式Ｂを∧結合したものは、充足可能である。

一方、インスタンスを一意に識別するために、特定の属性は、クラスのインスタンス間で一意の値をとるものとする。そのような属性を、Ｋｅｙ属性と呼ぶ。Ｎａｍｅ属性をＫｅｙ属性と仮定すると、論理式Ａと論理式Ｂでは、ｓとｔではＮａｍｅ属性の値が等しいため、ｓとｔは、同じインスタンスに対する言明を与えていることになる。この場合、ある論理式、すなわちポリシ記述と、別のポリシ記述とにおいて、同じインスタンスの属性に対して異なる値を同時に設定するように条件が与えられているため、このような組み合わせのポリシ記述は整合しないように結果を出力しなければならない。このように、インスタンスが同一の場合を考慮した充足可能性の判定を実現するために、本実施形態では、Ｋｅｙ属性を用いて、充足判定時にインスタンスの等価性制約を加える。

Ｋｅｙ属性記憶部１６３は、クラス名と、当該クラス名に定義されたＫｅｙ属性のリストとを対応付けて記憶する。１つのクラスには、１つ以上のＫｅｙ属性が定義され、Ｋｅｙ属性が複数ある場合には、複数のＫｅｙ属性を組み合わせた値が、同一クラスのインスタンス間で唯一となる。本実施形態では、第１の検査手段１１及び第２の検査手段１２は、Ｋｅｙ属性を利用した等価性制約を、充足可能性を判定する式に加えて、充足可能性の判定を行う。

図１０は、充足可能性判定の前に実行するインスタンスの等価性制約を追加する処理の動作手順を示している。この処理は、ステップＢ２０（図５）、ステップＤ２０（図７）、又は、ステップＥ２０（図８）で論理式を充足判定手段１３が検査可能な形式に変換した後に実行される。なお、等価性制約を加える対象となる論理式は、事後条件と不変条件とを∧で結合したもの（図５）、検査対象のポリシ記述の事前条件と不変条件と登録済みポリシ記述の事前条件とを∧で結合したもの（図７）、又は、検査対象のポリシ記述の事後条件と不変条件と登録済みポリシ記述の事後条件とを∧で結合したもの（図８）となるが、論理式に対する操作は何れの場合でも同じ動作となるため、以下では、代表として、第１の検査手段１１が、事後条件と不変条件とを∧で結合した論理式に対して等価性制約を加える例を用いて説明する。

第１の検査手段１１は、まず、論理式を冠頭標準形に変換する。これにより、論理式中に登場する束縛変数名は重複しないように名前が付け替えられる。次いで、その論理式に登場するクラス名と、当該クラス名のインスタンスに対応付けられた束縛変数名のリストとを組にした表を作成する（ステップＦ１０）。このとき、クラスのインスタンスに対応する束縛変数の数が１つのみであるときには、表に含めない。

ステップＦ１０で作成された表の各行には、クラス名と、対応する束縛変数のリストとが格納されている。第１の検査手段１１は、表の全ての行について処理を完了したか否かを判断する（ステップＦ２０）。未処理の行が残っているときには、未処理の行（クラス名）を、１つを選択する（ステップＦ３０）。第１の検査手段１１は、選択した行に含まれる束縛変数のリストから２つを選択してできる各束縛変数の可能な組み合わせを作成する。その後、作成した組み合わせに、未処理の組み合わせが存在するか否かを判断する（ステップＦ４０）。

第１の検査手段１１は、未処理の組み合わせが残っているときには、未処理の組み合わせのうちの１つを選択し、論理式を格納するための空のリストを作成する（ステップＦ５０）。このリストを制約リストと呼ぶ。第１の検査手段１１は、選択した行に含まれるクラス名を用いて、Ｋｅｙ属性記憶部１６３から、当該クラス名に定義されたＫｅｙ属性名のリストを取得する（ステップＦ６０）。第１の検査手段１１は、取得したＫｅｙ属性の全てについて処理を完了したか否かを判断する（ステップＦ７０）。

第１の検査手段１１は、全てのＫｅｙ属性について処理を完了していないときには、未処理のＫｅｙ属性を１つ選択し、当該組み合わせに含まれる束縛変数のＫｅｙ属性が等しいことを示す論理式を生成する。第１の検査手段１１は、生成した論理式を、制約リストに格納する（ステップＦ８０）。その際、第１の検査手段１１は、制約リストが空であれば、生成した論理式を、そのまま制約リストに格納する。制約リストに、既に論理式が格納されているときには、格納すべき論理式と、格納済みの論理式とを∧結合したものを、制約リストに格納する。

例えば、束縛変数名の組み合わせをｘとｙとし、Ｋｅｙ属性名をｐとすると、生成される論理式は、ｘ．ｐ＝ｙ．ｐとなる。制約リストが空であれば、第１の検査手段１１は、ステップＦ８０で、制約リストにｘ．ｐ＝ｙ．ｐを格納する。制約リストに、既に論理式Ｌが格納されている場合には、ステップＦ８０で、Ｌ∧（ｘ．ｐ＝ｙ．ｐ）を制約リストに格納する。

第１の検査手段１１は、ステップＦ８０からステップＦ７０へ戻り、未処理の組み合わせが存在するか否かを判断する。全てのＫｅｙ属性について処理を終えると、制約リストに含まれる論理式と、当該組み合わせに含まれる変数名が示すインスタンスが等しいことを示す論理式とが、論理的に等価であることを示す論理式を作成し、充足判定を行う論理式に、作成した論理式を∧結合して制約を追加する（ステップＦ９０）。例えば、制約リストに含まれる論理式をＬ、束縛変数名の組み合わせをｘとｙとすると、生成される論理式は、
（Ｌ）⇔ （ｘ＝ｙ）、又は、（（Ｌ）→（ｘ＝ｙ））∧（（ｘ＝ｙ）→（Ｌ））
となる。生成された論理式をＱとし、充足判定を行う論理式をＴとすると、ステップＦ９０では、論理式Ｔと論理式Ｑとを∧結合したＴ∧Ｑを生成する。

第１の検査手段１１は、ステップＦ９０の実行後、ステップＦ４０に戻り、未処理の組み合わせが存在するか否かを判断する。未処理の組み合わせが存在するときには、ステップＦ５０へ進み、未処理の行を１つ選択する。ステップＦ５０以降の処理を全ての組み合わせに対して実行したときには、ステップＦ２０に戻り、ステップＦ１０で作成した表の全ての行について、処理を完了したか否かを判断する。未処理の行が残っているときには、ステップＦ３０へ進み、未処理の行を１つ選択する。未処理の行がない、つまり、作成した表の全ての行について、ステップＦ２０以降の処理を完了したときには、等価性制約の処理を終了し、その後の、充足性判定処理（ステップＢ３０（図５））へ進む。

本実施形態では、論理式を、充足判定手段１３に与えて判定を行う前に、各クラスごと、各束縛変数の組み合わせごとに、等価性に関する制約式を作成し、これを充足判定を行う論理式に∧結合していき、制約式が追加された論理式に対して、充足判定手段１３による判定を行う。このように、論理式の充足判定に先立って、論理式に登場するクラス名に定義された各Ｋｅｙ属性のリストを用いて、インスタンスの等価性制約を生成し、充足判定を行う論理式に∧結合した上で充足判定を行うことで、検査に用いる論理式がより厳密になり、第１実施形態で得られる効果に加えて、インスタンスの等価性を考慮した、より正確なポリシ検査が可能となるという効果を得ることができる。

次に、本発明の第３実施形態について説明する。まず、本実施形態の目的について説明する。第２実施形態で説明したインスタンスの等価性制約追加では、登場するクラスに定義された全てのＫｅｙ属性について同じ値をとるようなインスタンスは同一であるという制約を加えた。この制約は、何れかのＫｅｙ属性が欠落していた場合、或いは、Ｋｅｙ属性に関する条件が登場しない場合など、束縛変数に対応付けられたインスタンスが同一であるか否かが明らかでない場合は充足判定に影響を与えない。よって、インスタンスが確実に同一である場合に加えて、同一であるか否かが明らかでない場合にも、同一であるとみなす手段が必要となる。本実施形態では、確実にインスタンスが異なることが論理式の条件により明らかにされている場合を除いて、束縛変数に対応付けられたインスタンス同士が等しいとする制約を加える。このようにすることで、インスタンスが同一か、又は、異なるかがわからないときに、「インスタンスは同一である」という制約を加えて充足可能性を判定できる。

本実施形態におけるポリシ検査システムの構成は、図９に示すポリシ検査システム１０ａの構成と同じである。図１１は、本実施形態の動作手順の一部を示している。本実施形態のポリシ検査システムの動作は、図１０に示す制約追加処理において、ステップＦ６０以降の処理手順が、第２実施形態の動作手順と相違する。第１の検査手段１１（又は第２の検査手段１２）は、ステップＦ５０（図１０）で、特定のクラス名と、当該クラス名に対応付けられた束縛変数名の組み合わせを１つ選択すると、Ｋｅｙ属性記憶部１６３から、当該クラス名に定義されたＫｅｙ属性の一覧を取得し、取得したＫｅｙ属性のうちで、充足判定を行う論理式の中で組み合わせに含まれる２つの束縛変数名を用いて参照されるＫｅｙ属性のみを検出する（ステップＧ１０）。

例えば、組み合わせに含まれる束縛変数名をｘ、ｙとし、ＣｌａｓｓＡという名前のクラスについて処理をしているとする。また、ＣｌａｓｓＡのＫｅｙ属性がｐ１、ｐ２であったとする。この場合、論理式中に「ｘ．ｐ１」、「ｙ．ｐ１」、「ｙ．ｐ２」という属性参照が現れたとすると、ステップＧ１０では、Ｋｅｙ属性ｐ１のみが検出される。Ｋｅｙ属性ｐ２については、束縛変数ｙによる参照はあるが、束縛変数ｘによる参照がないために除外される。第１の検査手段１１は、ステップＧ１０で、Ｋｅｙ属性を検出できたか否かを判断する（ステップＧ２０）。検出されたＫｅｙ属性が存在しない場合には、組み合わせに含まれる２つの束縛変数名が等しいという制約を、制約リストに追加する（ステップＧ５０）。例えば、組み合わせに含まれる２つの束縛変数名がｘとｙであれば、（ｘ＝ｙ）を制約リストに追加する。

第１の検査手段１１は、ステップＧ１０で検出したＫｅｙ属性のすべてについて処理を完了したか否かを判断する（ステップＧ３０）。未処理のＫｅｙ属性が存在する場合には、その中から１つを選択し、当該組み合わせに含まれる束縛変数のＫｅｙ属性が等しいことを示す論理式を生成し、生成した論理式を制約リストに格納する（ステップＧ４０）。ステップＧ４０では、図１０のステップＦ８０と同様に、制約リストが空であれば、生成した論理式をそのまま制約リストに格納し、制約リストに既に論理式が格納されているときには、格納すべき論理式と、格納済みの論理式とを∧結合したものを、制約リストに格納する。

第１の検査手段１１は、ステップＧ４０で論理式を制約リストに格納すると、ステップＧ３０に戻って、全てのＫｅｙ属性について処理したか否かを判断する。全てのＫｅｙ属性について処理を終えた場合には、制約リストに含まれる論理式と、当該組み合わせに含まれる変数名が示すインスタンスが等しいことを示す論理式とが論理的に等価であることを示す論理式を作成し、作成した論理式を、充足判定を行う論理式に∧結合する（ステップＧ６０）。例えば、制約リストに含まれる論理式をＬ、束縛変数名の組み合わせをｘとｙとすると、作成される論理式は、
（Ｌ）⇔ （ｘ＝ｙ）、又は、（（Ｌ）→（ｘ＝ｙ））∧（（ｘ＝ｙ）→（Ｌ））
となる。この作成された論理式をＱとし、充足判定を行う論理式をＴとすると、Ｔ∧Ｑ
が新たに充足判定を行う論理式となる。

上記した図１１に示す処理を加えた制約追加手順は、図５のステップＢ２０とステップＢ３０の間、及び、図８のステップＥ２０とステップＥ３０の間に挿入することが好ましい。これは、図５に示す検査、及び、図８に示す検査では、検査対象のポリシ記述が、不変条件又は他のポリシ記述と衝突するか否かを判定するため、危険な可能性がある場合に充足不可能となることが好ましいためである。インスタンスが同一かどうかがわからない場合に、同一とすることで、論理式の充足はより困難となり、潜在的に問題があるポリシ記述を検出できることになる。

一方で、図７に示す検査では、検査対象のポリシ記述と同時に発火する可能性があるポリシを選別しているため、明らかに同時に発火しないポリシの組み合わせのみを排除すべきである。仮に、インスタンスが同一かどうかわからない場合に同一と判断することとすると、同時に発火する可能性がポリシ記述の組み合わせを除外する可能性がある。このため、図５の検査、及び、図８の検査とは異なり、図７のステップＤ２０とステップＤ３０の間には、第２実施形態で説明した図１０に示す手順の制約追加動作を挿入することが好ましい。

本実施形態では、特に、不変条件と事後条件の検査（図５）、及び、２つのポリシ記述の事後条件と不変条件との検査（図８）で、論理式中に登場する束縛変数のうちで、対応する２つの束縛変数から参照されない束縛変数については、インスタンスが等しいとする制約を加える。このようにすることで、インスタンスが等しいか否かが明らかでない場合に、インスタンスが等しいと制約を与えることが可能であり、これより、問題がある可能性があるポリシ記述の組み合わせを広く検出することが可能となる。

本発明において、一階述語論理で記述される条件は、連接∧、選言∨、含意→、否定¬などの論理演算子と、“＜”、“＞”、“＝”などの数値や文字列の比較演算による述語、全称記号∀、存在記号∃、及び、ｘ∈Ｃｌａｓｓなどの束縛変数ｘがクラス名Ｃｌａｓｓのインスタンスに属することを示す∈という記号をＡＳＣＩＩ文字により表現した文字列により構成される。あるインスタンスの属性値を参照するためには、ｘ．ｐなどと記述する。ｘは束縛変数名で、ｐは当該束縛変数が属するインスタンスのクラスに定義された属性名である。

以下に説明する２つの条件を例に挙げて、充足判定を行う方法の概略を具体的に説明する。ここで述べる等価性制約の追加手法は、第２実施形態に準ずる。また、下記条件１を検査対象のポリシ記述に含まれる事後条件、下記条件２を不変条件として、その充足可能判定を行う場合について説明する。ＳｅｒｖｉｃｅというクラスのＫｅｙ属性は、Ｎａｍｅという名前の属性のみであるとする。
条件１：exists s in Service, s.Name="mysql" and s.Status="running"
条件２：exists s in Service, s.Name="mysql" and s.Status="stopped"

上記条件を∧結合し、冠頭標準形にした論理式を以下に示す。
exists s、t in Service,s.Name="mysql" and s.Status="running" and t.Name="mysql" and t.Status="stopped"
ここまでが、ステップＢ１０（図５）とステップＢ２０に対応する。論理式を冠頭標準形に変換する手順は広く知られている。

図１０に示す、Ｋｅｙ属性を用いた制約追加手続きを行う。論理式に登場するクラス名はＳｅｒｖｉｃｅのみである。論理式中に登場する束縛変数はｓとｔの２つであり、その組み合わせは（ｓ，ｔ）のみである。一方、ＳｅｒｖｉｃｅのＫｅｙ属性はＮａｍｅであり、これにより、以下に示す論理式が、ステップＦ９０で追加される制約となる。
（（ｓ．Ｎａｍｅ＝ｔ．Ｎａｍｅ）ｉｍｐｌｉｅｓ ｓ＝ｔ）

次に、充足判定手段１３が充足可能性判定ツールとしてシンプリファイ（simplify）を実装している場合の充足判定方法について説明する。シンプリファイを用いて充足判定するためには、インスタンスの属性値のアクセスを関数呼び出しに変換し、文字列は例えばハッシュ値をとり整数に変換し、論理式をＳ式で表現するなどの変換を行えばよい。更に、シンプリファイは、与えられた論理式の否定について充足可能性を判定するため、与える論理式をあらかじめ否定で反転しておく。

上記の例を、シンプリファイに与える論理式に変換したものを以下に示す。ここでは、ｍｙｓｑｌという文字列を１に、ｒｕｎｎｉｎｇを２に、ｓｔｏｐｐｅｄを３という整数に置き換えている。
(NOT (EXISTS (s t)
(AND
(AND
(AND (EQ (Service##Name s) 1)
(EQ (Service##Status s) 2))
(AND (EQ (Service##Name t) 1)
(EQ (Service##Status t) 3)))
(IFF
(EQ (Service##Name s) (Service##Name t))
(EQ s t)))))
上記論理式は、充足不可能であるため、シンプリファイではvalidという回答を出す。なお、充足可能である場合、又は、判定できない場合には、invalidという回答が返る。論理式の充足判定（ステップＢ４０）が完了し、充足不可能と判定されるため、ステップＢ５０に進んで、エラーが出力される。

以上、本発明をその好適な実施形態に基づいて説明したが、本発明のポリシ検査システム、方法、及び、プログラムは、上記実施形態にのみ限定されるものではなく、上記実施形態の構成から種々の修正及び変更を施したものも、本発明の範囲に含まれる。

本発明は、ポリシ記述を作成する際に、ポリシ記述の問題を検査するためのポリシ検査装置や、ポリシ検査装置をコンピュータに実現するためのプログラムといった用途に適用できる。また、ポリシ記述に従ってコンピュータ・システムやネットワーク・システムを管理するポリシ管理装置に組み込み、登録時に不適切なポリシ記述を検出・排除する機能としても適用可能である。

本発明の第１実施形態のポリシ検査システムの構成を示すブロック図。 ポリシ記述の構成を示すブロック図。 ポリシ仕様の構成を示すブロック図。 ポリシ検査システムの全体の動作の概略手順を示すフローチャート。 第１の検査手段による検査の動作手順を示すフローチャート。 第２の検査手段による検査の動作手順を示すフローチャート。 同時発火の可能性を判断するステップの動作手順の詳細を示すフローチャート。 実行可能か否かを判定するステップの動作手順の詳細を示すフローチャート。 本発明の第２実施形態のポリシ検査システムの構成を示すブロック図。 インスタンスの等価性制約を追加する処理の動作手順を示すフローチャート。 等価性制約の追加の処理の一部の動作手順を示すフローチャート。 非特許文献１に記載されたポリシ検査システムの構成を示すブロック図。 非特許文献２に記載されたポリシ検査システムの構成を示すブロック図。

符号の説明

１０：ポリシ検査システム
１１：第１の検査手段
１２：第２の検査手段
１３：充足判定手段
１４：入力装置
１５：出力装置
１６：記憶装置
１６１：不変条件記憶部
１６２：ポリシ記憶部
１６３：Ｋｅｙ属性記憶部
７１：ポリシ記述
７２：ポリシ仕様

Claims (13)

1. 検査対象のポリシ記述を検査するポリシ検査システムであって、
   前記検査対象のポリシ記述を受け付ける入力装置と、
   管理対象システムの状態について常に成立する条件を一階述語論理により記述した不変条件を記憶した不変条件記憶部と、
   登録済みのポリシ記述を記憶するポリシ記憶部と、
   前記入力装置により受け付けられた前記ポリシ記述中で定義されている操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した所定の論理式で表される事後条件と前記不変条件記憶部に記憶されている前記不変条件とに基づいて、前記入力装置により受け付けられた前記検査対象のポリシ記述の検査を行う検査手段と、を有し、
   前記検査手段が、
   論理式の充足判定を行う充足判定手段と、
   前記不変条件記憶部に記憶された不変条件及び前記ポリシ記憶部に記憶された登録済みのポリシ記述を参照し、前記入力装置により受け付けられた前記検査対象のポリシ記述に含まれる事後条件と前記登録済みポリシ記述に含まれる事後条件と前記不変条件とを∧結合した論理式を生成する論理式生成手段と、
   前記論理式生成手段が生成した論理式の充足可能性を、前記充足判定手段を用いて判定するポリシ整合性検査手段と、
   前記管理対象システムの状態を表現したインスタンスの属性のうち、管理対象システムのクラスに関し、同一クラス間で常に唯一の値をとるＫｅｙ属性の情報を記憶するＫｅｙ属性記憶部と、
   を有し、
   前記ポリシ整合性検査手段による判定に先立って、前記不変条件記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を、前記充足判定手段を用いて判定する不正ポリシ検査手段を更に備え、
   前記管理対象システムの状態はインスタンスによって表現され、
   前記不正ポリシ検査手段は、
   前記充足判定手段による充足性判定に先立って、前記Ｋｅｙ属性記憶部を参照し、前記管理対象システムの状態を表現したインスタンスのうち充足性判定の対象となる論理式に登場する束縛変数に対応付けられたインスタンスが等しいことを条件とする等価性制約を当該論理式に制約として加え、
   前記充足性判定の対象となる論理式に登場する２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、
   ことを特徴とするポリシ検査システム。
2. 前記ポリシ記述が、ポリシ発火条件を一階述語論理で記述した事前条件を更に含んでおり、
   前記ポリシ整合性検査手段は、前記不変条件記憶部及びポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事前条件と、前記登録済みポリシ記述に含まれる事前条件と、前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を、前記充足判定手段を用いて判定し、充足すると判定すると、前記検査対象のポリシ記述に含まれる事後条件と、前記登録済みポリシ記述に含まれる事後条件と、前記不変条件とを∧結合した論理式の充足可能性の判定を行う、請求項１に記載のポリシ検査システム。
3. 前記不正ポリシ検査手段は、
   前記充足性判定の対象となる論理式に登場する束縛変数のうちの任意の２つの組み合わせについて、当該論理式中に、前記任意の２つの束縛変数を用いて参照されるＫｅｙ属性が存在するか否かを判断し、存在しないと判断すると、前記任意の２つの束縛変数に対応するインスタンスが等しいとする等価性制約を前記充足性判定の対象となる論理式に加え、存在すると判断すると、前記任意の２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記任意の２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、請求項１又は２に記載のポリシ検査システム。
4. 前記ポリシ整合性検査手段は、
   前記充足性判定の対象となる論理式に登場する２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、請求項１、２又は３に記載のポリシ検査システム。
5. 前記ポリシ整合性検査手段は、
   前記充足性判定の対象となる論理式に登場する束縛変数のうちの任意の２つの組み合わせについて、当該論理式中に、前記任意の２つの束縛変数を用いて参照されるＫｅｙ属性が存在するか否かを判断し、存在しないと判断すると、前記任意の２つの束縛変数に対応するインスタンスが等しいとする等価性制約を前記充足性判定の対象となる論理式に加え、存在すると判断すると、前記任意の２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記任意の２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、請求項１〜４のいずれか１項に記載のポリシ検査システム。
6. 検査対象のポリシ記述を受け付ける入力装置と、管理対象システムの状態について常に成立する条件を一階述語論理により記述した不変条件を記憶した不変条件記憶部と、登録済みのポリシ記述を記憶するポリシ記憶部と、前記入力装置により受け付けられた前記ポリシ記述中で定義されている操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した所定の論理式で表される事後条件と前記不変条件記憶部に記憶されている前記不変条件とに基づいて、前記入力装置に受け付けられた前記検査対象のポリシ記述の検査を行う検査手段と、を有するコンピュータを用いて、検査対象のポリシ記述を検査するポリシ検査方法であって、
   前記コンピュータが、前記不変条件記憶部に記憶している不変条件と、前記入力装置により入力された前記ポリシ記述に定義された操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した論理式とに基づいて、前記検査対象のポリシ記述の検査を検査手段により行うステップを有し、
   前記ポリシ記述が、ポリシ記述に定義された操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した事後条件及びポリシ発火条件を一階述語論理で記述した事前条件を含んでおり、
   前記ポリシ記述の検査を行うステップが、
   前記コンピュータが、前記不変条件を記憶する前記不変条件記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と前記不変条件とを∧結合した論理式を生成するステップと、
   生成した論理式の充足可能性を判定する不正ポリシ検査ステップと、
   前記不正ポリシ検査ステップで充足すると判定すると、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事前条件と前記登録済みポリシ記述に含まれる事前条件と前記不変条件とを∧結合した論理式を生成するステップと、
   生成した論理式の充足可能性を判定するステップと、
   該判定するステップにおいて充足すると判定すると、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と前記登録済みポリシ記述に含まれる事後条件と前記不変条件とを∧結合した論理式を生成するステップと、
   生成した論理式の充足可能性を判定するポリシ整合性検査ステップと、
   を有し、
   前記ポリシ整合性検査ステップによる判定に先立って、前記不変条件記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を判定する不正ポリシ検査ステップを更に備え、
   前記不正ポリシ検査ステップが、前記論理式の充足性判定に先立って、前記コンピュータが、前記管理対象システムの状態を表現したインスタンスの属性のうち、同一クラス間で常に唯一の値をとるＫｅｙ属性の情報を記憶するＫｅｙ属性記憶部を参照し、充足性判定の対象となる論理式に登場する束縛変数に対応付けられたインスタンスが等しいことを条件とする等価性制約を当該論理式に制約として加えるステップを含み、
   前記制約を加えるステップでは、前記充足性判定の対象となる論理式に登場する２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、
   ことを特徴とするポリシ検査方法。
7. 前記制約を加えるステップでは、前記充足性判定の対象となる論理式に登場する束縛変数のうちの任意の２つの組み合わせについて、当該論理式中に、前記任意の２つの束縛変数を用いて参照されるＫｅｙ属性が存在するか否かを判断し、存在しないと判断すると、前記任意の２つの束縛変数に対応するインスタンスが等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、請求項６に記載のポリシ検査方法。
8. 前記ポリシ記述が、ポリシ記述に定義された操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した事後条件及びポリシ発火条件を一階述語論理で記述した事前条件を含んでおり、
   前記ポリシ記述の検査を行うステップが、
   前記コンピュータが、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事前条件と、前記登録済みポリシ記述に含まれる事前条件と、前記不変条件とを∧結合した論理式を生成し、前記管理対象システムの状態を表現したインスタンスの属性のうち、同一クラス間で常に唯一の値をとるＫｅｙ属性の情報を記憶するＫｅｙ属性記憶部を参照して、前記事前条件と不変条件とを∧結合して生成した論理式に登場する束縛変数に対応付けられたインスタンスが等しいことを条件とする等価性制約を当該論理式に制約として加え、該制約を加えた論理式の充足可能性を判定し、該充足性判定において充足すると判定すると、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と、前記登録済みポリシ記述に含まれる事後条件と、前記不変条件とを∧結合した論理式を生成し、前記管理対象システムの状態を表現したインスタンスの属性のうち、同一クラス間で常に唯一の値をとるＫｅｙ属性の情報を記憶するＫｅｙ属性記憶部を参照して、前記事後条件と不変条件とを∧結合して生成した論理式に登場する束縛変数に対応付けられたインスタンスが等しいことを条件とする等価性制約を当該論理式に制約として加え、該制約を加えた論理式の充足可能性を判定するポリシ整合性検査ステップを有し、
   前記ポリシ整合性検査ステップでは、論理式に制約を加える際に、前記充足性判定の対象となる論理式に登場する２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、請求項６又は７に記載のポリシ検査方法。
9. 前記ポリシ整合性検査ステップでは、前記事後条件と不変条件とを∧結合した論理式に登場する束縛変数のうちの任意の２つの組み合わせについて、当該論理式中に、前記任意の２つの束縛変数を用いて参照されるＫｅｙ属性が存在するか否かを判断し、存在しないと判断すると、前記任意の２つの束縛変数に対応するインスタンスが等しいとする等価性制約を当該論理式に加える、請求項８に記載のポリシ検査方法。
10. コンピュータに、検査対象のポリシ記述を検査する処理を実行させるプログラムであって、
    コンピュータを、検査対象のポリシ記述を受け付ける入力装置と、管理対象システムの状態について常に成立する条件を一階述語論理により記述した不変条件を記憶した不変条件記憶部と、登録済みのポリシ記述を記憶するポリシ記憶部と、前記入力装置により受け付けられた前記ポリシ記述中で定義されている操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した所定の論理式で表される事後条件と前記不変条件記憶部に記憶されている前記不変条件とに基づいて、前記入力装置で受け付けられた前記検査対象のポリシ記述の検査を行う検査手段と、として機能させ、
    前記コンピュータに、
    管理対象システムの状態について常に成立する条件を一階述語論理により記述した不変条件と、前記入力装置により入力された前記ポリシ記述に定義された操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した論理式とに基づいて、前記検査対象のポリシ記述の検査を前記検査手段により行うステップを実行させるプログラムであって、
    前記ポリシ記述が、ポリシ記述に定義された操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した事後条件及びポリシ発火条件を一階述語論理で記述した事前条件を含んでおり、
    前記ポリシ記述の検査を行うステップが、
    前記不変条件記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と、前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を判定する不正ポリシ検査ステップと、
    前記不正ポリシ検査ステップで充足すると判定すると、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事前条件と、前記登録済みポリシ記述に含まれる事前条件と、前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を判定し、該判定において充足すると判定すると、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と、前記登録済みポリシ記述に含まれる事後条件と、前記不変条件とを∧結合した論理式を生成し、該生成した論理式の充足可能性を判定するポリシ整合性検査ステップとを実行させ、
    前記不正ポリシ検査ステップが、
    前記論理式の充足性判定に先立って、前記管理対象システムの状態を表現したインスタンスの属性のうち、同一クラス間で常に唯一の値をとるＫｅｙ属性の情報を記憶するＫｅｙ属性記憶部を参照し、充足性判定の対象となる論理式に登場する束縛変数に対応付けられたインスタンスが等しいことを条件とする等価性制約を当該論理式に制約として加えるステップを含み、
    前記制約を加えるステップでは、前記充足性判定の対象となる論理式に登場する２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、
    ことを特徴とするプログラム。
11. 前記制約を加えるステップでは、前記充足性判定の対象となる論理式に登場する束縛変数のうちの任意の２つの組み合わせについて、当該論理式中に、前記任意の２つの束縛変数を用いて参照されるＫｅｙ属性が存在するか否かを判断し、存在しないと判断すると、前記任意の２つの束縛変数に対応するインスタンスが等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、請求項１０に記載のプログラム。
12. 前記ポリシ記述が、ポリシ記述に定義された操作の直後に管理対象システムの状態について成立すべき条件を一階述語論理により記述した事後条件及びポリシ発火条件を一階述語論理で記述した事前条件を含んでおり、
    前記ポリシ記述の検査を行うステップが、
    前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事前条件と、前記登録済みポリシ記述に含まれる事前条件と、前記不変条件とを∧結合した論理式を生成し、前記管理対象システムの状態を表現したインスタンスの属性のうち、同一クラス間で常に唯一の値をとるＫｅｙ属性の情報を記憶するＫｅｙ属性記憶部を参照して、前記事前条件と不変条件とを∧結合して生成した論理式に登場する束縛変数に対応付けられたインスタンスが等しいことを条件とする等価性制約を当該論理式に制約として加え、該制約を加えた論理式の充足可能性を判定し、該充足性判定において充足すると判定すると、前記不変条件記憶部及び前記ポリシ記憶部を参照し、前記検査対象のポリシ記述に含まれる事後条件と、前記登録済みポリシ記述に含まれる事後条件と、前記不変条件とを∧結合した論理式を生成し、前記管理対象システムの状態を表現したインスタンスの属性のうち、同一クラス間で常に唯一の値をとるＫｅｙ属性の情報を記憶するＫｅｙ属性記憶部を参照して、前記事後条件と不変条件とを∧結合して生成した論理式に登場する束縛変数に対応付けられたインスタンスが等しいことを条件とする等価性制約を当該論理式に制約として加え、該制約を加えた論理式の充足可能性を判定するポリシ整合性検査ステップを有し、
    前記ポリシ整合性検査ステップでは、論理式に制約を加える際に、前記充足性判定の対象となる論理式に登場する２つの束縛変数の全てのＫｅｙ属性の値が等しいとき該２つの束縛変数に対応するインスタンスが等しく、かつ、前記２つの束縛変数が等しいとき該２つの束縛変数の全てのＫｅｙ属性の値が等しいとする等価性制約を前記充足性判定の対象となる論理式に加える、請求項１０又は１１に記載のプログラム。
13. 前記ポリシ整合性検査ステップでは、前記事後条件と不変条件とを∧結合した論理式に登場する束縛変数のうちの任意の２つの組み合わせについて、当該論理式中に、前記任意の２つの束縛変数を用いて参照されるＫｅｙ属性が存在するか否かを判断し、存在しないと判断すると、前記任意の２つの束縛変数に対応するインスタンスが等しいとする等価性制約を当該論理式に加える、請求項１２に記載のプログラム。

Images