(57)【要約】【課題】不特定の入力元から入力されうるプログラムを対象として、プログラムが特定の状態に到達する可能性があるか判定可能とする。【解決手段】解析装置は、遷移解析部と、判定部と、を備える。遷移解析部は、評価対象のプログラムを解析し、プログラムに対する第１入力元からの入力により遷移する状態間の関係を示す第１遷移情報と、プログラムに対する第２入力元からの入力により遷移する状態間の関係を示す第２遷移情報とを求める。判定部は、第１遷移情報と第２遷移情報とに基づいて、第１入力元および第２入力元の両方からの入力によりプログラムが特定の状態に達するか否かを判定する。【選択図】図４
2018156159.tif 000002
【特許請求の範囲】
【請求項１】
評価対象のプログラムを解析し、前記プログラムに対する第１入力元からの入力により遷移する状態間の関係を示す第１遷移情報と、前記プログラムに対する第２入力元からの入力により遷移する状態間の関係を示す第２遷移情報とを求める遷移解析部と、
前記第１遷移情報と前記第２遷移情報とに基づいて、前記第１入力元および前記第２入力元の両方からの入力により前記プログラムが特定の状態に達するか否かを判定する判定部と、
を備える解析装置。
【請求項２】
前記判定部は、
前記第１遷移情報に基づいて、指定された遷移先の状態に前記第１入力元からの入力により到達する遷移元の状態を算出する第１算出部と、
前記第２遷移情報に基づいて、前記第２入力元からの任意の入力に対して、前記第１算出部により算出された状態が遷移先となる遷移元の状態を算出する第２算出部と、を備え、
前記特定の状態を最初の遷移先の状態に指定し、前記第２算出部により算出された状態を新たな遷移先の状態に指定して、前記第１算出部および前記第２算出部による算出処理を繰り返し、前記第２算出部により算出された状態が初期状態になるか否かにより、前記プログラムが前記特定の状態に達するか否かを判定する、
請求項１に記載の解析装置。
【請求項３】
前記判定部は、前記第１遷移情報と、前記第２遷移情報と、前記第２入力元からの複数の入力の順序を定めたシナリオ情報とに基づいて、前記第１入力元からの入力、および、前記シナリオ情報で定められる順序に従う前記第２入力元からの入力の両方が入力されることにより前記プログラムが前記特定の状態に達するか否かを判定する、
請求項１に記載の解析装置。
【請求項４】
前記判定部は、
前記第１遷移情報に基づいて、指定された遷移元の状態から前記第１入力元からの入力により到達する遷移先の状態を算出する第１算出部と、
前記第２遷移情報に基づいて、前記第１算出部により算出された状態を遷移元に指定し、前記シナリオ情報に従う順序で入力される前記第２入力元からの入力により遷移する遷移先の状態を算出する第２算出部と、を備え、
初期状態を最初の遷移元の状態に指定し、前記第２算出部により算出された状態を新たな遷移元の状態に指定して、前記第１算出部および前記第２算出部による算出処理を繰り返し、前記第１算出部により算出された状態が前記特定の状態に達するか否かにより、前記プログラムが前記特定の状態に達するか否かを判定する、
請求項３に記載の解析装置。
【請求項５】
前記判定部は、
前記第１遷移情報に基づいて、指定された遷移先の状態に前記第１入力元からの入力により到達する遷移元の状態を算出する第１算出部と、
前記第２遷移情報に基づいて、前記第１算出部により算出された状態を遷移先に指定し、前記シナリオ情報に従う順序で入力される前記第２入力元からの入力により遷移する遷移元の状態を算出する第２算出部と、を備え、
前記特定の状態を最初の遷移先の状態に指定し、前記第２算出部により算出された状態を新たな遷移先の状態に指定して、前記第１算出部および前記第２算出部による算出処理を繰り返し、前記第１算出部により算出された状態が初期状態になるか否かにより、前記プログラムが特定の状態に達するか否かを判定する、
請求項３に記載の解析装置。
【請求項６】
前記第１入力元および前記第２入力元は、ユーザ、センサ、および、プログラムのうち少なくとも１つである、
請求項１に記載の解析装置。
【請求項７】
評価対象のプログラムを解析し、前記プログラムに対する第１入力元からの入力により遷移する状態間の関係を示す第１遷移情報と、前記プログラムに対する第２入力元からの入力により遷移する状態間の関係を示す第２遷移情報とを求める遷移解析ステップと、
前記第１遷移情報と前記第２遷移情報とに基づいて、前記第１入力元および前記第２入力元の両方からの入力により前記プログラムが特定の状態に達するか否かを判定する判定ステップと、
を含む解析方法。
【請求項８】
コンピュータを、
評価対象のプログラムを解析し、前記プログラムに対する第１入力元からの入力により遷移する状態間の関係を示す第１遷移情報と、前記プログラムに対する第２入力元からの入力により遷移する状態間の関係を示す第２遷移情報とを求める遷移解析部と、
前記第１遷移情報と前記第２遷移情報とに基づいて、前記第１入力元および前記第２入力元の両方からの入力により前記プログラムが特定の状態に達するか否かを判定する判定部と、
として機能させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明の実施形態は、解析装置、解析方法およびプログラムに関する。
【背景技術】
【０００２】
スマートコントラクト（Smart  Contract）と呼ばれる技術が提案されている。スマートコントラクトとは、概念的には、履行を自動化する仕組みを伴った電子的な契約を意味する。実態としては、スマートコントラクトは、分散台帳（ブロックチェーン）上に構築されたプログラム実行環境で動作するアプリケーション（プログラム）を指す。スマートコントラクトは、インターネット上のパブリックな環境で、不特定多数のユーザが利用可能なプログラムとして動作させることもできる。
【０００３】
スマートコントラクトに問題（脆弱性）があると金銭的な被害を受ける場合がある。このため、利用開始前にそのプログラムが無害であるかを確認できることが望ましい。プログラムの解析方法としては、実際にプログラムを動作させることなくその性質を解析する静的解析技術などが知られている。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特許第５３３７４５４号公報
【非特許文献】
【０００５】
【非特許文献１】Karthikeyan  Bhargavan,  et.al.,  “Formal  Verification  of  Smart  Contracts”,  Microsoft,  2016.8.11
【非特許文献２】Roderick  Bloem,  Barbara  Jobstmann,  Nir  Piterman,  Amir  Pnueli,  Yaniv  Sa'ar,  “Synthesis  of  Reactive(1)  designs”,  Journal  of  Computer  and  System  Sciences,  Volume  78,  Issue  3,  May  2012,  Pages  911-938,  ISSN  0022-0000.
【発明の概要】
【発明が解決しようとする課題】
【０００６】
しかしながら、従来技術では、立場の異なるユーザなどのように、異なる入力元からプログラムに対する入力が行われることが考慮されていなかった。このため、例えば、不特定多数のユーザが利用可能なプログラムを対象として、特定のユーザ（ユーザのグループ）が不利益を被る可能性について判定できない場合があった。
【課題を解決するための手段】
【０００７】
実施形態の解析装置は、遷移解析部と、判定部と、を備える。遷移解析部は、評価対象のプログラムを解析し、プログラムに対する第１入力元からの入力により遷移する状態間の関係を示す第１遷移情報と、プログラムに対する第２入力元からの入力により遷移する状態間の関係を示す第２遷移情報とを求める。判定部は、第１遷移情報と第２遷移情報とに基づいて、第１入力元および第２入力元の両方からの入力によりプログラムが特定の状態に達するか否かを判定する。
【図面の簡単な説明】
【０００８】
【図１】評価対象プログラムへの入力を決めてテストを行う場合の状態遷移図。
【図２】実施形態の解析方法を行う場合の状態遷移図。
【図３】状態遷移を状態の集合による表現に置き換えた図。
【図４】第１の実施形態にかかる解析装置のブロック図。
【図５】敵対者状態算出部の算出処理を説明するための図。
【図６】協力者状態算出部の算出処理を説明するための図。
【図７】第１の実施形態の解析処理のフローチャート。
【図８】第１の実施形態の遷移解析処理のフローチャート。
【図９】第１の実施形態の状態算出処理のフローチャート。
【図１０】第１の実施形態の集合算出処理のフローチャート。
【図１１】第１の実施形態の判定処理のフローチャート。
【図１２】第２の実施形態にかかる解析装置のブロック図。
【図１３】第２の実施形態の状態算出処理のフローチャート。
【図１４】第２の実施形態の集合算出処理のフローチャート。
【図１５】第２の実施形態の判定処理のフローチャート。
【図１６】第１または第２の実施形態にかかる解析装置のハードウェア構成図。
【発明を実施するための形態】
【０００９】
以下に添付図面を参照して、この発明にかかる解析装置、解析方法およびプログラムの好適な実施形態を詳細に説明する。
【００１０】
以下の実施形態にかかる解析装置は、不特定多数のユーザ（マルチユーザ）が利用可能なプログラムなども対象として、特定のユーザが不利益を被る可能性について判定可能とする。実施形態にかかる解析装置は、ユーザがプログラムの利用を開始する前に使うことができる。また、プログラムの開発者が、そのプログラムの検証ツール（仕様と成果物の不整合を発見するためのツール）として用いることもできる。
【００１１】
なお、プログラムの障害の原因は様々である。例えば、意図的でない偶然の事象やサイバー攻撃などが障害の原因になりうる。また、プログラムの不具合の原因も様々である。単なる誤りや意図的に作りこまれた罠などが不具合の原因になりうる。プログラムが仕様を満足している場合、従って通常の意味では不具合を有さない場合であっても、ユーザにとっては不都合となる場合もある。例えば、仕様がユーザにとって不利な場合、および、ユーザが使用方法を誤解しやすい場合などが該当する。
【００１２】
（用語の定義）
以下に、各実施形態で用いる用語の定義を記載する。
・協力者、敵対者、ユーザ種別：
評価対象とするプログラム（評価対象プログラム）を利用するユーザのうち、特定のユーザ（または特定のユーザのグループ）など、特定のユーザに協力するユーザ（ユーザのグループ）を協力者と呼ぶ。協力者以外のユーザ（ユーザのグループ）を敵対者と呼ぶ。また、協力者であるか敵対者であるかを示す情報をユーザ種別と呼ぶ。敵対者は、例えば意図的にサイバー攻撃をしかける悪意のあるユーザのみでなく、悪意はないユーザなども含む。ユーザとは、評価対象プログラムにその入力となるデータを与える存在（入力元）、または、評価対象プログラムの機能を呼び出して利用する存在を指す。主として評価対象プログラムを利用する人間がユーザとして想定される。それ以外にも、解析装置の外部に設置されたセンサ、および、評価対象プログラムの機能を呼び出す他のプログラムをユーザの一種とみなすことが可能である。
【００１３】
・評価条件：
評価対象プログラムの良否を判定する基準とするための条件式を評価条件と呼ぶ。評価条件は、例えば協力者によるプログラムの利用が終了した後で成立しているべき条件を表す。なお、協力者による操作終了後に確実に評価条件を満足させられるなら、途中で一時的に評価条件を満たさない状態を経ても構わない。従って、評価条件は、形式検証における安全特性（Safety  Property）の概念とは異なる。なお、安全特性は常に成立せねばならない。
【００１４】
・想定シナリオ：
協力者が評価対象プログラムの利用において想定する操作手順（入力の順序）を想定シナリオと呼ぶ。例えば想定シナリオは、協力者による複数のファンクション呼び出しの列である。それぞれのファンクション呼び出しは、ファンクションの種類、引数、および、呼び出したユーザを示す情報である。
【００１５】
・像計算、逆像計算：
状態機械の遷移関係が与えられたとき、（時間順通りに）遷移前の状態の集合から遷移後の状態の集合を計算することを像計算（Image  Computation）と呼ぶ。時間順とは逆に、遷移後から遷移前の方向に計算することを逆像計算（Preimage  Computation）と呼ぶ。以下では像計算と逆像計算を区別しないで、単に像計算と呼ぶことがある。
【００１６】
・敵対者により到達可能：
敵対者から評価対象プログラムへの０回以上任意回の入力によって生じる遷移によって状態ｓから状態ｔへ到達する可能性があるとき、状態ｓから状態ｔへ敵対者により到達可能という。数式で書くと、以下の（１）式を満たすｋ≧０およびｐ（０）、ｐ（１）、・・・、ｐ（ｋ）が存在することが、敵対者により到達可能であることを意味する。なお、ｓ＝ｔの場合もこの条件を満たしていると考える。ｐは状態、ｕはユーザ、ｉは入力、ｏは出力（ファンクションの戻り値、例外処理の結果など）、Ａは、評価対象プログラムの遷移関係のうち、敵対者からの入力によって引き起こされる遷移に対応するものを表す。
ｐ（０）＝ｓ，ｐ（ｋ）＝ｔ，∃（ｕ，ｉ，ｏ）：（ｐ（ｊ），ｕ，ｉ，ｐ（ｊ＋１），ｏ）∈Ａ  ・・・（１）
【００１７】
・協力者にとって不可避−想定シナリオが与えられている場合（第２の実施形態）：
評価対象プログラムの状態ｓと状態の集合Ｔについて、協力者から評価対象プログラムへの任意の入力に対し、状態ｓからの１回の遷移によって集合Ｔに属するある状態ｔに到達する可能性があるとき、状態ｓから集合Ｔへの到達は協力者にとって不可避という。協力者にとって不可避とは、言い換えると、評価対象プログラムが集合Ｔに属する状態へ遷移するのを協力者が回避しようとしても、回避を保証できるような入力は存在しないことを意味する。想定シナリオが与えられている場合、協力者による想定シナリオによって各回の入力は固定なので、上記定義のうち「任意の入力」の部分は「想定シナリオの範囲内の任意の入力」と解釈する。
【００１８】
ｋ回目の入力で想定されるユーザｕ（ｋ）および入力ｉ（ｋ）が決まっているならば、状態ｓから集合Ｔに含まれる状態ｔへの到達が協力者にとって不可避とは、以下の（２）式が成り立つことを意味する。なお、ｋは０≦ｋ≦ｎを満たす整数であり、ｎは想定シナリオ内の入力（操作）の個数である。Ｐは、評価対象プログラムの遷移関係のうち、協力者からの入力によって引き起こされる遷移に対応するものを表す。
∃（ｔ，ｏ）：［（ｓ，ｕ（ｋ），ｉ（ｋ），ｔ，ｏ）∈Ｐ∧ｔ∈Ｔ］  ・・・（２）
【００１９】
・協力者にとって不可避−協力者による想定シナリオが与えられていない場合（第１の実施形態）：
想定シナリオが与えられていない場合、協力者は各回の入力において（想定シナリオが与えられている場合と同様に）ユーザと入力の組み合わせを一つ選択すること、または、入力を打ち切る（以降の入力を評価対象プログラムに与えない）ことを選択することができる。状態ｓが集合Ｔに属していなければ、入力の打ち切りによって集合Ｔに属する状態への遷移を回避できる。従って、協力者にとって不可避という概念を適用するのは、状態ｓが集合Ｔに属する場合に限定して構わない。そのため、想定シナリオが与えられていない場合の「協力者にとって不可避」は次のように定義できる。
【００２０】
すなわち、評価対象プログラムの状態ｓと状態の集合Ｔについて、状態ｓが集合Ｔに属しており、かつ、協力者から評価対象プログラムへの任意の入力に対し、状態ｓからの１回の遷移によって集合Ｔに属するある状態ｔに到達する可能性があるとき、状態ｓから集合Ｔへの到達は協力者にとって不可避という。
【００２１】
状態ｓから集合Ｔに含まれる状態ｔへの到達が協力者にとって不可避とは、以下の（３）式が成り立つことを意味する。
ｓ∈Ｔ∧∀ｉ：∃（ｕ，ｔ，ｏ）：［（ｓ，ｕ，ｉ，ｔ，ｏ）∈Ｐ∧ｔ∈Ｔ］  ・・・（３）
【００２２】
（解析方法の概要）
次に、実施形態によるプログラムの解析方法の概要について説明する。実施形態では、評価対象プログラムが評価条件を満たさない状態に到達することを協力者が回避できるか否かが判定される。まず評価対象プログラムの静的解析などにより、ファンクション呼び出しによって引き起こされる状態遷移を列挙した遷移関係が作成される。その際に、ファンクションを呼び出したユーザのユーザ種別に応じて、協力者によって生じる遷移と敵対者による遷移が区別される。次に到達可能性の判定が行われる。協力者による入力の前後には敵対者の任意回の入力が割り込みうる。区別された敵対者の遷移関係および協力者の遷移関係が交互に用いられ、評価条件を満たさない状態に達するか否かが判定される。
【００２３】
図１は、評価対象プログラムへの入力を決めてテスト（シミュレーション）を行うように構成した場合の状態遷移の例を示す図である。図１に示すように、このような方法では、評価対象プログラムの初期状態から開始し、事前に決められた敵対者または協力者からの入力に従い状態を遷移させ、最後に到達した状態が評価条件を満たさない状態であるかが判定される。このような方法では、事前に決められた特定の入力についてしか良否を判定できない。そこで、以下の実施形態では網羅的な判定ができるようにする。
【００２４】
図２は、以下の実施形態の解析方法を行う場合の状態遷移の例を示す図である。図２に示すように、実施形態では、「敵対者による０回以上任意回の入力」と「協力者による１回の入力」が繰り返される。なお最後は敵対者による入力が行われる。また、協力者は、評価条件を満たさない状態への到達を確実に回避可能な入力を選択することを前提とする。実施形態では、このような前提の下で、評価条件を満たさない状態に到達する可能性があるか否かが判定される。
【００２５】
図３は、図２の状態遷移を状態の集合による表現に置き換えた例を示す図である。図３の例では、以下のようなＶ（０），Ｖ（１），・・・，Ｖ（２ｎ＋１）が存在するか否かが判定される。なおｎは０以上の整数である。
・Ｖ（０）は初期状態ｗのみを含む集合を表す。すなわちＶ（０）＝｛ｗ｝である。
・Ｖ（２ｋ＋１）に属する任意の状態ｔに対し、Ｖ（２ｋ）に属する状態ｓが存在して、状態ｓから状態ｔへ敵対者により到達可能である。なお、この場合のｋは０以上ｎ以下の整数である。
・Ｖ（２ｋ＋１）に属する任意の状態からＶ（２ｋ＋２）への到達は協力者にとって不可避である。なお、この場合のｋは０以上（ｎ−１）以下の整数である。
・Ｖ（２ｎ＋１）は空集合でなく、かつ、Ｖ（２ｎ＋１）に属する状態はすべて評価条件を満たさない。すなわち、以下の（４）式が真になる。ただし、想定シナリオが固定長の場合は、その固定長に相当する特定のｎで判定し、そうでない場合は、（４）式を満たすｎが存在するか判定する。ｖは評価条件を表す。
［Ｖ（２ｎ＋１）≠O］∧［∀ｓ∈Ｖ（２ｎ＋１）：¬ｖ（ｓ）］・・・（４）
【００２６】
集合の列Ｖ（０），Ｖ（１），・・・，Ｖ（２ｎ＋１）が存在するならば、協力者がｎ回の入力をどのように決めても、それらに敵対者からの入力が混じることで、協力者からの入力が終了した後に評価対象プログラムが評価条件を満たさない状態に達する可能性があることを意味する。
【００２７】
実施形態では、Ｖ（０），Ｖ（１），・・・，Ｖ（２ｎ＋１）の存在を判定する方法として像計算を使う。具体的には、時間順通りの像計算のみを用いる場合、時間順とは逆の逆像計算のみを用いる場合、またはそれらの組み合わせなどがありうる。第１の実施形態では逆像計算を、第２の実施形態では像計算を使う例を挙げる。
【００２８】
各実施形態によれば、評価対象プログラムに対して協力者によるどのような入力の系列に対しても、敵対者からの入力の系列が存在して、評価対象プログラムが評価条件を満たさない状態に到達するか否かということを判定できる。それにより、評価対象プログラムを利用することが協力者にとって不利な状態をもたらす可能性があるか否かを判定可能となる。
【００２９】
（第１の実施形態）
第１の実施形態では、想定シナリオを指定せず、逆像計算をベースに判定処理が実行される。図４は、第１の実施形態にかかる解析装置１００の構成の一例を示すブロック図である。図４に示すように、解析装置１００は、条件記憶部１２１と、対象記憶部１２２と、ユーザ種別記憶部１２３と、初期状態記憶部１２４と、遷移記憶部１２５、１２６と、状態記憶部１２７、１２８と、結果記憶部１２９と、遷移解析部１０１と、不利状態算出部１０２と、判定部１１０と、を備えている。
【００３０】
条件記憶部１２１は、評価条件を記憶する。対象記憶部１２２は、評価対象プログラムを記憶する。評価対象プログラムは、解析可能な形式であればどのようなデータ形式で記憶されてもよい。例えば条件記憶部１２１は、評価対象プログラムのソースコード、または、バイナリ形式の評価対象プログラムを記憶する。
【００３１】
ユーザ種別記憶部１２３は、ユーザを協力者と敵対者に区別するための情報を記憶する。例えばユーザ種別記憶部１２３は、ユーザを識別する識別情報と、ユーザ種別と、を対応づけて記憶する。ユーザ種別は、例えば、協力者であるか、敵対者であるかを示す情報である。協力者と敵対者の区別が自明の場合は、ユーザ種別記憶部１２３は備えなくてもよい。例えば、解析装置１００のユーザが唯一の協力者であり、他のユーザを敵対者とみなす場合が該当する。
【００３２】
初期状態記憶部１２４は、評価対象プログラムの初期状態を記憶する。評価対象プログラムの意味および処理系の仕様などから初期状態が明らかである場合は、初期状態記憶部１２４は備えなくてもよい。
【００３３】
遷移記憶部１２５、１２６は、遷移解析部１０１により解析された遷移関係を示す遷移情報を記憶する。遷移記憶部１２５は、敵対者（第１入力元）からの入力により遷移する状態間の関係を示す遷移情報（第１遷移情報）を記憶する。遷移記憶部１２６は、協力者（第２入力元）からの入力により遷移する状態間の関係を示す遷移情報（第２遷移情報）を記憶する。遷移情報を区別して記憶する方法はこれに限られるものではなく、ユーザ種別に応じて遷移関係を区別できる方法であれば任意の方法を適用できる。例えば、同一の記憶部の中でフラグなどの情報によって遷移情報を区別することにしてもよい。
【００３４】
状態記憶部１２７、１２８は、判定部１１０などにより求められる、プログラムの状態を示す情報を記憶する。状態記憶部１２７は、協力者からの入力により遷移する状態の集合を示す情報を記憶する。状態記憶部１２８は、敵対者からの入力により遷移する状態の集合を示す情報を記憶する。
【００３５】
結果記憶部１２９は、判定部１１０による判定（評価）の結果を記憶する。
【００３６】
各記憶部（条件記憶部１２１、対象記憶部１２２、ユーザ種別記憶部１２３、初期状態記憶部１２４、遷移記憶部１２５、１２６、状態記憶部１２７、１２８、結果記憶部１２９など）は、ＨＤＤ（Hard  Disk  Drive）、光ディスク、メモリカード、ＲＡＭ（Random  Access  Memory）などの一般的に利用されているあらゆる記憶媒体により構成することができる。また、各記憶部の一部または全部は、物理的に同一の記憶媒体により構成してもよい。記憶部それぞれは、物理的に複数の記憶媒体に構成してもよい。
【００３７】
遷移解析部１０１は、評価対象のプログラムを解析する。遷移解析部１０１は、例えば、評価対象プログラムに対する敵対者からの入力により遷移する状態間の関係を示す遷移情報と、協力者からの入力により遷移する状態間の関係を示す遷移情報とを求め、遷移記憶部１２５、１２６に記憶する。
【００３８】
不利状態算出部１０２は、協力者が到達するか判定する対象となる状態である不利状態を算出する。例えば不利状態算出部１０２は、評価条件ｖを満たさない状態ｓの集合を求め、求めた状態ｓを状態記憶部１２７に記憶する。
【００３９】
判定部１１０は、遷移解析部１０１により求められた遷移情報などを参照して、プログラムが特定の状態（不利状態など）に達するか否かを判定する。例えば判定部１１０は、遷移記憶部１２５、１２６にそれぞれ記憶された遷移情報に基づいて、敵対者および協力者の両方からの入力によりプログラムが特定の状態（不利状態など）に達するか否かを判定する。判定部１１０は、敵対者状態算出部１１１（第１算出部）と、協力者状態算出部１１２（第２算出部）と、を備えている。
【００４０】
敵対者状態算出部１１１は、敵対者により到達可能という関係に基づいて逆像計算を行う。敵対者状態算出部１１１は、例えば、敵対者（第１入力元）からの入力により遷移する状態間の関係を示す遷移情報（第１遷移情報）に基づいて、指定された遷移先の状態に敵対者からの入力により到達する遷移元の状態を算出する。
【００４１】
逆像計算の場合は、敵対者状態算出部１１１は、評価対象プログラムの状態の集合Ｔを入力し、集合Ｔに属するある状態ｔについて状態ｓから状態ｔへ敵対者により到達可能という条件を満たす状態ｓをすべて求め、状態ｓの集合を出力する。数式で表すと、以下の（５）式を満たす集合Ｓのうち最小の集合を求めることに相当する。
Ｓ＝Ｔ∪｛ｓ｜∃（ｕ，ｉ，ｓ'，ｏ）：（ｓ，ｕ，ｉ，ｓ'，ｏ）∈Ａかつｓ'∈Ｓ｝・・・（５）
【００４２】
協力者状態算出部１１２は、協力者にとって不可避という関係に基づいて逆像計算を行う。協力者状態算出部１１２は、例えば、協力者（第２入力元）からの入力により遷移する状態間の関係を示す遷移情報（第２遷移情報）に基づいて、協力者からの任意の入力に対して、敵対者状態算出部１１１により算出された状態が遷移先となる遷移元の状態を算出する。
【００４３】
逆像計算の場合、協力者状態算出部１１２は、状態の集合Ｔを入力して、状態ｓから集合Ｔへの到達が協力者にとって不可避であるような状態ｓをすべて求め、求めた状態ｓの集合Ｓを出力する。なお、この条件を満たす集合Ｓは一意である。想定シナリオが与えられていない場合の逆像計算は以下の（６）式で表される。
Ｓ＝Ｔ∩｛ｓ｜∀（ｉ，ｕ）：∃（ｔ，ｏ）：［ｕが協力者ならば、（ｓ，ｕ，ｉ，ｔ，ｏ）∈Ｐかつｔ∈Ｔ］｝・・・（６）
【００４４】
なお、（５）式および（６）式などの計算は、例えばＢＤＤ（Binary  Decision  Diagram）などの従来から用いられている任意の方法を適用できる。
【００４５】
ここで、敵対者状態算出部１１１および協力者状態算出部１１２の違いについて説明する。図５は、敵対者状態算出部１１１の算出処理を説明するための図である。図６は、協力者状態算出部１１２の算出処理を説明するための図である。
【００４６】
図５に示すように、敵対者状態算出部１１１には、状態の集合５０１（集合Ｔ）が入力される。敵対者状態算出部１１１は、集合５０１に含まれる状態へ敵対者により到達可能な状態の集合５０２（集合Ｓ）を算出する。
【００４７】
図６に示すように、協力者状態算出部１１２には、状態の集合６０１（集合Ｔ）が入力される。協力者状態算出部１１２は、集合６０１に含まれる状態に１回の遷移によって到達する可能性がある状態（集合６０１への遷移が不可避な状態）の集合６０２（集合Ｓ）を算出する。図６の状態６０３は、評価対象プログラムへの入力によっては、集合６０１への遷移を回避可能な状態を表す。
【００４８】
判定部１１０は、敵対者状態算出部１１１および協力者状態算出部１１２による算出処理を繰り返すことにより、プログラムが特定の状態（不利状態など）に達するか否かを判定する。例えば判定部１１０は、不利状態を最初の遷移先の状態に指定し、その後に協力者状態算出部１１２により算出された状態を新たな遷移先の状態に指定して、敵対者状態算出部１１１および協力者状態算出部１１２による算出処理を繰り返す。そして判定部１１０は、協力者状態算出部１１２により算出された状態が初期状態になるか否かにより、プログラムが不利状態に達するか否かを判定する。
【００４９】
逆像計算を使う場合は次のように判定できる。まず、次のような集合の列Ｗ（・）がＷ（２ｎ＋１），Ｗ（２ｎ），・・・，Ｗ（０）という順に求められる。評価条件を満たさないすべての状態の集合をＷ（２ｎ＋１）とし、以下の逆像計算が繰り返され、Ｗ（０）が求められる。
・Ｗ（２ｋ＋１）から敵対者状態算出部１１１によりＷ（２ｋ）を計算する。
・Ｗ（２ｋ）から協力者状態算出部１１２によりＷ（２ｋ−１）を計算する。
【００５０】
得られたＷ（０）に評価対象プログラムの初期状態が含まれているならば、Ｖ（０），Ｖ（１），・・・，Ｖ（２ｎ＋１）が存在する。具体的には、Ｖ（０）＝｛ｗ｝，ｋ≧１についてＶ（２ｋ）＝Ｗ（２ｋ），Ｖ（２ｋ＋１）はＶ（ｋ）から敵対者により到達可能なすべての状態の集合、とすれば、Ｖ（０），Ｖ（１），・・・，Ｖ（２ｎ＋１）についての条件が満たされる。
【００５１】
なお、想定シナリオが与えられていないときはｎが事前に分からないが、敵対者状態算出部１１１と協力者状態算出部１１２の定義によりＷ（２ｋ−２）⊆Ｗ（２ｋ）となるから、逆像計算によってｋが減少する順に計算することを考慮すると、どこかでＷ（２ｊ−２）＝Ｗ（２ｊ）となることが分かる。そのようなＷ（２ｊ）をＷ（０）と読み替えればよい。
【００５２】
上記各部（遷移解析部、不利状態算出部、および、判定部）は、例えば、１または複数のプロセッサにより実現される。例えば上記各部は、ＣＰＵ（Central  Processing  Unit）などのプロセッサにプログラムを実行させること、すなわちソフトウェアにより実現してもよい。上記各部は、専用のＩＣ（Integrated  Circuit）などのプロセッサ、すなわちハードウェアにより実現してもよい。上記各部は、ソフトウェアおよびハードウェアを併用して実現してもよい。複数のプロセッサを用いる場合、各プロセッサは、各部のうち１つを実現してもよいし、各部のうち２以上を実現してもよい。
【００５３】
次に、このように構成された第１の実施形態にかかる解析装置１００による解析処理について図７を用いて説明する。図７は、第１の実施形態における解析処理の一例を示すフローチャートである。
【００５４】
まず、遷移解析部１０１は、評価対象のプログラムを解析して状態間の遷移関係を求める遷移解析処理を実行する（ステップＳ１０１）。判定部１１０（敵対者状態算出部１１１、協力者状態算出部１１２）は、逆像計算により状態の集合を求める状態算出処理を実行する（ステップＳ１０２）。判定部１１０は、状態算出処理の結果を用いてプログラムが特定の状態に達するか判定する判定処理を実行する（ステップＳ１０３）。以下、遷移解析処理、状態算出処理、および、判定処理の詳細について説明する。
【００５５】
図８は、遷移解析処理の一例を示すフローチャートである。遷移解析部１０１は、対象記憶部１２２から評価対象プログラムを読み出し、評価対象プログラムに含まれているファンクションを列挙する（ステップＳ２０１）。また遷移解析部１０１は、各ファンクションの引数、返り値のデータ型、および、処理内容の情報などを取り出す。
【００５６】
遷移解析部１０１は、例えば記号実行によって、すべての状態ｓとすべてのユーザｕ、および、すべての入力ｉについて、遷移先の状態ｓ'と出力ｏを求め、それらの組である（ｓ，ｕ，ｉ，ｓ'，ｏ）を得る（ステップＳ２０２）。入力ｉは、例えば“ファンクションの種類”および“ファンクションの引数”を組にしたデータである。
【００５７】
すべての組み合わせを網羅しても、論理式やＢＤＤを利用することで、メモリ上にコンパクトに格納できる。ユーザｕは入力の一部ともみなすこともできるが、本実施形態ではユーザｕのユーザ種別（協力者、敵対者）に応じた処理を含む点が従来技術とは異なっている。
【００５８】
遷移解析部１０１は、得られたデータの組（ｓ，ｕ，ｉ，ｓ'，ｏ）を、呼び出したユーザのユーザ種別に応じて、遷移記憶部１２５または遷移記憶部１２６に記憶する（ステップＳ２０３）。
【００５９】
図９は、状態算出処理の一例を示すフローチャートである。状態算出処理では、状態記憶部１２７の内容Ｂと状態記憶部１２８の内容Ｂ'とが交互に更新される。前者がＷ（２ｋ＋１）に相当し、後者がＷ（２ｋ）に相当する。
【００６０】
まず、不利状態算出部１０２は、評価条件ｖを満たさない状態ｓの集合を求め、求めた状態ｓの集合Ｂを状態記憶部１２７に記憶する（ステップＳ３０１）。例えば不利状態算出部１０２は、以下の（７）式を実行して集合Ｂを求める。Ｓは評価対象プログラムのすべての状態の集合、ｖは評価条件を表す。
Ｂ：＝｛ｓ∈Ｓ｜¬ｖ（ｓ）｝・・・（７）
【００６１】
敵対者状態算出部１１１は、状態ｓ'から集合Ｂ内のいずれかの状態ｓに敵対者による０回以上任意回の操作によって到達可能であるような状態ｓ'の集合Ｂ'を求め状態記憶部１２８に記憶する（ステップＳ３０２）。集合Ｂ'は、例えば以下の（８）式を満たす最小の解として算出される。集合Ｂは状態記憶部１２８の現在の内容、Ａは遷移記憶部１２５の内容である。ステップＳ３０２の詳細については後述する。
Ｂ'＝Ｂ∪｛ｓ｜∃（ｕ，ｉ，ｓ'，ｏ）：［（ｓ，ｕ，ｉ，ｓ'，ｏ）∈Ａかつｓ'∈Ｂ'］｝・・・（８）
【００６２】
協力者状態算出部１１２は、協力者による１回の操作においてどのような入力ｉを選択しても、その入力ｉによる遷移先がＢ'に属する可能性を排除できないような遷移元の状態ｓの集合Ｂ''を求める。すなわち、協力者状態算出部１１２は、状態ｓから集合Ｂ'への遷移が協力者にとって不可避であるような状態ｓの集合Ｂ''を算出する（ステップＳ３０３）。例えば協力者状態算出部１１２は、以下の（９）式を実行して集合Ｂ''を求める。Ｂ'は敵対者状態算出部１１１の出力、Ｐは遷移記憶部１２６の内容を表す。
Ｂ''：＝Ｂ'∩｛ｓ｜∀（ｉ，ｕ）：∃（ｓ'，ｏ）：［ｕが協力者ならば、（ｓ，ｕ，ｉ，ｓ'，ｏ）∈Ｐかつｓ'∈Ｂ'］｝・・・（９）
【００６３】
次に協力者状態算出部１１２は、Ｂ＝Ｂ''が満たされるか否かを判定する（ステップＳ３０４）。Ｂ＝Ｂ''でない場合（ステップＳ３０４：Ｎｏ）、協力者状態算出部１１２は、集合Ｂ''を集合Ｂに代入する、すなわち、集合Ｂ''を新たな集合Ｂとして状態記憶部１２８に記憶する（ステップＳ３０５）。その後、ステップＳ３０２に戻り処理が繰り返される。
【００６４】
Ｂ＝Ｂ''を満たす場合（ステップＳ３０４：Ｙｅｓ）、判定部１１０は、状態算出処理を終了する。
【００６５】
図１０は、ステップＳ３０２の集合算出処理の一例を示すフローチャートである。敵対者状態算出部１１１は、集合Ｂを集合Ｂ'''に代入する（ステップＳ４０１）。敵対者状態算出部１１１は、以下の（１０）式により、集合Ｂ'を算出する（ステップＳ４０２）。
Ｂ'：＝Ｂ'''∪｛ｓ｜∃（ｕ，ｉ，ｓ'，ｏ）：［（ｓ，ｕ，ｉ，ｓ'，ｏ）∈Ａかつｓ'∈Ｂ'''］｝・・・（１０）
【００６６】
敵対者状態算出部１１１は、Ｂ'＝Ｂ'''が満たされるか否かを判定する（ステップＳ４０３）。Ｂ'＝Ｂ'''でない場合（ステップＳ４０３：Ｎｏ）、敵対者状態算出部１１１は、集合Ｂ'を集合Ｂ'''に代入する、すなわち、集合Ｂ'を新たな集合Ｂ'''として状態記憶部１２７に記憶する（ステップＳ４０４）。その後、ステップＳ４０２に戻り処理が繰り返される。Ｂ'＝Ｂ'''を満たす場合（ステップＳ４０３：Ｙｅｓ）、敵対者状態算出部１１１は、集合算出処理を終了する。
【００６７】
図１１は、判定処理の一例を示すフローチャートである。判定部１１０は、状態算出処理により算出された集合Ｂ'に、初期状態ｗが含まれるか否か（ｗ∈Ｂ'を満たすか）を判定する（ステップＳ５０１）。集合Ｂ'に初期状態ｗが含まれる場合（ステップＳ５０１：Ｙｅｓ）、判定部１１０は、評価条件を満たさない状態に到達する可能性があることを示す判定結果を結果記憶部１２９に記憶する（ステップＳ５０２）。集合Ｂ'に初期状態ｗが含まれる場合は、協力者がどのような操作をしても、評価条件を満たさない状態に到達する可能性が残されることを意味する。
【００６８】
集合Ｂ'に初期状態ｗが含まれない場合（ステップＳ５０１：Ｎｏ）、判定部１１０は、評価条件を満たさない状態に到達する可能性がないことを示す判定結果を結果記憶部１２９に記憶する（ステップＳ５０３）。集合Ｂ'に初期状態ｗが含まれない場合は、敵対者がどのような操作をしても、あるシナリオが存在して、協力者がそのシナリオに従っていれば評価条件を満たす状態に必ず到達し、協力者による操作の終了後も評価条件を満たす状態の間のみを遷移する。
【００６９】
このように、第１の実施形態にかかる解析装置では、協力者による想定シナリオを指定しなくても、協力者にとって有利なシナリオが存在するか否かを判定できる。すなわち、ある入力の系列が存在して、その系列に従って協力者が評価対象プログラムに入力を与えれば、敵対者からの入力に関わらず、必ず評価条件を満たす状態に到達させられるか否かを判定することができる。逆に、そのような入力の系列が存在しない場合は、敵対者からの入力によっては協力者にとって不利な状況になる可能性があり、協力者の努力のみではその可能性を排除することができないことが判定できる。第１の実施形態では、評価対象プログラムについてこのような判定が可能となる。
【００７０】
（第２の実施形態）
第２の実施形態では、想定シナリオが与えられ、像計算を行う場合の例を説明する。図１２は、第２の実施形態にかかる解析装置１００−２の構成の一例を示すブロック図である。図１２に示すように、解析装置１００−２は、条件記憶部１２１と、対象記憶部１２２と、ユーザ種別記憶部１２３と、初期状態記憶部１２４と、遷移記憶部１２５、１２６と、状態記憶部１２７、１２８と、結果記憶部１２９と、シナリオ記憶部１３０−２と、遷移解析部１０１と、判定部１１０−２と、を備えている。
【００７１】
第２の実施形態では、不利状態算出部１０２を削除したこと、シナリオ記憶部１３０−２を追加したこと、および、判定部１１０−２の機能が第１の実施形態と異なっている。その他の構成および機能は、第１の実施形態にかかる解析装置１００のブロック図である図４と同様であるので、同一符号を付し、ここでの説明は省略する。
【００７２】
シナリオ記憶部１３０−２は、想定シナリオを示す情報（シナリオ情報）を記憶する。
【００７３】
判定部１１０−２は、シナリオ記憶部１３０−２に記憶された想定シナリオを用いて、像計算により、プログラムが特定の状態（不利状態など）に達するか否かを判定する。例えば判定部１１０−２は、遷移記憶部１２５、１２６にそれぞれ記憶された遷移情報、および、想定シナリオに基づいて、想定シナリオで定められる順序に従う協力者からの入力、および、敵対者からの入力の両方が入力されることによりプログラムが特定の状態（不利状態など）に達するか否かを判定する。判定部１１０−２は、敵対者状態算出部１１１−２と、協力者状態算出部１１２−２と、を備えている。
【００７４】
敵対者状態算出部１１１−２は、敵対者により到達可能という関係に基づいて像計算を行う。敵対者状態算出部１１１−２は、例えば、敵対者（第１入力元）からの入力により遷移する状態間の関係を示す遷移情報（第１遷移情報）に基づいて、指定された遷移元の状態から、敵対者からの入力により到達する遷移先の状態を算出する。
【００７５】
像計算の場合は、敵対者状態算出部１１１−２は、評価対象プログラムの状態の集合Ｓを入力し、集合Ｓに属する状態ｓから敵対者により到達可能な状態ｓ'をすべて求めて、状態ｓ'の集合Ｔを出力する。数式で表すと、以下の（１１）式を満たす集合Ｔのうち最小の集合を求めることに相当する。
Ｔ＝Ｓ∪｛ｓ'｜∃（ｕ，ｉ，ｓ，ｏ）：（ｓ，ｕ，ｉ，ｓ'，ｏ）∈Ａかつｓ∈Ｔ｝・・・（１１）
【００７６】
協力者状態算出部１１２−２は、協力者にとって不可避という関係に基づいて像計算を行う。協力者状態算出部１１２−２は、例えば、協力者（第２入力元）からの入力により遷移する状態間の関係を示す遷移情報（第２遷移情報）に基づいて、敵対者状態算出部１１１−２により算出された状態を遷移元に指定し、想定シナリオに従う順序で入力される協力者からの入力により遷移する遷移先の状態を算出する。
【００７７】
像計算の場合、協力者状態算出部１１２−２は、状態の集合Ｓを入力して、集合Ｓに属する任意の状態ｓから協力者によって不可避な集合Ｔを出力する。そのような集合Ｔは一般には一意ではないが、協力者状態算出部１１２−２は、例えばそのうちの一つを出力する。例えば協力者状態算出部１１２−２は、想定シナリオのｋ番目の入力の集合Ｉ（ｋ）として、集合Ｓに属する任意の状態ｓから協力者による１回の遷移で到達可能な状態の集合Ｔを、以下の（１２）式により算出する。
Ｔ＝｛ｔ｜∀ｉ∈Ｉ（ｋ）：∃（ｓ，ｕ，ｉ，ｏ）：（ｓ，ｕ，ｉ，ｔ，ｏ）∈Ｐかつｓ∈Ｓ｝・・・（１２）
【００７８】
判定部１１０−２は、敵対者状態算出部１１１−２および協力者状態算出部１１２−２による算出処理を繰り返すことにより、プログラムが特定の状態（不利状態など）に達するか否かを判定する。例えば判定部１１０−２は、初期状態を最初の遷移元の状態に指定し、その後に協力者状態算出部１１２−２により算出された状態を新たな遷移元の状態に指定して、敵対者状態算出部１１１−２および協力者状態算出部１１２−２による算出処理を繰り返す。そして判定部１１０−２は、敵対者状態算出部１１１−２により算出された状態が特定の状態に達するか否かにより、プログラムが特定の状態に達するか否かを判定する。
【００７９】
本実施形態では、協力者によるプログラムへの入力のシナリオ（想定シナリオ）が固定とされるため、計算量の削減が可能となる。また本実施形態によれば、協力者が想定シナリオの実行中および実行後に敵対者が任意の操作を行っても、想定シナリオの終了後には必ず評価条件が満たされていることを保証できるか否かが判定できる。第１の実施形態のように逆像計算を利用することも可能である。この場合は、例えば特定の状態（不利状態など）と初期状態とを入れ替えて、以下の手順を適用すればよい。
【００８０】
次に、このように構成された第２の実施形態にかかる解析装置１００−２による各処理について説明する。解析処理の全体の流れ、および、遷移解析処理は第１の実施形態（図７、図８）と同様であるため説明を省略する。本実施形態では、状態算出処理および判定処理が第１の実施形態と異なっている。以下、本実施形態の状態算出処理および判定処理について説明する。
【００８１】
図１３は、第２の実施形態における状態算出処理の一例を示すフローチャートである。
【００８２】
判定部１１０−２は、まず状態記憶部１２７を初期化する。例えば判定部１１０−２は、初期状態ｗのみを含む集合Ｂを状態記憶部１２７に記憶する（ステップＳ６０１）。また判定部１１０−２は、想定シナリオを読み出すためのカウンタｋを０で初期化する。ｋは、１からｎまでの想定シナリオの入力ｉ（ｋ）とユーザｕ（ｋ）をシナリオ記憶部１３０−２から順に読み出すためのカウンタである。ただし、入力ｉ（ｋ）は想定シナリオにおける評価対象プログラムへのｋ番目の入力、ｕ（ｋ）は入力ｉ（ｋ）を与えるユーザ（協力者のうちのいずれか）である。
【００８３】
敵対者状態算出部１１１−２は、集合Ｂの中のいずれかの状態ｓから敵対者により到達可能な状態ｓ’（すなわち、敵対者からの０回以上任意回の入力によって到達しうる状態ｓ'）の集合Ｂ'を求め状態記憶部１２８に記憶する（ステップＳ６０２）。集合Ｂ'は、例えば以下の（１３）式を満たす最小の解として算出される。ステップＳ６０２の詳細については後述する。
Ｂ'＝Ｂ∪｛ｓ'｜∃（ｓ，ｕ，ｉ，ｏ）：［（ｓ，ｕ，ｉ，ｓ'，ｏ）∈Ａかつｓ∈Ｂ'］｝・・・（１３）
【００８４】
協力者状態算出部１１２−２は、シナリオ記憶部１３０−２から、次の入力ｉ（ｋ）を取得する（ステップＳ６０３）。協力者状態算出部１１２−２は、集合Ｂ'に属する状態ｓから入力ｉ（ｋ）による遷移で到達可能な状態ｓ'の集合Ｂを算出する（ステップＳ６０４）。例えば協力者状態算出部１１２−２は、以下の（１４）式を実行して集合Ｂ'を求める。集合Ｂ'は状態記憶部１２８の内容、Ｐは遷移記憶部１２６の内容、ｉ（ｋ）はシナリオ記憶部１３０−２から読み出したｋ番目の入力である。
Ｂ'＝｛ｓ'｜∃（ｓ，ｏ）：［（ｓ，ｕ（ｋ），ｉ（ｋ），ｓ'，ｏ）∈Ｐかつｓ∈Ｂ'］｝・・・（１４）
【００８５】
第１の実施形態の（９）式との違いは、ｉがｉ（ｋ）に変わり、ｕがｕ（ｋ）に変わり、∀（ｉ，ｕ）が不要になること、および、時間順が逆であることである。全称量化子∀がなくなるとＳＡＴ（SATisfiability  problem）ソルバをより容易に適用できるようになり、実装の手間が省けるとともに高速に解けることが期待できる。
【００８６】
なお、理論的には、存在量化子∃のみからなる式の充足可能性問題はＳＡＴ問題と呼ばれ、ＮＰ完全であるが、ソルバが高機能化されるに従い高速に解くことが可能となっている。一方、存在量化子∃と全称量化子∀の両方が混在する式の場合はＱＢＦ（Quantified  Boolean  Formulas）問題と呼ばれ、ＳＡＴ問題よりも解くのが難しくなる。ＱＢＦ問題は、例えば空間計算量についてはＰＳＰＡＣＥ完全であり、時間計算量については量化子の個数について指数的である。
【００８７】
判定部１１０−２は、すべての入力ｉ（ｋ）を処理したか否か、すなわち、ｋがｎに達したか否かを判定する（ステップＳ６０５）。すべての入力ｉ（ｋ）を処理していない場合は、ステップＳ６０２に戻り処理が繰り返される。すべての入力ｉ（ｋ）を処理した場合、状態算出処理が終了する。
【００８８】
図１４は、ステップＳ６０２の集合算出処理の一例を示すフローチャートである。敵対者状態算出部１１１−２は、集合Ｂを集合Ｂ'''に代入する（ステップＳ７０１）。敵対者状態算出部１１１−２は、以下の（１５）式により、集合Ｂ'を算出する（ステップＳ７０２）。
Ｂ'：＝Ｂ'''∪｛ｓ'｜∃（ｓ，ｕ，ｉ，ｏ）：［（ｓ，ｕ，ｉ，ｓ'，ｏ）∈Ａかつｓ∈Ｂ'''］｝・・・（１５）
【００８９】
敵対者状態算出部１１１−２は、Ｂ'＝Ｂ'''が満たされるか否かを判定する（ステップＳ７０３）。Ｂ'＝Ｂ'''でない場合（ステップＳ７０３：Ｎｏ）、敵対者状態算出部１１１−２は、集合Ｂ'を集合Ｂ'''に代入する、すなわち、集合Ｂ'を新たな集合Ｂ'''として状態記憶部１２７に記憶する（ステップＳ７０４）。その後、ステップＳ７０２に戻り処理が繰り返される。Ｂ'＝Ｂ'''を満たす場合（ステップＳ７０３：Ｙｅｓ）、敵対者状態算出部１１１−２は、集合算出処理を終了する。
【００９０】
図１５は、判定処理の一例を示すフローチャートである。判定部１１０−２は、状態算出処理により算出された集合Ｂ'に、評価条件ｖを満たさない状態が含まれるか否かを判定（∃ｓ∈Ｂ'｜¬ｖ（ｓ）を計算）する（ステップＳ８０１）。集合Ｂ'に評価条件ｖを満たさない状態が含まれる場合（ステップＳ８０１：Ｙｅｓ）、判定部１１０−２は、評価条件を満たさない状態に到達する可能性があることを示す判定結果を結果記憶部１２９に記憶する（ステップＳ８０２）。そのような状態が存在するならば、協力者による想定シナリオに敵対者の操作が混じることによって、協力者にとって不都合な状態に到達しうることを意味する。
【００９１】
集合Ｂ'に評価条件ｖを満たさない状態が含まれない場合（ステップＳ８０１：Ｎｏ）、判定部１１０−２は、評価条件を満たさない状態に到達する可能性がないことを示す判定結果を結果記憶部１２９に記憶する（ステップＳ８０３）。
【００９２】
第２の実施形態では、協力者による想定シナリオに敵対者の任意の操作が混じっても、想定シナリオの終了後に評価条件を必ず満たすか否かを判定できる。想定シナリオ（協力者によるプログラムへの入力のシナリオ）を固定したことにより、第１の実施形態と比較して協力者状態算出部で列挙すべき入力の組み合わせが減り、状態集合の大きさが小さくなる。このため処理全体の計算量を減らすことができる。また、第１の実施形態と異なり、全称量化子∀を含まない計算とすることができるため、ＳＡＴソルバやＳＭＴソルバを利用しやすくなり、実装の容易化や、処理の高速化が可能となる。
【００９３】
以上説明したとおり、第１から第２の実施形態によれば、不特定の入力元から入力されうるプログラムを対象として、プログラムが特定の状態（不利な状態など）に到達する可能性があるか否かを判定可能となる。
【００９４】
次に、第１または第２の実施形態にかかる解析装置のハードウェア構成について図１６を用いて説明する。図１６は、第１または第２の実施形態にかかる解析装置のハードウェア構成例を示す説明図である。
【００９５】
第１または第２の実施形態にかかる解析装置は、ＣＰＵ（Central  Processing  Unit）５１などの制御装置と、ＲＯＭ（Read  Only  Memory）５２やＲＡＭ（Random  Access  Memory）５３などの記憶装置と、ネットワークに接続して通信を行う通信Ｉ／Ｆ５４と、各部を接続するバス６１を備えている。
【００９６】
第１または第２の実施形態にかかる解析装置で実行されるプログラムは、ＲＯＭ５２等に予め組み込まれて提供される。
【００９７】
第１または第２の実施形態にかかる解析装置で実行されるプログラムは、インストール可能な形式又は実行可能な形式のファイルでＣＤ−ＲＯＭ（Compact  Disk  Read  Only  Memory）、フレキシブルディスク（ＦＤ）、ＣＤ−Ｒ（Compact  Disk  Recordable）、ＤＶＤ（Digital  Versatile  Disk）等のコンピュータで読み取り可能な記録媒体に記録してコンピュータプログラムプロダクトとして提供されるように構成してもよい。
【００９８】
さらに、第１または第２の実施形態にかかる解析装置で実行されるプログラムを、インターネット等のネットワークに接続されたコンピュータ上に格納し、ネットワーク経由でダウンロードさせることにより提供するように構成してもよい。また、第１または第２の実施形態にかかる解析装置で実行されるプログラムをインターネット等のネットワーク経由で提供または配布するように構成してもよい。
【００９９】
第１または第２の実施形態にかかる解析装置で実行されるプログラムは、コンピュータを上述した解析装置の各部として機能させうる。このコンピュータは、ＣＰＵ５１がコンピュータ読取可能な記憶媒体からプログラムを主記憶装置上に読み出して実行することができる。
【０１００】
第１または第２の実施形態にかかる解析装置は、物理的に１つの装置（サーバ装置、パーソナルコンピュータなど）として実現しもよいし、複数の物理的な装置により構成される論理的な装置により実現してもよい。第１または第２の実施形態にかかる解析装置は、クラウド環境上に構築された仮想計算機などにより実現してもよい。
【０１０１】
本発明のいくつかの実施形態を説明したが、これらの実施形態は、例として提示したものであり、発明の範囲を限定することは意図していない。これら新規な実施形態は、その他の様々な形態で実施されることが可能であり、発明の要旨を逸脱しない範囲で、種々の省略、置き換え、変更を行うことができる。これら実施形態やその変形は、発明の範囲や要旨に含まれるとともに、特許請求の範囲に記載された発明とその均等の範囲に含まれる。
【符号の説明】
【０１０２】
１００、１００−２  解析装置
１０１  遷移解析部
１０２  不利状態算出部
１１０、１１０−２  判定部
１１１、１１１−２  敵対者状態算出部
１１２、１１２−２  協力者状態算出部
１２１  条件記憶部
１２２  対象記憶部
１２３  ユーザ種別記憶部
１２４  初期状態記憶部
１２５、１２６  遷移記憶部
１２７、１２８  状態記憶部
１２９  結果記憶部
１３０−２  シナリオ記憶部
【図１】
2018156159.tif 000003
【図２】
2018156159.tif 000004
【図３】
2018156159.tif 000005
【図４】
2018156159.tif 000006
【図５】
2018156159.tif 000007
【図６】
2018156159.tif 000008
【図７】
2018156159.tif 000009
【図８】
2018156159.tif 000010
【図９】
2018156159.tif 000011
【図１０】
2018156159.tif 000012
【図１１】
2018156159.tif 000013
【図１２】
2018156159.tif 000014
【図１３】
2018156159.tif 000015
【図１４】
2018156159.tif 000016
【図１５】
2018156159.tif 000017
【図１６】
2018156159.tif 000018