(57)【要約】【課題】  ウェブアプリケーションを検証するシンボリック実行を提供する。【解決手段】  １つ以上のウェブアプリケーション用のシンボリック文字列操作クラスライブラリが作成される。操作群は文字列操作シンボリック代数内に統合される。また、１つ以上のウェブアプリケーションに関してシンボリック実行が行われる。典型的に、シンボリック実行を行う際に一定種類の要求又はプロパティを検査するよう、Ｊａｖａモデルチェッカが拡張される。エラーシナリオが存在する場合、一組のシンボリック制約に対する解が取得され、この解は、エラートレース及びテストケースを取得するためソースコードにマッピングされる。要求又はプロパティはテンプレートを介して符号化されてもよく、パブリックドメインの決定手続きを用いて検査され得る。要求又はプロパティはセキュリティ検証に関するものとし得る。シンボリック実行はＪａｖａベースのウェブアプリケーション用に調整され得る。【選択図】  図１
2009087355.tif 000002
【特許請求の範囲】
【請求項１】
１つ以上のウェブアプリケーション用のシンボリック文字列操作ライブラリの一組のクラスを作り出す生成段階であり、操作群を文字列操作シンボリック代数内に統合する生成段階；及び
前記ウェブアプリケーションのうちの１つ以上への要求又はプロパティを検証するために、シンボリック実行に基づくモデル検査を行う実行段階；
を有する方法。
【請求項２】
前記文字列操作シンボリック代数を用いてシンボリック実行を行うことによって一定の種類の要求又はプロパティを検査するよう、状態に基づくＪａｖａ（登録商標）モデルチェッカが拡張される、請求項１記載の方法。
【請求項３】
連結、切り捨て、及び大文字／小文字変換を含み得る一連の可能性ある文字列操作をコンパイルするよう、相異なるウェブアプリケーションが評価される、請求項１記載の方法。
【請求項４】
エラーシナリオが存在する場合、一組のシンボリック制約に対する解が取得され、且つ前記解は、エラートレースと該エラーを発見しない具体的なテストケースとを取得するため、アプリケーションのソースコードにマッピングされる、請求項１記載の方法。
【請求項５】
エラーシナリオが存在しない場合、前記要求は検証されたことを示される、請求項１記載の方法。
【請求項６】
シンボリック文字列、シンボリック整数、浮動小数点数、及びブール値を含むシンボリックモデルを生成するよう、当初のアプリケーションモデルが自動コード計装によって変形される、請求項１記載の方法。
【請求項７】
前記計装は静的解析及び関連性解析技術によって制限される、請求項６記載の方法。
【請求項８】
前記計装は、ヒープ、スタック、アレイ又はリストを含むデータ構造のシンボリックモデルを生成する、請求項６記載の方法。
【請求項９】
プログラムパス条件が伝統的なデータ型のシンボリック方程式によって表され、且つ状態に基づくモデルチェッカの有限状態機械によって表されたシンボリック文字列と組み合わされる、請求項１記載の方法。
【請求項１０】
入力文字列に基づく要求又はプロパティが、プログラムポイントにおけるシンボリック文字列を表す有限状態機械を、該要求に従った許容されないシンボリック文字列を表す一組の有限状態機械で分けることによって検査される、請求項１記載の方法。
【請求項１１】
シンボリック実行に基づくモデル検査によって検査可能な一組の要求又はプロパティが特定される、請求項１記載の方法。
【請求項１２】
要求又はプロパティはテンプレートを介して符号化され、パブリックドメインの決定手続きを用いて検査される、請求項１記載の方法。
【請求項１３】
アプリケーションプログラムについてのシンボリック解析が代数及びモデルを用いて実行される、請求項１記載の方法。
【請求項１４】
ウェブアプリケーションについての前記要求又はプロパティはセキュリティ検証に関する、請求項１記載の方法。
【請求項１５】
シンボリック実行エンジンはＪａｖａ（登録商標）ベースのウェブアプリケーション用にカスタマイズされ且つ調整される、請求項１記載の方法。
【請求項１６】
コンピュータ読み取り可能な記録媒体に記録されたプログラムであって：
１つ以上のウェブアプリケーション用のシンボリック文字列操作ライブラリの一組のクラスを作り出す生成段階であり、操作群を文字列操作シンボリック代数内に統合する生成段階；及び
前記ウェブアプリケーションのうちの１つ以上への要求又はプロパティを検証するために、シンボリック実行に基づくモデル検査を行う実行段階；
を行わせるプログラム。
【請求項１７】
１つ以上のウェブアプリケーション用のシンボリック文字列操作ライブラリの一組のクラスを作り出す、シンボリック実行に基づくＪａｖａ（登録商標）モデルチェッカであり、
操作群を文字列操作シンボリック代数内に統合し；且つ
前記ウェブアプリケーションのうちの１つ以上への要求又はプロパティを検証するために、シンボリック実行に基づくモデル検査を実行する；
モデルチェッカ、を有するシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、概してウェブアプリケーションの分野に関し、より具体的にはウェブアプリケーションの機能を検証するシンボリック実行エンジンを提供するシステム及び方法に関する。
【背景技術】
【０００２】
一般的に、ソフトウェアアプリケーションは、該ソフトウェアに改修が行われる都度、一連の回帰試験が手動で、あるいは自動的に実行される試験を介して検証される。このような試験技術は、通常、対象とする被試験アプリケーションの機能的範囲に乏しく、更には時間のかかるものである。これらの問題を解決するため、ソフトウェアシステムを検証する代替技術として、形式的検証（formal  verification）技術が浮上してきている。このような検証ツールは、ソフトウェアアプリケーションに関する具体的な要件の充足可能性を数学的に立証すること、又は、要件を破るテストケースの形式の反例を得て、それによりバグを指摘することを試みる。
【０００３】
ソフトウェアの検証で用いられる形式的検証システムは、一般的に、その内部証明エンジンとして状態に基づくモデルチェッカを使用する。チェッカは、検査中のアプリケーションを供給するドライバへの非決定論的なユーザ入力を必要とする。このようなチェッカは入力スペース全体について論理的に考えることができない。例えば、整数や文字列などの全範囲に及ぶ場合、このようなチェッカは、ドライバにおいて指定される、可能性あるシナリオを評価できるに過ぎない。
【０００４】
シンボリック実行は、上述のものとは異なり、ステートレスなモデル検査である。これは、プログラムへの全ての入力を記号として扱い、該プログラム内の全ての可能性あるパスを実行することによって複素方程式群を作成する。そして、これらの方程式は、エラーシナリオが存在する場合にはそれを取得する（決定手続きと呼ばれる）ソルバによって解かれる。これまで、シンボリック実行は、大抵のウェブアプリケーションを創作するために使用されるＪａｖａ（登録商標）プログラムにおける、整数、浮動小数点数、及びブール代数のようなプリミティブ型を扱うことにおいてのみ成功していた。しかしながら、ウェブアプリケーションの場合、殆どの入力及びプリミティブ型は文字列である。従って、文字列をシンボリック実行代数にてモデル化することが必要である。また、性能上の理由から、リスト、マップ、セット等のようなウェブアプリケーションで頻繁に使用されるデータ構造をシンボリックにモデル化することが必要となり得る。
【０００５】
故に、ウェブアプリケーションにおける検証問題を解決することは興味深い課題を生じさせる。全てのこのような処理作業と同様に、高速性、正確性及び自動化に関する問題も非常に重要である。
【発明の開示】
【発明が解決しようとする課題】
【０００６】
本発明は、従来の方法及びシステムに関する欠点及び問題点の少なくとも一部を抑制あるいは実質的に排除し得る、ウェブアプリケーション用のシンボリック実行エンジンを実現する方法及びシステムを提供することを目的とする。
【課題を解決するための手段】
【０００７】
本発明の特定の一実施形態に従って、１つ以上のウェブアプリケーション用のシンボリック文字列操作群を作り出すことを含む方法が提供される。これら操作群は文字列操作シンボリック代数（algebra）内に統合される。この方法はまた、ウェブアプリケーションにおいて存在する整数又はブール値のようなその他のプリミティブデータ型についての統合されたシンボリック実行を行うことを含む。典型的に、シンボリック実行を行いながら一定の種類のプロパティを検査するよう、Ｊａｖａ（登録商標）モデルチェッカが拡張される。エラーシナリオが存在する場合、一組のシンボリック制約に対する解が取得され、この解は、エラートレースを取得するため、ソースコードにマッピングされる。
【０００８】
特定の実施形態において、シンボリック実行型のモデル検査によって検査可能な一組のプロパティが特定され、それにより、プロパティはテンプレートを介して符号化され、第三者からの既製の決定手続きを用いて検査される。検査されるプロパティはセキュリティ検証に関するものとし得る。また、シンボリック実行は、様々な種類のＪａｖａ（登録商標）ベースのウェブアプリケーション用にカスタマイズされ、調整され得る。
【発明の効果】
【０００９】
本発明の特定の実施形態の技術的効果は、１）入力ドメイン及び可能なプログラム実行パスの全体にわたって網羅的な検査が行われる；２）ドライバにおいてユーザ入力を生成することが不要になる；３）予期されないエラー／挙動をも発見することができる；４）バグが存在する場合にそれを発見するために、検査データの自動生成が利用可能である；ことを含む。
【００１０】
本発明のその他の技術的効果は、以下の記載と、添付の図面及び特許請求の範囲とから当業者に明らかになるであろう。また、ここでは具体的な効果を列挙したが、実施形態は様々であり、列挙された効果の全て又は一部を含むこともあるし、それらの何れをも含まないこともあり得る。
【発明を実施するための最良の形態】
【００１１】
本発明の特定の実施形態及びその効果を、より完全な理解のため、添付の図面を参照しながら説明する。
【００１２】
図１は、本発明の一実施形態に関するモデルチェッカ及びシンボリック実行システムライブラリ１０を例示する簡易ブロック図である。アプリケーションコードを変更し、シンボリック実行を容易にするシンボリックモデル２４を作り出すコード・インスツルメンタが設けられる。図１は、Ｊａｖａ（登録商標）モデルチェッカ１４、一組のユースケース（use  case）１６、アプリケーション２２、モデルジェネレータ２０、アプリケーションモデル１８、要求／プロパティ指定ツール２８（図１においては‘要求’と略す）、及びソルバとして使用される決定手続きソルバ２６を含んでいる。決定手続きソルバ２６は既製品とし得る。
【００１３】
本発明の例示的な実施形態の教示に従って、ここで提示されるアーキテクチャは、ウェブアプリケーション用に調整された新たなシンボリック実行エンジンを作り出す。以前には特定することが不可能であった一定の種類の要求／プロパティを検査することには、既製の部品（例えば、Ｊａｖａ（登録商標）モデルチェッカ１４及び決定手続きソルバ２６）が使用され得る。
【００１４】
図２は、シンボリック実行エンジンのアーキテクチャ全体を例示するトップレベルブロック図である。システムは、ユーザが指定したユースケース及び単純なデータ入力を有する単純なドライバを用いて作り出されたアプリケーションモデルのプログラム３０を入力とする。このモデルは、環境生成プロセスによって作り出すことができる。このアプリケーションモデルは自動の統合コード・インスツルメンタ３２によって修正される。このとき、インスツルメンタ３２は、ドライバにて指定された幾つかのシンボリックデータ型を考慮に入れるようにモデルを修正する。インスツルメンタ３２は、整数又はブール値のようなプリミティブデータ型だけでなく、ウェブアプリケーションドメインで重要な文字列をも扱うことができる。計装（インスツルメンテーション）段階は静的解析モジュール３４の助けを借りる。このモジュールは、ドライバ内の記号値を流れ込ませ得る正確なコードセクションを指摘するため、アプリケーションモデルについてのおおまかな関連性解析を実行する。アプリケーションモデルのこれらのセクションのみが計装され、故に、コード修正は最小に留められる。
【００１５】
その結果、この計装されたコードのシンボリック実行は、より良好な性能を有することが可能であるとともに、より少ない計算資源のみを必要とする。計装段階はウェブアプリケーションのシンボリックモデル３６を作り出す。認識されるべきことには、相異なるウェブアプリケーションがプリミティブデータ型での一連の可能性あるシンボリック操作関数をコンパイルするために調査され得る。本発明のこの実施形態においては、例えば連結、切り捨て、大文字／小文字などの文字列操作関数群が、１つの文字列操作シンボリック代数に統合される。例えばリスト、マップ、アレイ等のウェブアプリケーションで使用される一般的なデータ構造もまたシンボリックにモデル化されている。これらのシンボリックデータ操作関数はシンボリッククラスライブラリ３８に格納される。
【００１６】
この段階で、伝統的な状態に基づくＪａｖａ（登録商標）モデルチェッカ４０が起動され、シンボリックモデル３６上でシンボリック実行が行われる。このとき、計装された関数はシンボリックライブラリ３８を用いて解釈される。
【００１７】
結果として、シンボリック方程式及び文字列ＦＳＭ４２として示された、文字列ではないシンボリックデータをモデル化する一連の複素方程式と、シンボリック文字列データをモデル化する一連の有限状態機械（ＦＳＭ）とが得られる。これは、非文字列の方程式を解く既製の決定手続きと、アプリケーションプログラムの特定箇所のエラー文字列を表すＦＳＭでシンボリック文字列の組を二分するＦＳＭインターセクタ（要素４４として図示されている）へと送られる。決定手続き又はＦＳＭインターセクションの解がエンプティである場合、要求の正当性が認証される。そうでない場合、アプリケーションコードにマッピングし返すエラーシナリオが生成され、バグを発見しないテストケースが生成される。これは、正当性認証又はエラートレース部４６に示されている。この種のシンボリック実行に基づくモデル検査によってのみ検査され得るウェブアプリケーション内の一組のプロパティ／要求が特定されることになる。ウェブアプリケーションの堅牢性における完全な信頼性の網羅的な検査を必要とするセキュリティベースのプロパティにおいて、このような例は数多く存在する。
【００１８】
図３は、シンボリック実行に基づくモデル検査方法を更に詳細に示している。状態に基づくモデルチェッカは、プログラムモデル内の全ての実現可能なパスに沿って、シンボリックモデルを網羅的に実行する。プログラムの制御ポイント（例えば、“ｉｆ”文）ごとに、この実行は２つの異なる方向へと分岐する。各々のパスに沿って、そのプログラムポイントにて取り得る文字列の組を表す文字列ＦＳＭとともに、非文字列のシンボリック方程式が保持される。これは図３の５０及び５２に例示されている。
【００１９】
要求が検査されるべきプログラムのホットスポット５４にて、文字列ＦＳＭは、そのポイントで発生すべきでないエラー文字列の組を表すＦＳＭで分けられる。この文字列の組はユーザ要求により得られ、要素５６に図示されている。また、そのホットスポットにつながるプログラムパスを符号化するシンボリック方程式が、既製の決定手続きソルバを用いて解かれる。決定手続きの解がエンプティである場合、このプログラム内の取り得ないパス又は正しくないパスを意味する。代わりに、インターセクションＦＳＭがエンプティである場合、そのホットスポットにおいてエラー文字列はあり得ない。何れの場合も、要求の正当性が認証される。しかしながら、決定手続きが（本物のパスを意味する）解を返し、且つインターセクションＦＳＭがエンプティでない場合、そのホットスポットにおいてエラー文字列は可能であり、バグが発見される。この解はアプリケーションプログラムにマッピングし返され、ドライバ入力まで伝えられ、そして、エラートレースとバグを捕獲するテストケースとが作り出される。このテストケース生成は完全に自動化され、それにより、手動での検証時間が短縮される。さらに、このようなテストケースは、テストケースが手動生成される場合には見逃されることがあるので、この技術は有用である。
【００２０】
思い起こすことには、ソフトウェア検証構成で用いられる形式的検証エンジンは状態に基づくモデルチェッカである。このチェッカはドライバへの非決定論的なユーザ入力を必要とする。このようなモデルチェッカは、例えば整数や文字列などの全範囲に及ぶ場合、入力スペース全体について論理的に考えることができず、ドライバにおいて指定される可能性あるシナリオを評価できるに過ぎない。
【００２１】
シンボリック実行の場合、モデル検査はステートレスであり、プログラムへの全ての入力を記号として扱い、それにより入力スペース全体を対象とする。シンボリック実行は、（Ｊａｖａ（登録商標）プログラムにおける整数及びブール代数のような）プリミティブデータを扱うことにおいてのみ成功していた。しかしながら、ウェブアプリケーションの場合、殆どの入力及びプリミティブ型は文字列である。従って、文字列をシンボリック実行代数にてモデル化することが必要である。
【００２２】
しかしながら、この方法のバックエンドにてソルバとして使用される決定手続きは、ＣＰＵ時間集約的且つメモリ集約的なものである。故に、決定手続きソルバの性能改善のため、リスト、マップ、セット等のようなウェブアプリケーションで頻繁に使用されるデータ構造をシンボリックにモデル化することが必要である。また、シンボリックモデルを作り出すために必要なコード計装の量は、（関連性解析のような）静的解析技術を用いることによって、最小限に保たれる。これは、解かれる必要のあるシンボリック方程式の大きさを低減する助けとなり、更には、決定手続きの複雑さを対処可能に保つことになる。
【００２３】
本発明により得られるアーキテクチャは、ドライバにおいてユーザ入力を生成することを要しない方法を提供する。さらに、予期されないエラー／挙動が取り除かれ得る。また、本発明の使用により、手動でのテストケース生成時間が、ユーザ要求に基づく興味深いテストケースを自動生成することによって短縮される。最後に、この方法は実質的に、網羅的なプログラムパス及び入力の範囲に基づいて要求の正当性を確認することを可能にし得る。このことは、伝統的な試験方法を用いたときには不可能であったが、セキュリティ検証のような場合には非常に重要なことである。
【００２４】
なお、ソフトウェアの形式的検証技術の欠点は：１）状態に基づく形式的モデルチェッカはドライバにおける入力データを必要とする；２）整数範囲、文字列範囲などの全体にわたる全ての種類のプロパティを扱うことができない；そして、３）自動検査はドライバにて提供される非決定論的な入力選択に制限される；ことである。
【００２５】
システムを中断させる整数を入力スペース内に有することはあり得るかということを尋ねる要求が存在すると仮定する。状態に基づくモデル検査においては、そのような整数に到達することは常に可能なわけではない。この問題を回避するため、設計者は一般的に、数多くのシナリオを試験するために或る特定の整数又は或るランダムな整数を選択する。しかしながら、中断状態を生じさせる正確な整数は必ずしも特定されない。同様のアプリケーションは入力スペースに文字列を必要とする（例えば、ログイン名又はパスワードにて、アプリケーションに中断するよう命じる悪意の文字列が提供される）。この場合も結果的に、これらの状態に基づくシナリオにおいては、非常に多くが試みられなければ、設計者はどの文字列がアプリケーションを中断させることになるかを知ることはない。
【００２６】
さらに、既存のシンボリック実行エンジンは制限されたものである。例えば、１）代数（algebra）は整数、実数及びブール代数用に開発されており、文字列用ではない；２）文字列はウェブアプリケーションにおける主要な入力値である；そして、３）ウェブアプリケーションで頻繁に使用される一定のデータ構造（例えば、ハッシュマップ、セット等）がモデル化される必要がある。シンボリック実行はエラーシナリオを発見することができる。故に、本発明の狙いは、ウェブアプリケーション用にカスタマイズされ、調整されたシンボリック実行エンジンを提供することである。
【００２７】
図４は、セキュリティ検証のシンボリック実行を扱うアプリケーションシナリオを例示する簡易ブロック図である。図４は、攻撃を受けやすいウェブアプリケーション６０、ブラウザアプリケーション６２、インターネットのモデル６４、及びインターネット６４に接続されたバックエンド構成６６を含んでいる。バックエンド構成６６内には、ファイアウォール、ウェブサーバ、アプリケーションサーバ、及びデータベース７２がある。データベース７２は如何なる好適なデータベースオブジェクト（例えば、ＭｙＳＱＬ、Ｏｒａｃｌｅ、ＩＢＭ  ＤＢ２等）であってもよい。
【００２８】
図４には、本発明による教示を実現するための概略的な段階群の一部が例示されている。これは、一般的ログイン［doe］及びパスワード［xyz］を含む単純な例を表している。
【００２９】
図４はまた、このアプリケーションで実行されるコードの一部６８：
String  queryString  =  “SELECT  info  FROM  userTable  WHERE  ”;
if((!  login.equals(“”))  &&  (!  pin.equals(“”)))  {
queryString  +=  “login=’”  +  login  +  “’  AND  pin=”  +  pin  ;
}  else  {
queryString  +=  “login=’guest’”;
}
ResultSet  tempest  =  stmt.execute(queryString);
を含んでいる。
【００３０】
通常の使用構成において、ユーザは一般的ログイン“doe”及びｐｉｎ“123”を提示する［SELECT  info  FROM  users  WHERE  login=  doe  AND  pin=  123］。悪意の使用の場合、攻撃者は‘;  SHUTDOWN;--’及びｐｉｎ“0”を提示する［SELECT  info  FROM  users  WHERE  login=  ;  SHUTDOWN;--  AND  pin=0］。このシナリオにおける応答は、データベースがシャットダウンすることである。これは、ピギーバック・ストアドプロシージャ攻撃の一例を示している。これは、ウェブブラウザを使用することのみによる、ウェブアプリケーションデータベースへの一種のセキュリティ攻撃であり、ＳＱＬインジェクション攻撃として知られている。このような悪意の文字列は、本発明を用いることにより、検出し、更にはデータベースに到達することを制限することができる。これについて以下にて更に詳細に説明する。
【００３１】
図５は、本発明の一実施形態に従ったシンボリック実行方法を例示する簡易ブロック図である。図５は、エラープロパティ構成７０、及び該プロパティ構成７０と相互作用する構成７４を含んでいる。この例において、構成７４はウェブサーバ、アプリケーションサーバ、及びデータベースサーバを含んでいる。
【００３２】
図５に示されるように、ログイン入力を表すためにシンボリック文字列変数（ｘ）が使用される。エラー文字列は、何らかの文字の組に、任意の文字列に埋め込まれた‘;SHUTDOWN;--’とその後ろの更なる文字とが続く、検索文字列として設定される。プログラム内の特定のホットスポットにデータベースへの検索要求として入力され得る全ての文字列を生成するよう、シンボリック実行処理がアプリケーションサーバコードに関して図４及び５に示されるように実行される。そして、エンプティでない組が存在する場合にはそれを特定するために、そのホットスポットにおける文字列の組を表すＦＳＭが、標的とする悪意の文字列ＦＳＭで二分される。その場合、このデータベースに悪意の文字列を伝達する経路が発見されることになる。このように、文字列のこの種のシンボリック実行は、これらの種類のセキュリティ攻撃を探す効果的な方法である。
【００３３】
このように、シンボリック実行法と形式的モデル検査技術とが、セキュリティホールを見出すために使用される。ここで、図５のやり取りに含まれる幾つかの段階を形式化する。第１に、ウェブページからの入力文字列をシンボリック変数ｘとして取り扱う。第２に、アプリケーションサーバコードを通る全てのパスをシンボリックに実行し、シンボリックパス方程式と検索要求ホットスポットにおいて取り得る文字列セットを表すＦＳＭとを作り出す。第３に、要求／プロパティにて指定された悪意の文字列がデータベース検索要求内に現れ得るかを、決定手続きソルバを介して、２つのＦＳＭを二分し且つパス条件を解くことによって検査する。
【００３４】
このシナリオにおいては、予期される入力だけでなく予期されない入力をも検査することができる。これは、洗練されたシンボリック文字列操作ライブラリを用いて達成され得る。例えば、“declare  @a  char(20)  select  @a=0x73687574646f776e  exec(@a)”。これは、‘シャットダウン’用の１６進数を表す。シンボリック文字列操作ライブラリは、この悪意の文字列の変形を自動的に検査することができる。
【００３５】
効果に関して、この特別なシンボリック実行エンジンは、入力ドメインの全体にわたり、且つアプリケーションプログラムの全ての可能なパスにわたる網羅的な検査を提供する。ドライバにおけるユーザ入力は不要である。この場合、予期されない挙動／エラーをも発見することができる。さらに、システムは、要求／プロパティを指定するためのＧＵＩに基づく分かりやすいユーザインタフェースに結合される。このアーキテクチャはカスタマイズされ、Ｊａｖａ（登録商標）ベースのウェブアプリケーション用に調整されることが可能である。故に、そのような最適化されたアーキテクチャは、セキュリティ検証のための文字列操作代数及びアプリケーションを含んだ、ウェブアプリケーション用に調整されたシンボリック実行を提供する。入力スペース全体について論理的に考えることを必要とするプロパティ検査は、この技術によらなければ不可能である。
【００３６】
重要なことには、図１−５に示した構成要素は、デジタル回路、アナログ回路、ソフトウェア、又はこれらの好適な組み合わせとして実装され得る。また、これら図示した構成要素の何れも、その機能を達成するソフトウェアやアルゴリズム、及び／又はここで説明したようなアプリケーションを含んでいてもよい。そのソフトウェアは、ここで概説した機能が果たされ得るようにコードを実行することができる。代替的に、これらの処理及び技術は、如何なる好適なハードウェア、部品、デバイス、特定用途向け集積回路（ＡＳＩＣ）、追加ソフトウェア、フィールド・プログラマブル・ゲート・アレイ（ＦＰＧＡ）、プロセッサ、消去可能なプログラマブルＲＯＭ（ＥＰＲＯＭ）、電気的に消去可能なプログラマブルＲＯＭ（ＥＥＰＲＯＭ）、又はこれらの処理を容易にするよう作用するその他の好適なものによって実現されてもよい。この構成に関連するアーキテクチャの構造によって、相当の柔軟性がもたらされる。故に、容易に認識されるように、これらの機能は概説した環境の外部でも実現され得る。その場合、この機能性は別個の部品、デバイス又はモジュールに容易に実装され得る。
【００３７】
特定された具体的な構成要素を用いて本発明を詳細に説明したが、当業者には様々な変更及び改良が示唆され得る。また、それらの変更及び改良が添付の特許請求の範囲に入る限り、本発明は如何なるそのような変更及び改良をも包含するものである。
【００３８】
なお、開示した具体的なプロセスフローに関し、フローに含まれる如何なる段階も、本発明の範囲を逸脱することなく、変更、追加、あるいは省略されることがあり得る。段階群はまた、本発明の範囲を逸脱することなく、如何なる好適な順序で、あるいは同時に、実行されてもよい。
【００３９】
当業者は数多くのその他の変更、代用、変形、改変及び改良に想到し得る。本発明は、添付の特許請求の範囲に入る限りにおいて、そのような変更、代用、変形、改変及び改良を包含するものである。
【００４０】
以上の説明に関し、更に以下の項を開示する。
（付記１）  １つ以上のウェブアプリケーション用のシンボリック文字列操作ライブラリの一組のクラスを作り出す生成段階であり、操作群を文字列操作シンボリック代数内に統合する生成段階；及び
前記ウェブアプリケーションのうちの１つ以上への要求又はプロパティを検証するために、シンボリック実行に基づくモデル検査を行う実行段階；
を有する方法。
（付記２）  前記文字列操作シンボリック代数を用いてシンボリック実行を行うことによって一定の種類の要求又はプロパティを検査するよう、状態に基づくＪａｖａ（登録商標）モデルチェッカが拡張される、付記１記載の方法。
（付記３）  連結、切り捨て、及び大文字／小文字変換を含み得る一連の可能性ある文字列操作をコンパイルするよう、相異なるウェブアプリケーションが評価される、付記１記載の方法。
（付記４）  エラーシナリオが存在する場合、一組のシンボリック制約に対する解が取得され、且つ前記解は、エラートレースと該エラーを発見しない具体的なテストケースとを取得するため、アプリケーションのソースコードにマッピングされる、付記１記載の方法。
（付記５）  エラーシナリオが存在しない場合、前記要求は検証されたことを示される、付記１記載の方法。
（付記６）  シンボリック文字列、シンボリック整数、浮動小数点数、及びブール値を含むシンボリックモデルを生成するよう、当初のアプリケーションモデルが自動コード計装によって変形される、付記１記載の方法。
（付記７）  前記計装は静的解析及び関連性解析技術によって制限される、付記６記載の方法。
（付記８）  前記計装は、ヒープ、スタック、アレイ又はリストを含むデータ構造のシンボリックモデルを生成する、付記６記載の方法。
（付記９）  プログラムパス条件が伝統的なデータ型のシンボリック方程式によって表され、且つ状態に基づくモデルチェッカの有限状態機械によって表されたシンボリック文字列と組み合わされる、付記１記載の方法。
（付記１０）  入力文字列に基づく要求又はプロパティが、プログラムポイントにおけるシンボリック文字列を表す有限状態機械を、該要求に従った許容されないシンボリック文字列を表す一組の有限状態機械で分けることによって検査される、付記１記載の方法。
（付記１１）  シンボリック実行に基づくモデル検査によって検査可能な一組の要求又はプロパティが特定される、付記１記載の方法。
（付記１２）  要求又はプロパティはテンプレートを介して符号化され、パブリックドメインの決定手続きを用いて検査される、付記１記載の方法。
（付記１３）  アプリケーションプログラムについてのシンボリック解析が代数及びモデルを用いて実行される、付記１記載の方法。
（付記１４）  ウェブアプリケーションについての前記要求又はプロパティはセキュリティ検証に関する、付記１記載の方法。
（付記１５）  シンボリック実行エンジンはＪａｖａ（登録商標）ベースのウェブアプリケーション用にカスタマイズされ且つ調整される、付記１記載の方法。
（付記１６）  コンピュータ読み取り可能な記録媒体に記録されたプログラムであって：
１つ以上のウェブアプリケーション用のシンボリック文字列操作ライブラリの一組のクラスを作り出す生成段階であり、操作群を文字列操作シンボリック代数内に統合する生成段階；及び
前記ウェブアプリケーションのうちの１つ以上への要求又はプロパティを検証するために、シンボリック実行に基づくモデル検査を行う実行段階；
を行わせるプログラム。
（付記１７）  前記文字列操作シンボリック代数を用いてシンボリック実行を行うことによって一定の種類の要求又はプロパティを検査するよう、状態に基づくＪａｖａ（登録商標）モデルチェッカが拡張される、付記１６記載のプログラム。
（付記１８）  連結、切り捨て、及び大文字／小文字変換を含み得る一連の可能性ある文字列操作をコンパイルするよう、相異なるウェブアプリケーションが評価される、付記１６記載のプログラム。
（付記１９）  エラーシナリオが存在する場合、一組のシンボリック制約に対する解が取得され、且つ前記解は、エラートレースと該エラーを発見しない具体的なテストケースとを取得するため、アプリケーションのソースコードにマッピングされる、付記１６記載のプログラム。
（付記２０）  エラーシナリオが存在しない場合、前記要求は検証されたことを示される、付記１６記載のプログラム。
（付記２１）  シンボリック文字列、シンボリック整数、浮動小数点数、及びブール値を含むシンボリックモデルを生成するよう、当初のアプリケーションモデルが自動コード計装によって変形される、付記１６記載のプログラム。
（付記２２）  前記計装は静的解析及び関連性解析技術によって制限される、付記２１記載の方法。
（付記２３）  前記計装は、ヒープ、スタック、アレイ又はリストを含むデータ構造のシンボリックモデルを生成する、付記２１記載のプログラム。
（付記２４）  プログラムパス条件が伝統的なデータ型のシンボリック方程式によって表され、且つ状態に基づくモデルチェッカの有限状態機械によって表されたシンボリック文字列と組み合わされる、付記１６記載のプログラム。
（付記２５）  入力文字列に基づく要求又はプロパティが、プログラムポイントにおけるシンボリック文字列を表す有限状態機械を、該要求に従った許容されないシンボリック文字列を表す一組の有限状態機械で分けることによって検査される、付記１６記載のプログラム。
（付記２６）  シンボリック実行に基づくモデル検査によって検査可能な一組の要求又はプロパティが特定される、付記１６記載のプログラム。
（付記２７）  要求又はプロパティはテンプレートを介して符号化され、パブリックドメインの決定手続きを用いて検査される、付記１６記載のプログラム。
（付記２８）  アプリケーションプログラムについてのシンボリック解析が代数及びモデルを用いて実行される、付記１６記載のプログラム。
（付記２９）  ウェブアプリケーションについての前記要求又はプロパティはセキュリティ検証に関する、付記１６記載のプログラム。
（付記３０）  シンボリック実行エンジンはＪａｖａ（登録商標）ベースのウェブアプリケーション用にカスタマイズされ且つ調整される、付記１６記載のプログラム。
（付記３１）  １つ以上のウェブアプリケーション用のシンボリック文字列操作ライブラリの一組のクラスを作り出す、シンボリック実行に基づくＪａｖａ（登録商標）モデルチェッカであり、
操作群を文字列操作シンボリック代数内に統合し；且つ
前記ウェブアプリケーションのうちの１つ以上への要求又はプロパティを検証するために、シンボリック実行に基づくモデル検査を実行する；
モデルチェッカ、を有するシステム。
（付記３２）  前記文字列操作シンボリック代数を用いてシンボリック実行を行うことによって一定の種類の要求又はプロパティを検査するよう、状態に基づくＪａｖａ（登録商標）モデルチェッカが拡張される、付記３１記載のシステム。
（付記３３）  連結、切り捨て、及び大文字／小文字変換を含み得る一連の可能性ある文字列操作をコンパイルするよう、相異なるウェブアプリケーションが評価される、付記３１記載のシステム。
（付記３４）  エラーシナリオが存在する場合、一組のシンボリック制約に対する解が取得され、且つ前記解は、エラートレースと該エラーを発見しない具体的なテストケースとを取得するため、アプリケーションのソースコードにマッピングされる、付記３１記載のシステム。
（付記３５）  エラーシナリオが存在しない場合、前記要求は検証されたことを示される、付記３１記載のシステム。
（付記３６）  シンボリック文字列、シンボリック整数、浮動小数点数、及びブール値を含むシンボリックモデルを生成するよう、当初のアプリケーションモデルが自動コード計装によって変形される、付記３１記載のシステム。
（付記３７）  前記計装は静的解析及び関連性解析技術によって制限される、付記３６記載のシステム。
（付記３８）  前記計装は、ヒープ、スタック、アレイ又はリストを含むデータ構造のシンボリックモデルを生成する、付記３６記載のシステム。
（付記３９）  プログラムパス条件が伝統的なデータ型のシンボリック方程式によって表され、且つ状態に基づくモデルチェッカの有限状態機械によって表されたシンボリック文字列と組み合わされる、付記３１記載のシステム。
（付記４０）  入力文字列に基づく要求又はプロパティが、プログラムポイントにおけるシンボリック文字列を表す有限状態機械を、該要求に従った許容されないシンボリック文字列を表す一組の有限状態機械で分けることによって検査される、付記３１記載のシステム。
（付記４１）  シンボリック実行に基づくモデル検査によって検査可能な一組の要求又はプロパティが特定される、付記３１記載のシステム。
（付記４２）  要求又はプロパティはテンプレートを介して符号化され、パブリックドメインの決定手続きを用いて検査される、付記３１記載のシステム。
（付記４３）  アプリケーションプログラムについてのシンボリック解析が代数及びモデルを用いて実行される、付記３１記載のシステム。
（付記４４）  ウェブアプリケーションについての前記要求又はプロパティはセキュリティ検証に関する、付記３１記載のシステム。
（付記４５）  シンボリック実行エンジンはＪａｖａ（登録商標）ベースのウェブアプリケーション用にカスタマイズされ且つ調整される、付記３１記載のシステム。
【図面の簡単な説明】
【００４１】
【図１】本発明の一実施形態に従ったシンボリック実行に基づくモデル検査に関するモデルチェッカ及び段階群を例示する簡易ブロック図である。
【図２】本発明の一実施形態に係るシンボリック実行エンジンを示すブロック図である。
【図３】本発明の一実施形態に係るシンボリック実行エンジン内での文字列とその他の変数との組み合わせ方法を例示する簡略図である。
【図４】セキュリティ検証のシンボリック実行を扱うアプリケーションシナリオを例示する簡易ブロック図である。
【図５】本発明の一実施形態に従ったシンボリック実行方法を例示する簡易ブロック図である。
【符号の説明】
【００４２】
１０、３８    シンボリックライブラリ
１４、４０    Ｊａｖａモデルチェッカ
１６    ユースケース
１８    アプリケーションモデル
２０    モデルジェネレータ
２２    ウェブアプリケーション
２４、３６    シンボリックモデル
２６    決定手続きソルバ
２８    要求
３０    アプリケーションモデルのプログラム
３２    統合コード・インスツルメンタ
３４    静的解析ツール
４８    制御フローポイント
６２    ブラウザアプリケーション
６４    インターネット
６６    バックエンド構成
７２    データベース
【図１】
2009087355.tif 000003
【図２】
2009087355.tif 000004
【図３】
2009087355.tif 000005
【図４】
2009087355.tif 000006
【図５】
2009087355.tif 000007