(57)【要約】【課題】  分散型システムのセキュリティ目標をチェックするためのシステムおよび方法を提供すること。【解決手段】  一態様では、複数の詳細なセキュリティポリシーが１つのモデルに変換される。この詳細なセキュリティポリシーは、１つまたは複数の端点間でメッセージを交換する際に実現される。この１つまたは複数の端点は、分散型動作環境でネットワーク接続されたそれぞれのプリンシパルをホスティングする。詳細なセキュリティポリシーが、１つまたは複数の端点のうち少なくとも１つの端点の１つまたは複数のセキュリティ目標を実現するか否かを判定するために、モデルが評価される。【選択図】  図１
2005322234.tif 000002
【特許請求の範囲】
【請求項１】
詳細なセキュリティポリシーをモデルに翻訳するステップであって、前記詳細なセキュリティポリシーは、１つまたは複数の端点間でのメッセージ交換中に実現され、前記１つまたは複数の端点は、分散型動作環境でネットワーク接続されたそれぞれのプリンシパルをホスティングするステップと、
前記詳細なセキュリティポリシーが前記１つまたは複数の端点の少なくとも１つの端点の１つまたは複数のセキュリティ目標を実現するか否かを判定するために、前記モデルを評価するステップと
を含むことを特徴とするコンピュータで実施される方法。
【請求項２】
前記詳細なセキュリティポリシーは、前記１つまたは複数の端点に対する構成データ内で指定されることを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項３】
前記詳細なセキュリティポリシーは、端点間の信頼関係、前記１つまたは複数の端点の１つの端点によってサポートされるサービス、前記１つまたは複数の端点のうちの１つの端点によってサポートされるアクションのうちの、１つまたは複数を示すことを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項４】
前記モデルは、前記１つまたは複数の端点を表すために並行プロセスの計算を使用するステップをさらに含むことを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項５】
前記モデルは、メッセージのフィルタリングおよび処理を表すために論理述部を使用するステップをさらに含むことを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項６】
前記モデルは、前記１つまたは複数の端点に関連付けられたリンク記述内で表明された前記１つまたは複数のセキュリティ目標の正式な仕様をさらに含むことを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項７】
前記詳細なセキュリティポリシーは、１つ以上の基礎的アサーションに対する１つ以上の論理式を含む宣言型データで指定されることを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項８】
前記１つまたは複数の端点は、クライアントとサーバを含む複数の端点であることを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項９】
前記１つまたは複数のセキュリティ目標の１つのセキュリティ目標は、前記メッセージに関連付けられた内容の少なくとも１つの部分集合の秘密または完全性に方向付けられることを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項１０】
前記モデルを評価するステップは、前記１つまたは複数の端点のうちの１つの端点が交換されたメッセージの書換え攻撃に対して脆弱であるか否かを自動的に判定するステップを含むことを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項１１】
前記詳細なセキュリティポリシーに関連付けられた情報の部分集合を翻訳するステップは、前記モデルを作成するために使用可能でなく、
前記モデルを評価するステップは、前記少なくとも１つの端点の前記１つまたは複数のセキュリティ目標が情報の前記部分集合と独立して実現されるか否かを判定するために、前記部分集合を自動的にシミュレートするステップをさらに含む
ことを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項１２】
前記詳細なセキュリティポリシーが変更されたか否かを判定するステップと、
前記判定するステップに応じて、変更された前記詳細なセキュリティポリシーが、前記１つまたは複数の端点の１つ以上のセキュリティ目標を実現するか否かを判定するために、前記モデルを評価するステップと、
前記１つ以上のセキュリティ目標が満たされた場合にのみ、変更された前記詳細なセキュリティポリシーを実現するステップと
をさらに含むことを特徴とする請求項１に記載のコンピュータで実施される方法。
【請求項１３】
詳細なセキュリティポリシーをモデルに変換するステップであって、前記詳細なセキュリティポリシーは、１つまたは複数の端点間でのメッセージ交換中に実現され、前記１つまたは複数の端点は、分散型動作環境でネットワーク接続されたそれぞれのプリンシパルをホスティングするステップと、
前記詳細なセキュリティポリシーが前記１つまたは複数の端点の少なくとも１つの端点の１つまたは複数のセキュリティ目標を実現するか否かを判定するために、前記モデルを評価するステップと
を行うためにプロセッサによって実行可能なコンピュータプログラム命令を含むことを特徴とするコンピュータ可読媒体。
【請求項１４】
前記詳細なセキュリティポリシーが、端点間の信頼関係、前記１つまたは複数の端点の１つの端点によってサポートされるサービス、前記１つまたは複数の端点の１つの端点によってサポートされるアクションのうちの、１つまたは複数を示すことを特徴とする請求項１３に記載のコンピュータ可読媒体。
【請求項１５】
前記１つまたは複数の端点は、クライアントとサーバを含む複数の端点であることを特徴とする請求項１３に記載のコンピュータ可読媒体。
【請求項１６】
前記詳細なセキュリティポリシーに関連付けられた情報の部分集合を翻訳するための前記コンピュータプログラム命令は、前記モデルを作成するために使用可能でなく、
前記モデルを評価するための前記コンピュータプログラム命令は、前記少なくとも１つの端点の前記１つまたは複数のセキュリティ目標が情報の前記部分集合と独立して実現されるか否かを判定するために、前記部分集合を自動的にシミュレートするための命令をさらに含む
ことを特徴とする請求項１３に記載のコンピュータ可読媒体。
【請求項１７】
前記詳細なセキュリティポリシーが変更されたか否かを判定するステップと、
前記判定に応じて、変更された前記詳細なセキュリティポリシーが、前記１つまたは複数の端点の１つ以上のセキュリティ目標を実現するか否かを判定するために、前記モデルを評価するステップと、
前記１つ以上のセキュリティ目標が満たされた場合にのみ、変更された前記詳細なセキュリティポリシーを実現するステップと
を行うために前記プロセッサによって実行可能なコンピュータプログラム命令をさらに含むことを特徴とする請求項１３に記載のコンピュータ可読媒体。
【請求項１８】
スキーマチェックまたは識別子範囲制限照会、端点構成設定照会、ポリシー発送照会、個別ポリシー照会、ポリシー互換性照会、またはカスタム照会のうちの１つまたは複数により詳細なセキュリティポリシーを照会するステップであって、１つまたは複数の端点間での１つ以上のメッセージ交換に関連付けられる前記セキュリティポリシー照会は、分散型動作環境でネットワーク接続されたそれぞれのプリンシパルをホスティングするステップと、
前記照会に応じて、肯定的または否定的セキュリティ報告を生成するステップと
を含むことを特徴とするコンピュータで実施される方法。
【請求項１９】
前記詳細なセキュリティポリシーは、構成ファイルまたはオブジェクトモデル内にあることを特徴とする請求項１８に記載のコンピュータで実施される方法。
【請求項２０】
前記肯定的報告は、ポリシーに割り当てられた端点およびアクションの記述、追跡のメッセージの署名または暗号化された部分の指示、メッセージ受け入れ後の送信側と受信側の間の合意の肯定的表明、およびメッセージ追跡中に発生するいかなる非標準ヘッダーの指示のうちの１つまたは複数を含み、
前記否定的報告は、ある種のメッセージヘッダーの署名またはチェックの失敗の指示、複数メッセージの相互の関係付けの失敗、入力ミス、および脆弱性の訂正方法に関するアドバイスのうちの、１つまたは複数を含むことを特徴とする請求項１８に記載のコンピュータで実施される方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明のシステムおよび方法は、分散型システムのセキュリティに関する。
【背景技術】
【０００２】
既存のプロトコル証明書は、セキュリティプロトコルの特別の手書きによる抽象的な記述を対象とする。
【発明の開示】
【発明が解決しようとする課題】
【０００３】
手書きによる記述と実行コードとの間のギャップは、エラーに繋がる可能性がある。さらに悪いことに、手書きによる記述を確認し、維持することは、非常に労働集約的であり時間が掛かることである。
【０００４】
分散型システムのセキュリティ目標をチェックするためのシステムおよび方法について説明する。一態様では、複数の詳細なセキュリティポリシーが１つのモデルに変換される。この詳細なセキュリティポリシーは、１つまたは複数の端点間でメッセージを交換する際に実現される。この１つまたは複数の端点は、分散型動作環境でネットワーク接続されたそれぞれのプリンシパルをホスティングする。詳細なセキュリティポリシーが、１つまたは複数の端点のうち少なくとも１つの端点の１つまたは複数のセキュリティ目標を実現するか否かを判定するために、モデルが評価される。
【０００５】
図面では、構成要素の参照番号の一番左の数字は、最初にその構成要素が表示された図面を示す。
【０００６】
（概要）
保護されてない搬送手段を介して送信されたＳＯＡＰメッセージは、埋め込まれたセキュリティヘッダーによって保護することができる。このＷＳ−Ｓｅｃｕｒｉｔｙ仕様は、そのようなヘッダーが、署名または暗号文のような暗号材料と、特定のプリンシパルを特定するトークンのようなセキュリティトークンの範囲とをどのように含むことができるかを定義する。ライブラリにおけるそれらの一般的な実施態様に応じて、ウェブサービス開発者は、それぞれのセキュリティ目標に従い、それぞれのメッセージに対するヘッダーとトークンを選択することができ、したがって、それぞれに独自のアプリケーションレベルのプロトコルをＳＯＡＰベース標準の上部で設計することができる。
【０００７】
暗号化技術によって保護された全てのネットワーク接続されたシステムと同様に、ＷＳ−Ｓｅｃｕｒｉｔｙを使用したウェブサービスは、攻撃者がメッセージを傍受し、演算し、挿入するが、基礎となる暗号化アルゴリズムは傷つけないという部類の攻撃に対して脆弱な場合がある。ＳＯＡＰセキュリティの設定において、このような攻撃は、バッファオーバラン、ＳＱＬ挿入等のようなウェブサービス実装に対する攻撃に対して、拡張マークアップ言語（ＸＭＬ）書換え攻撃と呼ばれる。
【０００８】
ＷＳ−Ｓｅｃｕｒｉｔｙのウェブサービス付加拡張機能（ＷＳＥ）２．０実装（および恐らくはこの他も）では、セキュリティヘッダーの処理は、必須コード（ランタイム内で実行するように直接コンパイルされたコード）とは別の宣言構成ファイルを介してプログラムすることができる。ＷＳＥ２．０は、ＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙ仕様に準拠したＸＭＬメタデータファイルに従って、発信セキュリティヘッダーを生成し、入来セキュリティヘッダーをチェックする。これは、保護されたシステムを構築する際に、人間がセキュリティを確認するのに役立つようメッセージ処理の他の態様からセキュリティチェックを分離することを表明する原則に従うものである。それでも尚、このようなシステムには非常に問題が多い。例えば、ＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙは、個別のセキュリティヘッダーを構築し、かつチェックすることに関して低レベル（非常に詳細な）言語である。メッセージ認証または秘密性のような高レベル目標にポリシーを関連付けるようにこのような低レベル言語を使用する直接的な方法はない。既存システムの他の問題点は、ＸＭＬ書換え攻撃に対するエンティティの脆弱性を大きく決定付ける構成ファイル（例えば、ＳＯＡＰベースシステムのＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙファイル）の使用に関するものである。プログラマーには、他のプロトコルおよび新たに発明された暗号化プロトコルによって構成ファイルを変更するほぼ完全な自由がある。これらのプロトコルは、それがどのように見えても、正しく直すことは困難である。すなわち、ランタイム構成ファイルに対する変更は、所望のいかなるセキュリティ目標をも損ないかねない。
【課題を解決するための手段】
【０００９】
本明細書に記載するシステムおよび方法は、これらの問題点に対処するために新しい言語と新しいツールを提案する。例えば、後述する、ＳＯＡＰプロセッサ間で流れるメッセージに関する対象となる秘密および認証目標のための高レベル（抽象的）リンク記述言語を提示する。このリンク言語は、例えばユーザインターフェース（またはウィザード）および／またはシステムモデリングツールから生成することのできるメッセージフローの一般的な場合を対象とする単純な表記法である。ウェブサービス構成のセキュリティをチェックするためのこのシステムおよび方法は、構成ファイル／データにリンク記述をコンパイルするために（図１を参照して以下で説明する）「ジェネレータ」コンピューティングモジュールを使用する。一部には構成ファイルの複雑なセマンティクスのために、構成ファイルを直接書くことよりも、抽象リンク記述から構成ファイルを自動的に生成することの方が、遥かに安全であり、エラーも起こりにくい。説明および実施態様例のために、構成ファイルはしばしばＷＳ−Ｓｅｃｕｒｉｔｙポリシーファイルと呼ばれるが、その構成ファイルは、そのようなデータ形式またはＷＳ−Ｓｅｃｕｒｉｔｙポリシーを実施する環境には限定されない。
【００１０】
さらに、ウェブサービス構成のセキュリティをチェックするためのこのシステムおよび方法は、リンク記述のセキュリティ目標が所与のＷＳ実施態様で達成されるか否かを実行前にチェックするために、「解析」コンピューティングモジュールを使用する。この実施態様では、解析プログラムは、例えば１つ以上のＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙファイルのような構成ファイルと１つの抽象リンク記述との集合体を入力とする。解析プログラムは、この構成のためのモデルを一組のＳＯＡＰプロセッサとして、そのプロセッサが実行するセキュリティチェックと共に構築する。モデルは、リンク記述で表明されたセキュリティ目標の正式な仕様も含む。一実施態様では、例および説明のために、このようなモデルは、このような分散型実施態様を表現するために開発されたパイ計算の方言である、ＴｕｌａＦａｌｅスクリプティング言語で表現される。この実施態様では、ＴｕｌａＦａｌｅ用の既存ツールは、モデルのセキュリティ目標がいかなるＸＭＬ書換え攻撃に対しても脆弱であるか否かを自動的にチェックするために実行される。
【００１１】
上記に鑑みて、ウェブサービス構成のセキュリティをチェックするためのシステムおよび方法は、ＷＳセキュリティ用の暗号化プロトコルの抽象記述の自動分析に、正式な意味を提供する。ツールに分析用モデル（例えば、ＴｕｌａＦａｌｅモデル）を自動的に構築させることにより、手動でモデルを構築することに起因するいかなる人的エラーも大幅に解消され、さらにウェブサービスを実施するために使用される構成ファイルの系統的検証が可能になる。これらのシステムおよび方法は、堅牢な宣言型セキュリティポリシーを構成してサポートすることにより、アプリケーション間の非常に強固な端点間セキュリティを保証する。すなわち、２つのアプリケーションがある場合、またはそれらのセキュリティ設定だけがある場合、上記ツールを使用して静的分析を行うことができる。同様に、実行時に上記ツールを使用して動的分析を適用することもできる。例えば、別のサービスにアクセスする前に、そのサービスに関するデータを取得し、安全な通信が可能か否かをそれらのセキュリティ設定に基づいて判定するためにそのデータを分析することができる。
【００１２】
別の実施態様では、また構成データのセキュリティ目標の仕様の高レベルリンク記述がない場合、ウェブサービス構成のセキュリティをチェックするシステムおよび方法は、ユーザに警告するある種の問題のある構成設定を自動的に識別する。このために、この実施態様は、構成データに対して直接的に、または構成データのオブジェクトモデルに対して、一組の照会を実行するようポリシーアドバイザーを実施する。このポリシーアドバイザーは、ユーザに報告する結果を収集する。各照会は、構文条件（すなわち、構成データの全てまたは一部を満たしても満たさなくてもよいテスト）によってトリガされ、リスクの報告（どのような種類のセキュリティ上の脆弱性が存在しうるかを示すテキスト報告）および補正処置（その脆弱性を解消または低減するために構成データをどのように修正するかを示すテキスト報告）をもたらす場合がある。一実施態様では、各照会の結果がユーザに報告される。さらに、補正処置を、例えばユーザから許可を得た後で、自動的に実行することができる。また、ポリシーアドバイザーは、人間のユーザが保証内容を理解し、潜在的なエラーを突き止めるのを支援するために、構成データを要約して肯定的報告を生成する。
【発明を実施するための最良の形態】
【００１３】
（セキュリティ目標を自動チェックするためのシステム例）
図１は、ウェブサービス用のセキュリティポリシーを自動的に生成し、ウェブサービス構成のセキュリティをチェックするためのシステム例１００を示す。この実施形態ではセキュリティ目標は人間によって書かれるが、他の実施形態では、セキュリティ目標は、自動的に生成されるなど、他のソースから導かれる場合もある。システム１００は、ネットワーク１０６を介して１つまたは複数の遠隔コンピューティング装置１０４に結合されたコンピューティング装置１０２を含む。コンピューティング装置１０２は、コンピュータプログラムモジュール１０８とプログラムデータ１１０を含む。コンピュータプログラムモジュールは、例えば、ランタイムプログラムモジュール１１２、アナライザープログラムモジュール１１４、およびチェッカープログラムモジュール１１６を含む。
【００１４】
ランタイム１１２（例えば、．ＮＥＴランタイム）は、１つまたは複数の遠隔コンピューティング装置１０４全体に亘るなど、複数のマシン全体に分散することのできるランタイム環境を提供する。この実施形態では、ランタイム１１２は、少なくとも一部には構成データ１１８またはスクリプトに基づいて通信に暗号化セキュリティプロトコルを使用する。ランタイム１１２は、例えばオペレーティングシステム、インターネット情報サービス（ＩＩＳ）およびＷＳＥライブラリを含む、他のソフトウェア構成要素とインターフェースをとる。説明のために、このような他のソフトウェア構成要素は、「他のプログラムモジュール」１２０の一部としてそれぞれ表現される。
【００１５】
構成データ１１８は、例えばアドレスのようなシステム１００の配置と、システム１００の複数のコンピューティング装置（マシン）およびそれらの関係のローカル構成とに関する情報を含む。このような情報は、署名を暗号化し、暗号解読し、演算し、署名を検証し、キー材料または新しいｎｏｎｃｅを生成し、メッセージ内の識別情報またはｎｏｎｃｅをチェックし、暗号化アルゴリズム一式から選択し、また例えばＷＳ−Ｓｅｃｕｒｉｔｙデータ形式でセキュリティトークンの範囲を処理する動作のような、暗号化材料の処理を決定することができる。この実施形態では、例えば構成データ１１８は、それぞれが（ＷＳ−Ｐｏｌｉｃｙ言語の特定の場合）ＷＳ−ＳｅｃｕｔｉｒｙＰｏｌｉｃｙ言語に関してポリシー記述の集合体（すなわち、宣言型セキュリティポリシー）に関連付けられた一組のＳＯＡＰ端点の記述である。ＰｏｌｉｃｙＬａｎｇｕａｇｅデータは、ＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙ言語のＸＭＬファイルだが、セキュリティポリシー言語の他のマークアップを使用することもできる。
【００１６】
解析プログラム１１４およびチェッカー１１６は、その保護された実行を検証する（または施行する）よう構成データ１１８をチェックするための正式なツールを共同して提供する。解析プログラム１１４は、構成データ１１８の少なくとも一部をモデル１２２に翻訳する。この実施形態では、モデルは、ＰｒｏｃｅｓｓＭｏｄｅｌ言語で表現される。ＰｒｏｃｅｓｓＭｏｄｅｌは、メッセージのフィルタリングおよび処理を表現する論理述部を含む。この実施形態では、ＰｒｏｃｅｓＭｏｄｅｌデータは、ＴｕｌａＦａｌｅ構文のパイ計算処理だが、他の構文を使用することもできる。例えば、解析プログラム１１４は、ＰｏｌｉｃｙＬａｎｇｕａｇｅを、チェッカー１１６への入力として使用される論理Ｐｒｅｄｉｃａｔｅに翻訳する（ＰｏｌｉｃｙＳｅｍａｎｔｉｃｓ：ＰｏｌｉｃｙＬａｎｇｕａｇｅ−＞Ｐｒｅｄｉｃａｔｅ）。この実施形態では、Ｐｒｅｄｉｃａｔｅは、ＴｕｌａＦａｌｅ構文で論理述部を定義する節である（すなわち、暗号化のシンボリック表現によるＸＭＬデータに関するＰｒｏｌｏｇスタイル述部）。
【００１７】
チェッカー１１６は、例えばＳｅｃｕｒｉｔｙＡｓｓｅｒｔｉｏｎｓ言語で表現される、ＰｒｏｃｅｓｓＭｏｄｅｌのプロパティをチェック／評価するための自動または準自動ツールである。ＳｅｃｕｒｉｔｙＡｓｓｅｒｔｉｏｎｓ言語で表現可能なプロパティの例には、マシン間で交換される一部情報に対する機密性プロパティと、それらマシンによって実行されるローカルアクション間の対応関係として表現される認証プロパティとが含まれる。ＳｅｃｕｒｉｔｙＡｓｓｅｒｔｉｏｎｓは、（識別情報またはデータ保護のような）プライバシーまたはサービス品質に関するセキュリティプロパティも表現することができる。この実施形態では、ＳｅｃｕｒｉｔｙＡｓｓｅｒｔｉｏｎｓ言語は、（正式な対応関係による）認証またはセキュリティプロパティのＴｕｌａＦａｌｅアサーションを含むが、このアサーションの他の表現を使用することもできる。
【００１８】
処理例は、ランタイム１１２の構成Ｃ（構成データ１１８）と人間が生成した比較的短いＳｅｃｕｒｉｔｙＡｓｓｅｒｔｉｏｎｓ  Ａとに鑑みて、システム１００を使用する。チェッカー１１６は、アサーションＡに鑑みて構成Ｃを処理する解析プログラム１１４からの出力を評価する。チェッカー１１６は、ＯＫ（そのアサーションが満たされたことを意味する）、反例（調査を使用し、Ｃのセキュリティ上の脆弱性を示すことができる）、または未認知（チェッカーが終了に失敗することを含み、ここでもまた調査を指定する）を示す結果を出力する。
【００１９】
上記に鑑みて、ランタイム１１２によって直接実行される構成データ１１８も、解析プログラム１１４およびチェッカー１１６によって処理され、ランタイム１１２の実行が攻撃に対して脆弱である可能性があるか否かを直接判定する。これは従来のシステムの逆であり、プロトコル検証装置（検証装置）が、エラーに繋がる危険性のある随時、手書きによる、セキュリティプロトコルの特別の抽象記述、および手書きによる記述と実行コードとの間のギャップに作用し、ならびに繰り返しチェックし、かつ維持する。すなわち、系統的にランタイム１１２とチェッカー１１６をリンクするための解析プログラム１１４は新しい。
【００２０】
システム１００の代替の実施形態は、例えばランタイム１１２がＷＳ−Ｓｅｃｕｒｉｔｙを使用する暗号化プロトコルのいかなるポリシー駆動型実施形態であってもよく、ＸＭＬまたはいかなるマークアップも全く使用しないことを含む。構成データ１１８は、ＰｒｏｃｅｓｓＭｏｄｅｌ自体、または一部の実施形態で直接的に実行することのできるある種の混合を含むことができる。例えば、ＴｕｌａＦａｌｅとＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙとの混合で指定される宣言型構成をサポートするために、ＷＳＥを拡張することができる。さらに、ＰｒｏｃｅｓｓＭｏｄｅｌを取得するために解析プログラム１１４を使用した後で、チェッカー１１６に加えて広範囲の技術およびツールを適用することができる。
【００２１】
チェッカー１１６のこの実施形態は、ＴｕｌａＦａｌｅツールと解決ベースの定理ｐｒｏｖｅｒであるＰｒｏＶｅｒｉｆを使用する。別の実施形態では、別の定理ｐｒｏｖｅｒ（例えば、ＴＡＰＳ）が適用され、加えてモデルチェッカー、タイプチェッカーなども適用される。他の有用な技術は、例えばこのシステムの実施形態のモデルに基づくテストと、そのランタイム挙動のモデルに基づく監視またはフィルタリングとを含む。解析プログラム１１４およびチェッカー１１６は、部分的な構成に対して動作し、１つのシステムの全てではなく一部のマシンに対して例えばポリシーを記述するように改良することができる。この改良は、一部のセキュリティプロパティが、ローカル構成が未知または信頼のない一部のマシンと独立して適用できる（ｈｏｌｄ）か否かをチェックするために有用である。
【００２２】
（ウェブサービスのためのセキュリティポリシーの自動生成）
図１には、ウェブサービスのためのセキュリティポリシーを自動的に生成するシステム例１００も示す。この実施形態においてコンピューティング装置１０２は、リンク言語１２６から構成ファイル１１８を生成する生成モジュール１２４と、（認証のために）リンク言語１２６（リンク記述）を対応関係にマッピングするセキュリティ目標モジュール１２８と、モデル１２２に埋め込むことのできるセキュリティアサーション（例えば一実施形態では、これらの態様はＴｕｌａＦａｌｅスクリプトに埋め込まれる）をさらに含む。モデル１２２への埋め込み用のセキュリティ目標モジュールの出力は、プログラムデータ１１０のそれぞれの部分である。より具体的には、セキュリティ目標モジュールの出力は、一連の対応関係とセキュリティアサーションである。対応関係は、メッセージの受信側がそのメッセージの送信側と一致することのできる一組のデータを示す。このようなデータは、受信側と送信側の識別情報、メッセージの内容、タイムスタンプのようなメッセージのヘッダー、メッセージ識別子、およびルーティング情報、並びにこのメッセージとその対話における前回のメッセージとの関係を含むことができる。秘密アサーションは、（暗号化キー材料を含む）ある種のデータが攻撃者に対して秘密を保たれることを示す。
【００２３】
ＬｉｎｋＬａｎｇｕａｇｅは、端点間の保護されたリンクの単純な言語である。生成モジュール１２４は、これらのリンクをＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙにマッピングする。より具体的には、ＬｉｎｋＬａｎｇｕａｇｅ１２６（「Ｌ」）は、要約か、または、典型的にはクライアントおよびサーバとして動作する数組のプリンシパルの間のＳＯＡＰ端点間の保護されたリンクを記述するための高レベル形式である。各リンクに対して、この形式は、メッセージ認証、機密性、匿名性、要求と応答の相関関係、プリンシパル間の信頼関係、再生またはＤＯＳ保護などを含むことができ、対象となる認証機構のような一部の実施形態の詳細（例えば、共用パスワード、公開キー署名、Ｋｅｒｂｅｒｏｓトークン、ＷＳ−ＳｅｃｕｒｅＣｏｎｖｅｒｓａｔｉｏｎトークン等）にも関係する場合のある、リンクの対象となる目標を記述する。さらに、この形式は、高レベルアプリケーション構成を形成するためにリンクの構成を記述する。
【００２４】
ＬｉｎｋＬａｎｇｕａｇｅ１２６は構成データ１１８よりも非常に抽象的である（例えば、表現力が劣る）ので、ＬｉｎｋＬａｎｇｕａｇｅ記述のセキュリティを確認することは、構成データ１１８の全ての詳細のセキュリティの意味を理解することよりも遥かに容易である。例えば、ＬｉｎｋＬａｎｇｕａｇｅ１２６と生成モジュール１２４は、いかなる生成された構成データ１１８でも、通常ならば手書きによる構成で表現可能なエラーの共通パターンを回避するように設計することができ、したがってランタイム１１２に「ディフォルトで安全」な構成を提供することができる。
【００２５】
このような入力Ｌがある場合、構成Ｃ＝Ｇｅｎｅｒａｔｏｒ（Ｌ）は、Ｌの全てのリンクに対して対象となるセキュリティプロパティを達成するようランタイム１１２を駆動することを意図する。さらに、ＳｅｃｕｒｉｔｙＡｓｓｅｒｔｉｏｎｓ  Ａ＝ＳｅｃｕｒｉｔｙＧｏａｌｓ（Ｌ）は、自動確認に適した、対象となるセキュリティプロパティの正式な表現である。第１の使用例は、いかなるリンク記述Ｌに対しても、本発明者らは、ＯＫまたは反例を戻すべきチェッカー１１６（Ａｎａｌｙｚｅｒ（Ｇｅｎｅｒａｔｏｒ（Ｌ））、ＳｅｃｕｒｉｔｙＧｏａｌｓ（Ｌ））を実行することにより生成モジュール１２４が安全なポリシーを提供することをチェックできるというものである。このチェックは、固定または任意に生成された複数の入力Ｌの組に対する生成モジュール１２４の従来のテストラン中であっても、生成モジュール１２４の実際の配置中であってもよい。したがって、構成Ｃ＝Ｇｅｎｅｒａｔｏｒ（Ｌ）を提供するようにそれが実行される時はいつでも、それをランタイム１１２に渡す前にＣのセキュリティがチェックされる。
【００２６】
第２の使用例は、対象リンクの記述であるリンク記述Ｌと既存のまたは手書きによるポリシーからなる構成Ｃとがある場合、Ｃｈｅｃｋｅｒ（Ａｎａｌｙｚｅｒ（Ｃ）、ＳｅｃｕｒｉｔｙＧｏａｌｓ（Ｌ））を実行することによりＣがＬの目標を満たすか否かをチェックすることができる。
【００２７】
第３の使用例は、リンク記述Ｌと、恐らくはインストール後にＧｅｎｅｒａｔｏｒ（Ｌ）を編集することによって得られた構成Ｃとがある場合、Ｃｈｅｃｋｅｒ（Ａｎａｌｙｚｅｒ（Ｃ）、ＳｅｃｕｒｉｔｙＧｏａｌｓ（Ｌ））を実行することによりセキュリティが維持されたことをチェックすることができる。
【００２８】
生成機能がその構成の一部しか作成せず、残りの構成は変更しないままである場合、これらの使用例は結合することもできる。Ｃｈｅｃｋｅｒ（Ａｎａｌｙｚｅｒ（Ｃ＋Ｇｅｎｅｒａｔｏｒ（Ｌ））、ＳｅｃｕｒｉｔｙＧｏａｌｓ（Ｌ））を実行することによりセキュリティ目標をテストすることができる。
【００２９】
一実施形態では、チェッカー１１６は、定理証明および／またはタイプチェックアプリケーションと共に実行される。このような実施形態では、チェッカー動作は、例えばタイプ注釈のような１つまたは複数の追加ヒントによって円滑化される。例えば、タイプ注釈は、様々なタイプおよび効果システムおよび暗号化プロトコルのための（ＭＳＲ／ＤｅＰａｕｌ大学暗号プロジェクト内で作成されたような）依存型システムを使用して表現することができる。相違は、生成モジュール１２４と共に実行されるべきヘルパー機能を導入することである。説明のために、このようなヘルパー機能を、図６の１つ以上の他のプログラムモジュール６３６のそれぞれの部分として示す。例えば、次の通りである。
【００３０】
【表１】
2005322234.tif 000003
【００３１】
一実施形態では、このヘルパー機能は生成機能と共に実行され、別の実施形態では、このヘルパー機能は生成機能によって実施される。どちらの実施形態でも、ヘルパー機能は、例えばキー材料のための対象となるタイプのような、作成された構成に適切なヒントを構築する。Ａ＝ＳｅｃｕｒｉｔｙＧｏａｌｓ（Ｌ）に対してＣ＝Ｇｅｎｅｒａｔｏｒ（Ｌ）をテストするには、それ以前の自動テストとほぼ同様に、ＳｅｍｉＡｕｔｏｍａｔｉｃＣｈｅｃｋｅｒ（Ａｎａｌｙｚｅｒ（Ｃ），Ａ，Ｈｅｌｐｅｒ（Ｌ））を実行する。本発明者らは、この準自動の変形形態は実施していない。
【００３２】
（ウェブサービスのためのセキュリティポリシー）
（ウェブサービスおよびそれらの構成）
システム１００は、複数のマシン全体に分散されたＳＯＡＰプロセッサ（例えば、コンピューティング装置１０２および１０４）を想定する。各プロセッサは、様々なサービスに対してＳＯＡＰエンベロープ１３０および１３２を送受信することができる。このエンベロープ形式は、ある種の宣言型構成ファイルによって駆動される汎用システムライブラリによって処理され、そのエンベロープペイロードは、必須のアプリケーションコードによって処理される。単純な（保護されていない）エンベロープは、例えば次に示す形式であってよい。
【００３３】
【表２】
2005322234.tif 000004
【００３４】
このエンベロープは、サービスでのメソッドコールを表し、その前に目標サービスおよびアクションのＵＲＩを提供する任意選択ヘッダーと独自のメッセージ識別子とを伴うメッセージ本体を有する。上記の例では、ＧｅｔＯｒｄｅｒ（２０）の結果を戻すには、サービスは、要求者に応答をルーティングするためにヘッダー＜ＲｅｌａｔｅｓＴｏ＞ｕｕｉｄ：５ｂａ８６ｂ０４．．．＜／ＲｅｌａｔｅｓＴｏ＞を付けた１つのエンベロープを使用することができる。
【００３５】
ＳＯＡＰエンベロープは、適切なセキュリティトークンを収集する追加セキュリティヘッダーを使用して保護することができる。例えば、メッセージの完全性はＸＭＬデジタル署名を埋め込む署名トークンによって保護することができるが、送信側の識別情報はＸ．５０９証明書を埋め込む第２のトークンとして渡すことができる。このエンベロープの一部は、可能ならば暗号解除キーの導出方法を示すために第３のトークンを使用して暗号化することもできる。従来の搬送プロトコルと比較して、この方法は性能と複雑性の点で犠牲を払って柔軟性を高める。実際に、ＷＳ−Ｓｅｃｕｒｉｔｙは、セキュリティトークンに正確な文法とディフォルト処理を提供するが、特定のプロトコルは既定しない。
【００３６】
アプリケーションライターには、セキュリティトークンを操作するためのアプリケーションプログラムインターフェース（ＡＰＩ）を使用することではなく、ジェネレータモジュール１２４によって構成データファイル１１８内の一組の詳細なセキュリティポリシーに自動変換するための抽象リンク言語１２６において、それらのセキュリティ要件を記述することが推奨される。この実施形態では、システム１００は、例えば所与のサーバによってサポートされるサービスおよびアクションと、クライアントとサーバ（例えば、１０２と１０４またはこの反対）の間の信頼関係とを記述することによって構成される。この結果、構成データ１１８は、署名を暗号化し、暗号解除し、演算し、署名を検証し、キー材料または新しいｎｏｎｃｅを生成し、メッセージの識別情報またはｎｏｎｃｅをチェックし、暗号化アルゴリズムを選択し、またＷＳ−Ｓｅｃｕｒｉｔｙ形式でセキュリティトークンの範囲を処理するための動作のような、暗号化材料の処理を完全に決定することができる。（ｎｏｎｃｅは、通常は生であることを保証し、したがって再生攻撃を検出しこの攻撃から保護する目的のため、プロトコルにより交換されるデータに含まれる無作為または非反復値である。）
例示による説明のために、システム１００は．ＮＥＴランタイムの上部で実行されるＷＳＥ２．０というウェブサービスを実施するが、他のウェブサービスとランタイムの組み合わせを使用することもできる。このツールが、ＷＳＥ２．０と同じＸＭＬエンベロープおよび構成ファイルを消費し、作成することをチェックするには、次に示す説明は例示の目的でそのセキュリティセマンティックスを取り込んでいる。この方法は、そのような仕様例に応じて他のシステムに適用することができる。
【００３７】
（ＷＳ−ＰｏｌｉｃｙおよびＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙ）
一連のウェブセキュリティ標準、例えばＷＳ−Ｐｏｌｉｃｙ［５］、ＷＳ−ＰｏｌｉｃｙＡｓｓｅｒｔｉｏｎ［６］、およびＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙ［７］は、送信メッセージに埋め込むべきセキュリティトークンおよび受信メッセージに関してチェックすべきセキュリティトークンである、クライアント側とウェブサービス側とに関する宣言を可能にする。これらの名称に関わらず、ポリシーは、通常、それほど抽象的ではない。ポリシーは、機密性または認証目標ではなく、エンベロープの要素を暗号化し署名するための機構を提示する。ＷＳ−Ｐｏｌｉｃｙは、連結、Ａｌｌ［．．．］、および分離、ＯｎｅＯｒＭｏｒｅ［．．．］のための演算子を使用して構成することのできる、基礎的アサーションに対する論理式としてポリシーファイルを構成する。この実施形態では、ＥｘａｃｔｌｙＯｎｅ［．．．］演算子および拒絶された修飾子と任意選択の修飾子のような、セキュリティのために滅多に使用されないＷＳ−Ｐｏｌｉｃｙの他の機能は使用されない。
【００３８】
ＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙは、完全性と機密性のために２つの基礎的アサーションを定義する。各アサーションは、Ｘ．５０９証明書由来か、またはクライアントに関連付けられた共用の秘密から導かれたキーを参照する。ＳＯＡＰエンベロープでは、これは、セキュリティヘッダーにＸ．５０９トークンまたはユーザ名トークンを埋め込むことによって実施される。実際のキーは実行時にローカルデータベースから提供されるが、このアサーションは主題名を具体的に要求することができる。各アサーションはまた、暗号化されるべき、または共同で署名されるべきエンベロープの目標要素を示す明細表によってパラメータ化される。各部分は、そのヘッダー名によって、より一般的にはＸＰＡＴＨ表現を使用して指定することができる。各完全性アサーションに関して、ＸＭＬデジタル署名トークンがセキュリティヘッダーに埋め込まれる。各暗号化された部分に関して、その暗号が目標要素に取って代わる。
【００３９】
受信側では、そのポリシーがこのエンベロープに対して満される場合、ＳＯＡＰエンベロープは有効であるとして受け入れられ、アプリケーションに渡される。反対に、送信側においてプロトコルスタックは、そのポリシーを満たすＳＯＡＰエンベロープを生成する。一実施形態では、および機能の正確さのために、送信側のポリシーは少なくとも受信側のポリシーと同様に要求が厳しい。これは、予備プロトコルを使用して予めポリシーを交換し、比較することにより実現することができる。
【００４０】
次に、ポリシーに対する抽象構文を定義する。この説明では、標準化のためのアルゴリズム、安全なハッシュ、共用キー暗号化の明示的な選択は省略し、それぞれの目的のために固定した明白なアルゴリズムを想定する。（反対に、本発明者らのツールは、ウェブサービス仕様で定義され、ＷＳＥ  ２．０によって使用されるポリシーのために、具体的なＸＭＬ構文を消費し、作成する。）
【００４１】
【表３】
2005322234.tif 000005
【００４２】
一例として、そのメッセージ本体をサービスのＸ．５０９公開暗号キーを使用して暗号化することにより、およびクライアントに関連付けられた共用秘密を使用して全てのその要素に署名することにより、上記のＳＯＡＰエンベロープ例を保護するために、次に示すポリシーを使用することができる。
【００４３】
【表４】
2005322234.tif 000006
【００４４】
（ポリシーマップ（例えば、ＷＳＥ２．０で））
ＳＯＡＰプロセッサは、種々のセキュリティ要件によって多くのサービスをホスティングする（またこれと対話する）ことができるので、サービスおよびエンベロープにポリシーがどのように関連付けられるかを指定する。ＷＳＥ２．０で、これは、それぞれ入来エンベロープと発信エンベロープに対して、ＳＯＡＰ端点から個々のポリシーへの２つの（ＸＭＬ）部分マップを提供する、ＨＴＴＰを介して送信されたＳＯＡＰエンベロープを発送するために使用されるローカル構成ファイルで表現される。（ＨＴＴＰサーバに対して、これはサービスと同じＩＩＳ仮想ディレクトリ内のＷｅｂ．ｃｏｎｆｉｇファイルである。すなわち、クライアントの場合、これはアプリケーションコードと同じローカルディレクトリ内のａｐｐ．ｃｏｎｆｉｇファイルである。）この説明では、ポリシー構成のために抽象構文を使用する。
【００４５】
【表５】
2005322234.tif 000007
【００４６】
一例として、上記の要求および応答をサポートするクライアントに関する構成が提供される。クライアントは、次のように要求を送信し、応答を受信する。
【００４７】
【表６】
2005322234.tif 000008
【００４８】
（ポリシー分析用ツール：アーキテクチャ）
一実施形態におけるウェブサービス構成のセキュリティをチェックする一般的な方法を、図１に示す。図に示すように、この方法例は、（１）ウェブサービスの実際の配置を厳密に反映し、（２）セキュリティプロパティの自動的な検証をサポートするウェブサービスに関する動作モデルを開発する。ＷＳＥ  ２．０を使用してウェブサービスアプリケーションを実際に実行するのではなく、ＸＭＬセキュリティプロトコルを表現するためのスクリプティング言語であるＴｕｌａＦａｌｅを使用してそれらのセキュリティを象徴的に検証する。
【００４９】
図２は、ＴｕｌａＦａｌｅスクリプトとして書かれたシステム記述を分析する場合のデータフロー例を示す。一部のスクロールは、手書きまたは他のスクリプトからコンパイルしたスクリプトを表し、その他の長方形スクロールは、１つのスクリプトを別のスクリプトにコンパイルするか、１つのスクリプトを分析するツールを示す。ＰｒｏＶｅｒｉｆツールは、中間パイ計算で表現されたセキュリティプロトコルを分析するサードパーティのソフトウェアである。ＴｕｌａＦａｌｅツールは、その入力スクリプトのタイプチェックを実行し、次いでＰｒｏＶｅｒｉｆによって分析するためにそれを中間パイ計算においてコンパイルする。
【００５０】
（ウェブサービス用セキュリティツール、ＴｕｌａＦａｌｅ（レビュー））
Ｔｕｌａｆａｌｅ［２］は、暗号化プロトコル検証装置であるＰｒｏＶｅｒｉｆ［３，４］の上部に構築されたＸＭＬ処理をサポートする、適用されたパイ計算に基づきタイプされた言語である。この言語は、用語、述部およびプロセスを有する。用語は、一組の書換え規則によってパラメータ化されたＸＭＬと記号「ブラックボックス」暗号を結合する。例えば、ＴｕｌａＦａｌｅにおけるＡＥＳ対称暗号化および暗号解除を次のように定義する。
【００５１】
【表７】
2005322234.tif 000009
【００５２】
Ｐｒｏｌｏｇスタイルの述部は用語に作用する。これらは、ウェブサービス仕様の構文および非公式セマンティクスを反映するために使用される。例えば、次に示す（付録Ａで使用される）述部は、このＸＭＬトークンを構築し、ユーザ名ｕ、秘密ｐｗｄ、タイムスタンプｔ、およびｎｏｎｃｅ  ｎから導き出されたキーを計算する方法を説明することによってＷＳ−Ｓｅｃｕｒｉｔｙユーザ名トークンの正式な説明を提供する。
【００５３】
【表８】
2005322234.tif 000010
【００５４】
プロセスは、それらの述部を使用して用語を送信し、受信し、変換するプリンシパルの構成を表す。範囲に基づいて、プロセスは、秘密、ｎｏｎｃｅ、およびメッセージ識別子をモデル化する新しい名称を生成することもできる。
【００５５】
攻撃者は、任意の（プロセス）状況全体に分布しており、したがって、通信、暗号化およびＸＭＬ書換えを結合するいかなる積極的な攻撃でも試みることができる。唯一の制約は、新しい名称が攻撃者に対して最初に使用可能でないことである。
【００５６】
正式なセキュリティプロパティは、ＴｕｌａＦａｌｅでも表現可能である。本発明者らは、このスクリプトをコンパイルし、解決ベースのプロトコル検証装置であるＰｒｏＶｅｒｉｆを呼び起こす。各プロパティに対して、ＰｒｏＶｅｒｉｆが成功し、いかなる状況においても全ての実行に対してプロパティを確立するか、または（通常）Ｔｕｌａｆａｌｅ実行に逆コンパイルすることのできる追跡を失敗するか、または分岐する。プロパティは、（一部名称は全ての実行に対して秘密に保たれる）機密性と（それらの進捗状況をマーク付けするためにプロセスによって実行される特別のイベント間の対応関係として表現される）信頼性を含む。ＴｕｌａＦａｌｅスクリプトがプロセスを定義するので、パイ計算の一般的な理論も、例えば補完的なプロパティを手動で証明するか、または自動的に証明されたプロパティを生成するために有効に適用することができる。
【００５７】
（ポリシー構成からのＴｕｌａＦａｌｅスクリプトの生成）
宣言型ＳＯＡＰ構成の検証を容易にするために、まずこれらの構成をＴｕｌａＦａｌｅスクリプトにコンパイルするツールによって本発明者らの枠組みを拡張し、それによってそれらの仕様に正確な動作上のセマンティクスを提供する。本発明者らの「構成コンパイラ」の核（例えば、図１のジェネレータモジュール１２４）は、ＷＳ−Ｓｅｃｕｒｉｔｙに基づくモデル例に関して動作するように構成されたエンベロープ上でのＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙ式からＴｕｌａＦａｌｅ述部への翻訳を含む。実際には、本発明者らのツールは、ＷＳＥ  ２．０実施形態のポリシーマップを収集し、そのＴｕｌａＦａｌｅスクリプトを自動的に生成することもできる。この点から、構成に関する比較的短いセキュリティプロパティを手書きし、ＴｕｌａＦａｌｅを使用してそれらを検証することができる。より具体的には、このツールは、正当性が証明されていないルーティング情報のようなポリシー構成（しばしばＴｕｌａＦａｌｅで明らかな）における一般的なエラーを検出し、報告することもできる。
【００５８】
本発明者らのツールおよび実際のウェブサービスランタイムは、同じポリシー構成を入力する。したがって、本発明者らは、ウェブサービスが攻撃に対して脆弱か否かを直接判定することができる。反対に、前回の作業で、プロトコル検証装置は、エラーに繋がる危険性がある随時、手書きによる、セキュリティプロトコルの特別の抽象的な記述、および手書きによる記述と実行コードとの間のギャップを対象として作用し、ならびに繰り返し確認し、かつ維持する。すなわち、暗号化プロトコルを検証するための多くの正式な技術は、現在は使用可能だが、それらのプロトコルの実際の分散された配置を反映したそれらの系統的な適用は新しい。
【００５９】
（セキュリティ目標の生成および抽象構成のためのポリシー）
高レベルセキュリティ目標を表現するための仕様がない場合、リンク記述１２６は、クライアントとサーバとして動作する数組のプリンシパルをホスティングするＳＯＡＰ端点間の保護されたリンクを記述するために単純な形式を使用する。この形式は、ポリシーマップよりもリンクの方が構成するには遥かに容易かつ安全であることを保証するために、メッセージ認証のようないくつかの基本的なセキュリティプロパティに言及することができる。リンク記述から、本発明者らは、自動確認に適した、対象となるセキュリティプロパティのＴｕｌａＦａｌｅ表現と、それらのプロパティを満たすＷＳＥ構成の両方を生成するツールを提供する。
【００６０】
リンク記述１２６の言語は、抽象的であり、ポリシーマップよりも表現が簡素であるので、リンク記述のセキュリティを確認することは構成の全ての細部のセキュリティの含意を理解するよりも遥かに容易である。例えば、自動的に生成された構成は共通の落とし穴を回避し、したがって「ディフォルトによる安全」をウェブサービス構成に提供するように、それらを設計することができる。
【００６１】
いかなるリンク記述の場合でも、複数のツールを組み合わせて、構成データ１１８内の関連付けられたポリシーが実際に正確であることを、それらを（例えば、ＴｕｌａＦａｌｅまたは別の手段で表現される）モデル１２２に変換し、チェッカー１１６（検証装置）を実行することによりチェックすることができる。例えば一部のポリシーを手書きし、修正された構成が依然として元のセキュリティ目標を満足することをチェックすることにより、異なる（または変更された）構成を使用することもできる。この実施形態では、本発明者らは、ＴｕｌａＦａｌｅスクリプトの手動操作を使用せずに、正式なセキュリティ保証を自動的に検証する。例えば、実行構成の変更後に目標を検証することができる。
【００６２】
図３は、ウェブサービス構成のセキュリティをチェックするための、暗号構成データファイル生成とセキュリティポリシー分析用のデータフロー例を示す。まず、「参照実施形態」（右側）例として示すモデルが、目標システム（左側）のモジュラー構造に従うことに留意されたい。実際、ＷＳ−Ｓｅｃｕｒｉｔｙのモデル化は、例えば、ＴｕｌａＦａｌｅエンベロープが、一連の例に関してＷＳＥで経験的に観察されたものへの対応をチェックすることにより、またＴｕｌａＦａｌｅとＷＳＥで実行されるセキュリティトークンに関する動的チェックを比較することにより、高レベル仕様とは独立して開発され、かつ完全にテストされたものである。第２の段階では、ポリシーのコンパイルが検証される。ポリシーのコンパイルはまた、生成されたポリシーが、ＷＳＥ  ２．０によって受け入れられ、予想されるＳＯＡＰエンベロープを生じることもチェックする。これとは無関係に、このツールは、ポリシー生成の正確さを（仮定するのではなく）チェックする。
【００６３】
この実施形態において、ＳＯＡＰプロセッサおよび攻撃者に対するモデル例は、若干任意である。本発明者らは、攻撃者に追加の機能を提供する追加ＡＰＩをプログラムすることにより、ＴｕｌａＦａｌｅでいくつかの変形を実施した。それでも尚、記載したシステムおよび方法は、任意のＸＭＬ書換え攻撃、および様々なサービスおよびアクションに対する並列セッションでの異なる役割に対して場合によっては同じキーを再利用するＳＯＡＰプロセッサがホスティングするプリンシパルの無制限の数を対処する。より具体的には、また一実施形態では、宣言型ＳＯＡＰ構成を検証するには、構成をＴｕｌａＦａｌｅスクリプトにコンパイルするツールでその枠組みが拡張され、それによりそれらの仕様に正確な動作上のセマンティクスが提供される。「構成コンパイラ」は、ＷＳ−Ｓｅｃｕｒｉｔｙに基づいてエンベロープ上でＷＳ−ＳｅｃｕｒｉｔｙＰｏｌｉｃｙ式からＴｕｌａＦａｌｅ述部への翻訳を実施する。このツールは、ＷＳＥ実施形態のポリシーマップも収集し、そのＴｕｌａＦａｌｅスクリプトを自動的に生成する。この点から、構成に対する比較的短いセキュリティプロパティを手書きし、ＴｕｌａＦａｌｅを使用してそれらを検証することができる。
【００６４】
システム１００はまた、正当性が証明されていないルーティング情報のような、ポリシー構成（しばしばＴｕｌａＦａｌｅで明らかな）の共通エラーを検出し、報告する。このツールと実際のウェブサービスランタイムは、同じポリシー構成を入力とする。したがって、このシステムおよび方法は、構成データポリシーファイルの構成ミスによって生じるウェブサービスの脆弱性を直接決定することができる。反対に、前回の作業で、プロトコル検証装置は、セキュリティプロトコルの特別な手書きによる抽象的な記述を対象とし、手書きによる記述と実行コードの間のギャップがエラーに繋がる危険性があり、チェックし、維持することは退屈である。上記に鑑みて、システム１００の記載したシステムおよび方法は、これらのプロトコルの実際の分散型配置を反映するために、それらのアプリケーションの暗号化プロトコルを検証する。
【００６５】
（ポリシー分析：実施形態）
（ＳＯＡＰプロセッサを使用したプリンシパル）
以下の説明は、まず、モデル１２２の非公式の概要を提供し、次いで本発明者らのパイ計算の異形であるＴｕｌａｆａｌｅでのモデル符号化例を詳述する。本発明者らのシステムは、公共ネットワークによって接続されたマシンで実行されるＳＯＡＰプロセッサを含む。例えば、信頼あるプロセッサでも信頼のないプロセッサ（攻撃者により制御される）でも実施することのできるシステム１００を参照されたい。プロセッサは、プリンシパルに代わってＳＯＡＰエンベロープを送受信する。一実施形態では、プリンシパルは、どのエンベロープを送信し、受信したエンベロープをどうすべきかを記述するコードを提供する。簡約化のために、プリンシパルは、それらが認証トークンに表示されるように、すなわちＸ．５０９の主題名とＵｓｅｒｎａｍｅＴｏｋｅｎｓのユーザ名のように、それらの（ストリング）名によって識別される。プリンシパルは、それらの関連付けられた秘密に対するアクセスを制御するので重要である。この分散型システムは、秘密をプロセッサに分配するために抽象的な機構を使用する。
【００６６】
単一プロセッサが多くのプリンシパルをホスティングすることができ（例えば、いくつかのプリンシパルによって署名されたエンベロープを送信する際に）、さらに無数のプロセッサが同じプリンシパルをホスティングすることができる（例えば、１つのサービスを繰り返すために）。したがって、次のようにパラメータ化された一般的なＳＯＡＰプロセッサを使用する。
・  ＳＯＡＰ端点からポリシーへの部分マップを表現する、ＳＯＡＰメッセージを送信し受信するための２つの宣言型構成。  
・  ホストプリンシパル用の共用パスワードとＸ．５０９証明書と秘密鍵とを記録するローカルデータベース。  
【００６７】
例えば、データベースに記録された秘密のいくつかを使用して、そのＵＲＩおよびアクションに関連付けられた受信ポリシーによって表現された要件を満たすことができる場合、ＳＯＡＰエンベロープが受け入れられる。一実施形態では、パイ計算は、攻撃者に豊富なインターフェースを提供する。この環境は、プリンシパルの作成、それらの破損、および証明書と共用キーの生成を制御する。
【００６８】
以下では、アクセスすることのできる全ての秘密がそれらのＳＯＡＰプロセッサによってのみ使用されるように、一組の準拠プリンシパルを区別する。当然ながら、ＳＯＡＰ処理は、準拠プリンシパルの知識に依存しない。この知識は、セキュリティプロパティ例を指定するためにだけ使用される。準拠プリンシパルが一度特定されると、ＳＯＡＰプロセッサ間におけるそれらの分配は正式に無関係となる。正式には、いかなるそのような構成が、全ての準拠プリンシパルをホスティングする単一プロセッサによる構成、すなわち全てのローカルマッピングおよびデータベースをマージするグローバルポリシーマッピングとデータベースによる構成と、観察上は等価であることを示す。
【００６９】
（ポリシー駆動ＳＯＡＰシステムのモデル化）
モデル例１２２スクリプトを、ライブラリと主要ＴｕｌａＦａｌｅプログラムとして付録に示す。これらのスクリプト例は、詳細な正式のセマンティクス例を提供する。次に、一部には一例として、それらのスクリプトの重要な部分を説明する。本発明者らのＳＯＡＰ構成のトップレベルの構造は、次に示す、並列に実行される４つの複製されたプロセスを含む。
【００７０】
（ＵｓｅｒｎａｍｅＧｅｎｅｒａｔｏｒ（）｜Ｘ５０９Ｇｅｎｅｒａｔｏｒ（）｜ＧｅｎｅｒｉｃＳｅｎｄｅｒ（）｜ＧｅｎｅｒｉｃＲｅｃｅｉｖｅｒ（））
（ユーザ名ジェネレータ）
ユーザ名ジェネレータは、ｇｅｎＵＰＣｈａｎチャネルで（攻撃者から）プリンシパル名ｕをとり、新しいパスワード「ｐｗｄｕ」を生成する。このパスワードとユーザ名は、ｄｂＣｈａｎへの複製された出力として、秘密データベースに追加された新しい項目を形成する。したがって、この項目は、ｄｂＣｈａｎを共有するいかなる公正なプロセッサに対しても使用可能となる。
【００７１】
【表９】
2005322234.tif 000011
【００７２】
信頼のないプリンシパルを有効なパスワードでモデル化するために、別の複製されたプロセスを、類似の構造で、ユーザ名ジェネレータに追加する。このプロセスは、ｇｅｎＬｅａｋＵＰＣｈａｎのプリンシパル名ｕをとり、新しいパスワードを生成し、それを公共チャネルｐｕｂｌｉｓｈＣｈａｎ上の攻撃者に漏洩し、そのユーザ名とパスワードをデータベースに挿入する。パスワードを漏洩する前に、このプロセスは、プリンシパルｕが最早信頼することができない旨を示して、開始ＬｏｇＰ（ｕ）を呼び起こす。このイベントは、システム内の全てのプロセスに不可視であり、純粋に本発明者らの証明目標を指定するために使用される。
【００７３】
同様に、Ｘ５０９Ｇｅｎｅｒａｔｏｒ（付録Ｅで定義される）は、１つの秘密署名キーｓｒを制御する１つの証明書当局により、公共チャネルｇｅｎＸＣｈａｎおよびｇｅｎＬｅａｋＸＣｈａｎで２つのサーバを実施する。
【００７４】
（一般送信側）
例示のために、ＳＯＡＰ送信側および受信側は、それぞれにコンピューティング装置１０２および１０４により表現される。ＳＯＡＰ送信側は、述部ｍｋＣｏｎｆｏｒｍａｎｔで符号化され、通常ならば一般的である、その送信ポリシー構成により異なる。これは、チャネルｉｎｉｔＣｈａｎで攻撃者からエンベロープをとり、対象となる宛先に対して送信ポリシー構成を実現し、ｈｔｔｐＣｈａｎで送信される新しいポリシー準拠エンベロープを生成する。
【００７５】
述部ｍｋＣｏｎｆｏｒｍａｎｔは、送信ポリシーを選択し、それを、入力エンベロープに対して暗号化動作を実行することにより数組のプリンシパルに対して実現するよう試みる。プリンシパルのその組と、それらの関連付けられた秘密は、リストｉｄｅｎｔｓによって表現される。このリストは、データベースから適切な数の識別情報を抽出することによりポピュレートされる。さらに、新しいキーまたはｎｏｎｃｅとして使用することのできる新しい名前の新たなリストに述部が提供される。
【００７６】
【表１０】
2005322234.tif 000012
【００７７】
（一般的なレシーバ）
ＳＯＡＰレシーバは、チャネルｈｔｔｐＣｈａｎの攻撃者からエンベロープをとり、対象となる宛先に対して受信ポリシー構成を実現し、そのエンベロープが受け入れ可能な証拠を生成する。述部ｉｓＣｏｎｆｏｒｍａｎｔは、受信ポリシーを選び、暗号化動作を実行することにより数組のプリンシパルに対してそのエンベロープがそれと一致するか否かをチェックする。送信側に関しては、その組のプリンシパルとそれらの関連付けられた秘密は、データベースの部分集合を表現するリストｉｄｅｎｔｓによって表現される。
【００７８】
【表１１】
2005322234.tif 000013
【００７９】
（ポリシーのセマンティクス）
ＳＯＡＰシステム１００のポリシー構成１１８は、ｍｋＣｏｎｆｏｒｍａｎｔとｉｓＣｏｎｆｏｒｍａｎｔの２つの述部として符号化される。具体的には、送信ポリシーマップは、ｍｋＣｏｎｆｏｒｍａｎｔの節によって表現され、受信ポリシーマップは、ｉｓＣｏｎｆｏｒｍａｎｔの節によって表現される。このセクションでは、所与のポリシー構成からこれらの節を生成するツールを指定する。本発明者らは、１つは送信ポリシー、１つは受信ポリシーの、セクション２のクライアント側構成ｃｌｉｅｎｔＣｏｎｆｉｇから生成されたサンプルの節を提示する。この送信ポリシーは、パスワードベースのキーを使用して５つのメッセージ部分のデジタル署名を使用する。このポリシーは、リンク記述１２６から、例えば次に示す述部（構成１１８内の）に翻訳される。
【００８０】
【表１２】
2005322234.tif 000014
【００８１】
この述部は、まず、エンベロープのためのメッセージｉｄ、ｎｏｎｃｅ、およびパスワードベースキーを生成するためのタイムスタンプという３つの新しい名称を抽出する。次の４のｈａｓＸｘｘコールは、署名されるために使用される５つのメッセージ部分のうちの４つを抽出する。この述部は次いで、新しいメッセージｉｄにより新しい＜ＭｅｓｓａｇｅＩｄ＞要素を作成する。この述部ｇｅｔＵｓｅｒｎａｍｅＴｏｋｅｎは、１つの任意のユーザ名とパスワードをｉｄｅｎｔｓデータベースから抽出し、新しいｎｏｎｃｅとタイムスタンプを使用して新しいユーザ名トークンｕｔｏｋとパスワードベースのキーｋとを生成する。ｍｋＳｉｇｎａｔｕｒｅ述部は、全ての５つのメッセージ部分を署名するＸＭＬ署名ｓｉｇを構築するためにキーｋを使用する。最後に、この述部は、全ての入力メッセージ部分、新しいメッセージｉｄ、および新しいユーザ名トークンおよび署名によって出力エンベロープｏｕｔｅｎｖを構築する。
【００８２】
ｈａｓＳｅｎｄＰｏｌｉｃｙＣｌｉｅｎｔＴｏＳｅｒｖｉｃｅは、それぞれの構成１１８に記載されたクライアント送信ポリシーを実現する。対応する送信ポリシーマップが、ｍｋＣｏｎｆｏｒｍａｎｔ述部の節に翻訳される。この節はまず、メッセージの宛先サービスとアクションをポリシーマップのアドレスと照合し、次いでｈａｓＳｅｎｄＰｏｌｉｃｙＣｌｉｅｎｔＴｏＳｅｒｖｉｃｅ述部を呼び起こす。
【００８３】
【表１３】
2005322234.tif 000015
【００８４】
ｃｌｉｅｎｔＣｏｎｆｉｇ  １１８の第２のポリシーは、応答メッセージ内の５つのメッセージ部分が、プリンシパルＢｏｂｓＰｅｔＳｈｏｐに発行されたＸ５０９証明書で署名されていることをチェックする受信ポリシーである。
【００８５】
【表１４】
2005322234.tif 000016
【００８６】
対応する受信ポリシーマップが、ｈａｓＲｅｃｖＰｏｌｉｃｙＳｅｒｖｅｒＴｏＣｌｉｅｎｔを単純に呼び起こすｉｓＣｏｎｆｏｒｍａｎｔ述部の節に翻訳される。
【００８７】
【表１５】
2005322234.tif 000017
【００８８】
付録Ｃは、ポリシー構成を述部に翻訳するための規則例を詳述して、一般的な場合の例を提示する。これは、図１の解析モジュール１１４によって実行される。
【００８９】
（ポリシー構成およびセキュリティ目標の生成）
（リンク仕様の抽象構文）
リンクは、ウェブサービスとそのクライアントの間のＳＯＡＰセッションに対して高レベルセキュリティ目標を定義する。リンク記述１２６は、一組のリンク（対象ウェブサービス全てに対する）を含む。ウェブサービスは、そのサービスＵＲＩ、ｓｕｒｉによって特定され、また、それらのＳＯＡＰアクションＵＲＩ、ａｃｔｉｏｎｓによって特定される一組のウェブメソッドを提供する。
【００９０】
例示のために、クライアントとウェブサービスの間で定義されるＳＯＡＰセッションの３つの異なる場合がある。このセクションの大部分で想定する第１の場合では、１つのセッションは１つのメッセージを含む。各リンクは、クライアントからサービスに対する要求のセッションとサービスからクライアントに対する要求のセッションの、２つのセッションを指定する。このリンクは、各方向のメッセージが署名され、任意選択で暗号化されており、その署名は共同してウェブサービスとメッセージ本体と独自のメッセージ識別子とを認証する必要があることを規定する。この場合、このリンク仕様は、サービスごとに多くても１つのリンクを定義する（ｓｕｒｉ）。具体的には、１つのサービスの全てのアクションが、同じセキュリティ目標を有するということである。２つのウェブメソッドが異なるセキュリティ保証を使用する場合、それらは別個のウェブサービスとして実施される。この仮定は、他のタイプのセッションでは緩やかである。
【００９１】
第２の場合、１つのセッションは要求−応答の交換を含む。この場合、このリンクは、応答が要求に適切に相関関係を有することを付加的に規定する。第３の場合、１つのセッションは、ＷＳ−ＳｅｃｕｒｅＣｏｎｖｅｒｓａｔｉｏｎ仕様によって定義されるような、クライアントとサーバの間の保護された複数メッセージによる対話である。
【００９２】
リンクの構文例を次に示す。この例は、ＭＬスタイルリスト（括弧で括られ、コンマで分離された一連の要素）に言及するためにコンストラクタリストを使用する。
【００９３】
【表１６】
2005322234.tif 000018
【００９４】
この実施形態では、リンク記述１２６に記載された各リンク（保護されたリンク）は、ウェブサービスＵＲＩ、ｓｕｒｉ、一組の許可されたアクション、ａｃｔｉｏｎｓ、クライアントとして動作可能なプリンシパルの名（ｃｌｉｅｎｔＰｒｉｎ）またはウェブサービスとして動作可能なプリンシパルの名（ｓｅｒｖｉｃｅＰｒｉｎ）、および双方向のメッセージのセキュリティレベルを含む。プリンシパル名がユーザ−パスワードの組み合わせ中のユーザ名であるか、またはＸ．５０９証明書中の主題名であることを想起されたい。特別な場合として、クライアント（またはサービス）プリンシパルのエンプティリストを、いかなるプリンシパルでもそのリンクに対するクライアント（またはサービス）として動作することを可能にするものと解釈する。このセキュリティレベルは、暗号化なしを意味するＣｌｅａｒであっても、要求と応答の両方が暗号化された本体を有することを意味するＥｎｃｒｙｐｔｅｄであってもよい。暗号化の場合、クライアントとサーバの両方のプリンシパルがＸ．５０９証明書を使用する必要がある。
【００９５】
一例として、次に示すリンクを想定する。
【００９６】
【表１７】
2005322234.tif 000019
【００９７】
このリンクは、http://bobspetchop.com/service.asmxにあるウェブサービスがHttp://Petshop/Premiumとhttp://petshop/regularの２つのアクションを提供し、そのクライアントがいかなる信頼できるプリンシパルの代わりとしても動作でき、サービスはＢｏｂｓＰｅｔＳｈｏｐの代わりとしてのみ動作することを表明する。双方向のメッセージが認証されるが、暗号はｈａｖｅｄではない。後のセクションでは、このリンクの暗号化されたバージョンをＥｎｃＬｉｎｋと呼ぶ。
【００９８】
（リンク仕様からのポリシー構成の生成）
次に、リンク記述１２６のリンクのリストをポリシーマップのリストを含む構成１１８に翻訳するためのモジュール１２４のジェネレータ機能を説明する。上記の例示の翻訳から始める。まず、ウェブサービスの各アクションとそのクライアントに対するアドレスを次に示すように定義する（ａｄｄｒ表記法で）。
【００９９】
【表１８】
2005322234.tif 000020
【０１００】
要求メッセージ（１３０または１３２）の場合、ポリシーは、ある種の信頼あるプリンシパルによって署名されたメッセージのデジタル署名を使用する。この署名は、メッセージの完全性と信頼性を保証する。このｒｅｑｕｅｓｔＰｏｌｉｃｙは次のようなものである。
【０１０１】
【表１９】
2005322234.tif 000021
【０１０２】
メッセージ内容（Ｂｏｄｙ）、宛先（Ｔｏ，Ａｃｔｉｏｎ）、および識別子（ＭｅｓｓａｇｅＩｄ，Ｃｒｅａｔｅｄ）は、メッセージに含まれるデジタル署名の対象であり、そのサービスが信頼するある種のプリンシパルのパスワードまたはＸ５０９証明書に基づいている。
【０１０３】
応答メッセージ（１３０または１３２）の場合、ＢｏｂｓＰｅｔＳｈｏｐに発行されたＸ５０９に基づいたデジタル署名であるｒｅｓｐｏｎｓｅＰｏｌｉｃｙは、次に示すように使用される。
【０１０４】
【表２０】
2005322234.tif 000022
【０１０５】
この応答メッセージは、そのＲｅｌａｔｅｓＴｏヘッダー内に先行要求のメッセージ識別子を含む。応答の宛先は、暗黙的に、そこにこの要求メッセージを送信したクライアントである。ポリシーは、サービスＵＲＩ（Ｆｒｏｍ）と要求ｉｄ（ＲｅｌａｔｅｓＴｏ）が応答識別子（ＭｅｓｓａｇｅＩｄ，Ｃｒｅａｔｅｄ）および応答内容（Ｂｏｄｙ）と共にデジタル署名の対象であることを規定する。
【０１０６】
サービスでのポリシー構成１１８は、次に示すように、要求に対する受信ポリシーと応答に対する送信ポリシーとを含む。
【０１０７】
【表２１】
2005322234.tif 000023
【０１０８】
一般的に、サービス構成１１８は、各タプル（アクション、クライアントプリンシパル、サーバプリンシパル）当たり１つの受信ポリシーと、各対（クライアントプリンシパル、サーバプリンシパル）当たり１つの送信構成とを含む。反対に、クライアントでは、ポリシー構成１１８は、要求に対する送信ポリシーと応答に対する受信ポリシーとを含む。
【０１０９】
【表２２】
2005322234.tif 000024
【０１１０】
付録Ｄに、ポリシー構成を生成するための規則例を示す。
【０１１１】
（セキュリティ目標の埋め込み）
リンク記述１２６のリンクは、複数のクライアントプリンシパルの１つの代わりに動作するクライアントと、複数のサービスプリンシパルの１つの代わりに動作するウェブサービスとの間のセッションに対するセキュリティ目標を規定する。認証目標は、サービスプリンシパルは、クライアントプリンシパルによって送信された要求メッセージのみを受け入れ、クライアントプリンシパルは、サービスプリンシパルによって送信された応答メッセージ（顕著な要求に関する）のみを受け入れるというものである。さらに、リンクが秘密を使用する場合、メッセージ本体は、そのリンクに参加しないいかなるプリンシパルに対しても秘密に保たれる。このセクションでは、これらのセキュリティ目標を形式化し、それらにどのようにＴｕｌａＦａｌｅスクリプトが埋め込まれるかを示す。
【０１１２】
アサート機能は、リンク仕様１２６をとり、信頼性とセキュリティアサーションを支配するｈａｓＬｉｎｋＡｓｓｅｒｔとｍｋＬｉｎｋＥｎｖｅｌｏｐｅ述部に対する節を生成する。これは、図１の解析モジュール１１４によって実行される。
【０１１３】
公正なＳＯＡＰプロセッサによって送信され、または受け入れられるエンベロープは、ある種のリンクＬに対する要求または応答である。そのようなエンベロープそれぞれに関して、ｈａｓＬｉｎｋＡｓｓｅｒｔはメッセージの方向とエンベロープ内容とに基づいて完全性アサーション（「ａｓｓ」）を計算する。公正なＳＯＡＰプロセッサは、メッセージｅｎｖを送信するたびに、まずイベント開始Ｌｏｇ（ａｓｓ）を呼び起こす。反対に、ｅｎｖを受け入れるたびに、次いで終了Ｌｏｇ（ａｓｓ）を呼び起こす。本発明者らの信頼性目標は、全ての終了Ｌｏｇ（ａｓｓ）の前に開始Ｌｏｇ（ａｓｓ）との一致が先行するというものである。
【０１１４】
上記で定義されたＳｉｍｐｌｅＬｉｎｋ例の場合、生成された節は、例えば次に示すようなものである。
【０１１５】
【表２３】
2005322234.tif 000025
【０１１６】
この述部の最初の２行は、そのエンベロープがＳｉｍｐｌｅＬｉｎｋに属することを、その宛先サービスとアクションをチェックすることによってチェックする。次いで、本体、メッセージｉｄ、および作成タイムスタンプという、対象となる３つの他のフィールドを抽出する。最後に、本発明者らが保護しようとする５つのメッセージ部分と連結してクライアントおよびサーバプリンシパル名を含むアサーションを戻す。リンクはサービスプリンシパルだけに言及するので、クライアントプリンシパルは任意のプリンシパルを表現する「＊」で置き換えられる。
【０１１７】
応答メッセージの場合、計算されたアサーションは、宛先サービス（Ｔｏ）とアクションフィールドがソースサービス（Ｆｒｏｍ）とＲｅｌａｔｅｓＴｏフィールドと交換されることを除いて、極めて類似している。
【０１１８】
【表２４】
2005322234.tif 000026
【０１１９】
ここで、リンクはＦｒｏｍフィールドをリンクサービスＵＲＩと照合することにより特定される。上記と同様、次いでメッセージ部分が抽出され、分かっている場合はプリンシパル名と連結される。
【０１２０】
本発明者らの一般的なＳＯＡＰ送信側は、攻撃者から１つのエンベロープをとり、いくつかのセキュリティヘッダーと暗号化したブロックを追加した後でそれを送出する。リンクが秘密を使用する場合、次いでそのエンベロープの本体はその攻撃者から保護される。これをモデル化するために、ＳＯＡＰ送信側は、暗号化されたリンクでエンベロープを送信することが要求される場合はいつでも、メッセージ本体を秘密本体Ｂと交換するためにｍｋＬｉｎｋＥｎｖｅｌｏｐｅ述部を使用する。この場合、秘密アサーションは、攻撃者が様々なリンクでいくつかのメッセージを監視したとしてもＢを知ることはできないというものである。
【０１２１】
プライベート名Ｂ
秘密Ｂ
暗号化されたリンクの例として、要求メッセージのｍｋＬｉｎｋＥｎｖｅｌｏｐｅ節であるＥｎｃＬｉｎｋを次に示す。応答メッセージは類似である。
【０１２２】
【表２５】
2005322234.tif 000027
【０１２３】
この節は、このエンベロープがＥｎｃＬｉｎｋに属するか否かをチェックし、次いで本体を秘密本体（Ｂ）と交換する。データＢは、本発明者らが秘密を維持しようとするシステム内の全てのデータを表す。したがって、これは、暗号化されたリンクでのみ送出することができる。対照的に、秘密でないデータはいかなるリンクでも送出することができ、単にそのエンベロープを変更せずに置くｍｋＬｉｎｋＥｎｖｅｌｏｐｅ節によってモデル化することができる。
【０１２４】
付録Ｄに、セキュリティ目標に対するリンクのマッピング例を示す。
【０１２５】
（リンクスペックおよび構成により定義されるスクリプトの分析）
特別なポリシー構成が、リンク記述／スペック１２６によって定義されるセキュリティ目標を達成するか否かをチェックするために、ＴｕｌａＦａｌｅスクリプトをどのように構築するかを定義する。リンクＬがある場合、生成モジュール１２４は、述部ｈａｓＬｉｎｋＡｓｓｅｒｔおよびｍｋＬｉｎｋＥｎｖｅｌｏｐｅに対する節を生成する。構成Ｃがある場合、生成モジュール１２４は、述部ｍｋＣｏｎｆｏｒｍａｎｔおよびｉｓＣｏｎｆｏｒｍａｎｔに対する節を生成する。これら４つの述部は、ＳＯＡＰプロセッサのＴｕｌａＦａｌｅモデルに埋め込まれる。送信側は、ｍｋＬｉｎｋＥｎｖｅｌｏｐｅを使用して秘密本体を使用することができる。次いで送信側は、ｈａｓＬｉｎｋＡｓｓｅｒｔを使用して完全性アサーションを計算し、開始Ｌｏｇ（ａｓｓ）を呼び起こし、ｍｋＣｏｎｆｏｒｍａｎｔを使用してポリシー準拠発信エンベロープを計算し、ネットワークでそのメッセージを送信することができる。反対に、受信側は、ｉｓＣｏｎｆｏｒｍａｎｔを使用してポリシー準拠に関して入来エンベロープをチェックし、次いで終了Ｌｏｇ（ａｓｓ）を呼び起こす前にｈａｓＬｉｎｋＡｓｓｅｒｔを使用して完全性アサーションを計算する。
【０１２６】
ポリシー構成がリンクセキュリティ仕様を満たしていることを検証するために、チェッカー１１６は、ＴｕｌａＦａｌｅを実行して信頼性とセキュリティ目標をチェックする。この実施形態では、一般的な定義には、例えば次のものが含まれる。
【０１２７】
定義４．１  受信側プロセスが終了Ｌｏｇ（［ｕ］＠ａｓｓ）を呼び起こすときはいつでも、既に開始Ｌｏｇ（［ｕ］＠ａｓｓ）を呼び起こした送信側プロセスがいくつかあるか、またはいくつかのトークンジェネレータプロセスが既に開始ＬｏｇＰ（ｕ）を呼び起こしている場合、ＴｕｌａＦａｌｅプロセスはＬｏｇ、ＬｏｇＰに対して確実に安全であると言われている。
【０１２８】
攻撃者がＢを知っているときはいつでも、いくつかのトークンジェネレータプロセスが既に開始ＬｏｇＰ（ｕ）を呼び起こしており、いくつかの送信側プロセスが既に開始ＬｏｇＳ（ｕ、Ｂ）を呼び起こしているようにプリンシパルｕがある場合、ＴｕｌａＦａｌｅプロセスは、ＬｏｇＰ、ＬｏｇＳに対してＢの秘密を維持するものであると言われている。
【０１２９】
終了Ｌｏｇ（ａｓｓ）が最終的に呼び起こされるようにプロセスの実行がある場合、ＴｕｌａＦａｌｅプロセスは、Ｌｏｇ（ａｓｓ）に対して機能上適切であると言われている。
【０１３０】
リンク仕様ＳｉｍｐｌｅＬｉｎｋから生成されたポリシー構成ＳｉｍｐｌｅＣｏｎｆｉｇを想定する。次に示す定理は、この構成はリンクが指定する信頼性目標を維持することを表明する。
【０１３１】
定理４．１（ＳｉｍｐｌｅＬｉｎｋ、ＳｉｍｐｌｅＣｏｎｆｉｇに対する確実な安全性）  ＳｉｍｐｌｅＬｉｎｇおよびＳｉｍｐｌｅＣｏｎｆｉｇから生成されたＴｕｌａＦａｌｅスクリプトは、Ｌｏｇ、ＬｏｇＰに対して確実に安全である。
【０１３２】
同様に、次に示す定理も、ＥｎｃＬｉｎｋから生成されたポリシー構成ＥｎｃＣｏｎｆｉｇはＥｎｃＬｉｎｋの秘密目標を維持することを表明する。
【０１３３】
定理４．２（ＥｎｃＬｉｎｋ、ＥｎｃＣｏｎｆｉｇに対する信頼性）  ＥｎｃＬｉｎｋおよびＥｎｃＣｏｎｆｉｇから生成されたＴｕｌａＦａｌｅスクリプトは、ＬｏｇＰ、ＬｏｇＳに対するＢの秘密を維持する。
【０１３４】
ＥｎｃＬｉｎｋはＳｉｍｐｌｅＬｉｎｋよりも極めて強固な仕様なので、ＥｎｃＬｉｎｋおよびＥｎｃＣｏｎｆｉｇから生成されたスクリプトに対して確実な安全性を確立することもできる。次のセクションでは、分析を再び実行せずにこのプロパティを導き出すことのできる、一般的な定理を提示する。
【０１３５】
生成したどちらのスクリプトも、一部のアサーションに対して機能上適切であることを示すことができる。次に示す定理は、ＳｉｍｐｌｅＬｉｎｋおよびＳｉｍｐｌｅＣｏｎｆｉｇから生成されたスクリプトに対してこのプロパティを表明する。  定理４．３（ＳｉｍｐｌｅＬｉｎｋ、ＳｉｍｐｌｅＣｏｎｆｉｇに対する機能上の適切性）  ＳｉｍｐｌｅＬｉｎｋおよびＳｉｍｐｌｅＣｏｎｆｉｇから生成されたＴｕｌａＦａｌｅプロセスがＬｏｇ（ａｓｓ）に対して機能上適切であるようなアサーションａｓｓがある。
【０１３６】
（ポリシーの論理的理論）
前セクションでは、システム１００がリンク仕様１２６に対する固定したポリシー構成１１８の正確さをどのように検証するかを示す例をいくつか示した。しかし、本明細書で図１〜６を参照して説明するシステムおよび方法は、さらに一般的であり、例えば以下で説明するような一般的なクラスのポリシー構成およびリンク仕様に関する定理を表明し、証明するために使用することができる。
【０１３７】
（ポリシーに対する論理的セマンティクス）
セキュリティポリシーを、連結と分離を使用して結合された、微小定理として完全性および信頼性アサーションを有する論理公式として取り扱うことができる。これは、どのようなメッセージでも１つのポリシーを満たすならば別のメッセージも満たすという場合、１つのポリシーが別のポリシーを洗練するという、洗練の自然の概念に繋がる。
【０１３８】
Ｔｕｌａｆａｌｅに対するコンパイルは、論理のモデルを提供する。すなわち、基本公理が当てはまることをチェックすることができ、プロセス構成を完遂することができ（例えば、ポリシーの分離に対するサーバの並列構成の比較）、例えばユーザ名トークンに対する署名および新しい名を共有する複数の署名の推移性のない認証などの、本発明者らのモデルにおいて当てはまる追加規則を明示することもできる。このような論理プロパティは、論理がＷＳポリシーであっても有用である。
【０１３９】
具体的には、ポリシー洗練がセキュリティプロパティの維持に翻訳する場合、ポリシーがセキュリティ目標を満たすことをチェックするために、それが（モデルでは論理的に）、ＴＦを使用してチェック済みのポリシーを洗練することを示すだけで十分である。
【０１４０】
見出し語１（［１］から適用）  ＴｕｌａＦａｌｅスクリプトとして表現されたあるクラスのプロトコルに関して、トップレベルの述部の論理的意味は確実な安全性を維持する。
【０１４１】
見出し語２  ポリシーＰ１がＰ２を洗練する場合、Ｐ１から生成された送信（受信）述部は、Ｐ２から生成された送信（受信）述部を意味する。
【０１４２】
論理洗練は、ポリシー構成に拡張することができる。すなわち、構成Ｃ１が点別にＣ２を洗練する構成Ｃ１´の部分集合である場合、Ｃ１はＣ２を洗練する。
【０１４３】
定理５．１  リンクＬとポリシー構成Ｃがある場合、ＬとＣから生成されたＴｕｌａＦａｌｅスクリプトが確実に安全ならば、Ｃ´がＣを洗練する場合はＬとＣ´から生成されたスクリプトも確実に安全である。
【０１４４】
主要な結果を確立するために、手動証明と自動証明の組み合わせを使用する。
【０１４５】
（リンク生成ポリシー）
リンク仕様によって直接的に生成されたポリシー構成は、常に安全である。これは、次に示す定理により公式化される。
【０１４６】
定理５．２（信頼性）  全てのリンクＬに対して、ＣをＬから生成されたポリシー構成とすると、ＬおよびＣから生成されたＴｕｌａＦａｌｅスクリプトはＬｏｇに対して（インサイダーに対して）確実に安全である。
【０１４７】
定理５．３（セキュリティ）  全てのリンクＬに対して、ＣをＬから生成されたポリシー構成とすると、ＬおよびＣから生成されたＴｕｌａＦａｌｅスクリプトは（インサイダーに対して）Ｂの秘密を維持する。
【０１４８】
定理５．４（機能上の妥当性）  全てのリンクＬに対して、ＣをＬから生成されたポリシー構成とすると、ＬおよびＣから生成されたＴｕｌａＦａｌｅスクリプトは機能上妥当である。
【０１４９】
（リンクおよび送信ポリシー）
構成に対する洗練定理は、送信ポリシーを強化することによってポリシー構成の確実な安全性が維持されることを表明する。場合により、強固な送信ポリシーは、弱いサーバポリシーを補うことさえできる。
【０１５０】
一方、サーバポリシーがリンク仕様を検証するために十分強固な場合、送信ポリシーは信頼性にとって重要ではない。
【０１５１】
定理５．５（信頼性）  いかなるリンクＬの場合でも、ＣをＬから生成されたポリシー構成とし、ＲにＣの受信ポリシーマップを含ませるとする。送信ポリシーマップのいかなる組Ｓに対しても、ＬおよびＳ＠Ｒから生成されたＴｕｌａＦａｌｅスクリプトは確実に安全である。
【０１５２】
反対に、秘密は、次のように送信ポリシーにのみ依存する。
定理５．６（秘密）  いかなるリンクＬの場合でも、ＣをＬから生成されたポリシー構成とし、ＳにＣの全ての受信ポリシーマップを含ませるとする。受信ポリシーマップのいかなる組Ｒに対しても、ＬおよびＳ＠Ｒから生成されたＴｕｌａＦａｌｅスクリプトは秘密を維持する。
【０１５３】
（ウェブサービスに対するセキュリティポリシー生成のための手順例）
図４は、ウェブサービス用のセキュリティポリシーを自動的に生成するための手順例４００を示す。解説のために、この手順の動作は、図１の構成要素に関して解説する。（全ての参照番号は、その構成要素が最初に紹介された図面の番号で始まる）。ブロック４０２で、クライアントサーバ動作環境でネットワーク接続された端点間の保護されたリンクを説明する。この保護されたリンクは、高レベルリンク言語１２６で説明する（図１）。保護されたリンクは、１つまたは複数のセッション中のマシン間におけるメッセージ交換に関するセキュリティ目標を示す。１つのセッションは、クライアントプリンシパルの代わりに動作するクライアントと、サービスプリンシパルの代わりに動作するウェブサービスの間のものである。セキュリティ目標は、メッセージが署名され、暗号化されたことの指示を含むか、または関連付けられた署名を有し、共同してそれぞれのクライアントおよび／またはウェブサービスプリンシパルを認証することができる。セキュリティ目標の信頼性目標は、サービスプリンシパルは、クライアントプリンシパルによって送信された要求メッセージだけを受け入れることを示すか、またはクライアントプリンシパルは、サービスプリンシパルからの応答メッセージだけを受け入れることを示すか、またはいかなるメッセージでも、そのリンクに参加しないクライアントまたはサービスプリンシパルに対して秘密に保つべきであることを示すことができる。
【０１５４】
一実施形態では、複数の保護されたリンクのうちの１つのリンクは、ウェブサービスのＵＲＩ、一組の許可されたアクション、クライアントまたはウェブサービスとして動作することのできる一組のプリンシパルの名、または１つまたは複数のセッションでのマシン間におけるメッセージ交換の秘密レベルを示す。１つのセッションは、要求と応答の交換を含む。このセッションは、クライアントとサーバの間での保護された複数メッセージの対話であってよい。
【０１５５】
ブロック４０２の動作は、受信ポリシーによるサービス構成と送信構成を含めて、セキュリティポリシー構成に対する、抽象的な固定アルゴリズム構文を消費するステップを含むことができる。受信ポリシーは、アクション、クライアントプリンシパル、またはサーバプリンシパルに対応する。送信構成は、クライアントプリンシパルおよびサーバプリンシパルの各対に対応する。ブロック４０２の動作は、セキュリティポリシー構成に対する、抽象的な固定アルゴリズム構文を消費することも含むことができる。ここで、その構成は、ウェブサービスのクライアント装置に関して送信要求ポリシーと受信応答ポリシーを含む。
【０１５６】
ブロック４０４で、生成モジュール１２４は、リンク言語１２６から構成データ１１８を自動的に生成する。構成データは、ランタイム１１２によって使用されるセキュリティプロトコルに関連付けられた宣言型保護ポリシーを含む。構成データは、サーバがサポートするアクションにおけるサービスおよびクライアントとサーバの間の信頼関係の指示を、さらに含むことができる。構成データに関するさらなる形態は、図５を参照して後述する分散型システムのセキュリティ目標をチェックするための手順例で説明する。
【０１５７】
（分散型システムのセキュリティ目標をチェックするための手順例）
図５は、ウェブサービス構成のセキュリティをチェックするための手順例５００を示す。解説のために、手順５００の動作は、図１の構成要素に関して説明する。（全ての参照番号は、その構成要素が最初に紹介された図面の番号で始まる）。ブロック５０２で、解析モジュール１１４（図１）は、構成データ１１８内の情報をモデル１２２に翻訳する。構成データは、ランタイム１１２が実施するセキュリティプロトコルに関連付けられた宣言型セキュリティポリシーを含む。宣言型セキュリティポリシーに対する一実施形態は、基礎的アサーションに関する論理公式を含む。モデル１２２は、分散型コンピューティングシステム１００（図１）のコンピューティング装置間で伝達されるメッセージのフィルタリングおよび処理を表す述部を含む。
【０１５８】
一実施形態では、構成データ１１８は、図４を参照して上記で説明される手順例により生成される。
【０１５９】
ブロック５０４で、チェッカーモジュール１１６は、ランタイム１１２の宣言型セキュリティポリシーがシステム１００のセキュリティ目標を実現するか否かを判定するために、モデル１２２を評価する。この評価動作は、宣言型セキュリティポリシーが書換え攻撃に対して脆弱か否かを自動的に判定するステップを含む。ブロック５０６で、チェッカーモジュール１１６は、分散型システム１００がモデルの評価に鑑みてセキュリティ攻撃に対して脆弱か否かを判定する。
【０１６０】
一実施形態では、構成データ１１８は、第１および第２のコンピュータプログラムアプリケーションに関連付けられたセキュリティ設定に対応する。この実施形態では、ブロック５０２から５０６の動作は、セキュリティ攻撃に対するシステム１００の脆弱性の静的分析またはランタイム分析の一部として実行される。
（動作環境例）
ウェブサービスに対するセキュリティポリシーの生成を自動的にチェックし、またウェブサービス構成のセキュリティをチェックするためのシステムおよび方法を、パーソナルコンピュータが実行中のコンピュータ実行可能命令（プログラムモジュール）の一般的な状況で説明する。プログラムモジュールは、一般的に、特定のタスクを実行するか、または特定の抽象データタイプを実施するルーチン、プログラム、オブジェクト、構成要素、データ構造などを含む。このシステムおよび方法は上記の状況で説明するが、以下で説明する行為および動作は、ハードウェアで実施することもできる。
【０１６１】
図６は、ウェブサービスに対してセキュリティポリシーを自動的に生成し、ウェブサービス構成のセキュリティをチェックするシステムおよび方法が、例えば図１〜６に示し、それらを参照して説明したように、完全にまたは部分的に実施することのできる、適切なコンピューティング環境例を示す。コンピューティング環境６００例は、適切なコンピューティング環境の一例に過ぎず、本明細書に記載のシステムおよび方法の用途または機能性の範囲に関していかなる限定をも示唆することを目的としない。また、コンピューティング環境６００は、コンピューティング環境６００に示す構成要素のどれか１つまたはそれらの組み合わせに関する依存または要件を有するものとも解釈されるべきではない。
【０１６２】
本明細書に記載の方法およびシステムは、多数の他の汎用または専用コンピューティングシステム環境または構成で動作可能である。使用に適した、良く知られたコンピューティングシステム、環境、および／または構成の例には、限定はしないが、パーソナルコンピュータ、サーバコンピュータ、マルチプロセッサシステム、マイクロプロセッサベースのシステム、ネットワークＰＣ、ミニコンピュータ、メインフレームコンピュータ、上記システムまたは装置のどれかを含む分散型コンピューティング環境などが含まれる。この枠組みのコンパクトまたはサブセットバージョンは、手持ち式コンピュータまたは他のコンピューティング装置のような限定された資源のクライアントでも実施することができる。本発明は、通信ネットワークを介してリンクされる遠隔処理装置によってタスクが実行される、分散型コンピューティング環境で実施される。分散型コンピューティング環境では、プログラムモジュールは、ローカルおよび遠隔記憶装置の両方に配置することができる。
【０１６３】
図６を参照して、ウェブサービス構成のセキュリティをチェックするためのシステム例は、コンピュータ６１０の形式で汎用コンピューティング装置を含む。コンピュータ６１０の次に説明する形態は、図１のコンピューティング装置１０２および／または１０４の実施形態例である。コンピュータ６１０の構成要素は、限定はしないが、１つ以上の処理装置６２０、システムメモリ６３０、およびシステムメモリを含めて様々なシステム構成要素を処理装置６２０に結合するシステムバス６２１を含むことができる。システムバス６２１は、メモリバスまたはメモリコントローラ、周辺バス、および様々なバスアーキテクチャのどれかを使用するローカルバスを含めて、数種類のバス構造のどれであってもよい。限定ではなく一例として、そのようなアーキテクチャは、業界標準アーキテクチャ（ＩＳＡ）バス、マイクロチャネルアーキテクチャ（ＭＣＡ）バス、拡張ＩＳＡ（ＥＩＳＡ）バス、ビデオ電子標準化協会（ＶＥＳＡ）ローカルバス、およびメザニンバスとしても知られる周辺装置相互接続（ＰＣＩ）バスを含むことができる。
【０１６４】
コンピュータ６１０は、通常、様々なコンピュータ可読媒体を含む。コンピュータ可読媒体は、コンピュータ６１０によってアクセス可能な、いかなる使用可能な媒体であってもよく、揮発性および不揮発性媒体、取り外し可能および取り外し不可能な媒体の両方を含む。限定ではなく一例として、コンピュータ可読媒体は、コンピュータ記憶媒体と通信媒体を含むことができる。コンピュータ記憶媒体は、コンピュータ可読命令、データ構造、プログラムモジュールまたは他のデータのような情報を記憶するためのいかなる方法または技術でも実施される、揮発性および不揮発性の取り外し可能および取り外し不可能な媒体を含む。コンピュータ記録媒体は、限定ではないが、ＲＡＭ、ＲＯＭ、ＥＥＰＲＯＭ、フラッシュメモリまたは他のメモリ技術、ＣＤ−ＲＯＭ、デジタル多用途ディスク（ＤＶＤ）または他の光ディスク記憶装置、磁気カセット、磁気テープ、磁気ディスク記憶装置または他の磁気記憶装置、または所望の情報を記憶するために使用することができ、コンピュータ６１０によってアクセス可能な任意の他の媒体を含む。
【０１６５】
通信媒体は、通常、コンピュータ可読命令、データ構造、プログラムモジュールまたは他のデータを、搬送波のような変調されたデータ信号または他の搬送機構で実施され、いかなる情報配信媒体をも含む。「変調されたデータ信号」という用語は、その特徴セットの１つまたは複数を有し、または情報を信号に符号化するそのような方法で変更された信号を意味する。限定ではなく一例として、通信媒体は、有線ネットワークまたは直接配線接続のような有線媒体と、アコースティック、ＲＦ、赤外線および他の無線媒体のような無線媒体とを含む。上記のどれとどれの組み合わせでも、コンピュータ可読媒体の範囲に含まれるべきである。
【０１６６】
システムメモリ６３０は、読み出し専用メモリ（ＲＯＭ）６３１およびランダムアクセスメモリ（ＲＡＭ）６３２のような、揮発性および／または不揮発性メモリの形式によるコンピュータ記憶媒体を含む。起動時などに、コンピュータ６１０内の素子間で情報を転送するために役立つ基本ルーチンを含む、基本入出力システム６３３（ＢＩＯＳ）は、通常、ＲＯＭ  ６３１に記憶される。ＲＡＭ  ６３２は、通常、処理装置６２０に即座にアクセス可能であり、かつ／または処理装置６２０によって現在操作を受けているデータおよび／またはプログラムモジュールを含む。限定ではなく一例として、図６は、オペレーティングシステム６３４、アプリケーションプログラム６３５、他のプログラムモジュール６３６、およびプログラムデータ６３８を示す。一実施形態では、アプリケーションプログラム６３５は、例えば図１のプログラムモジュール１０８と、プリンシパルの代わりにＳＯＡＰエンベロープを送信し、受信するための、「プロセッサ」（アプリケーション）のような他のコンピュータプログラムモジュールを含む。プログラムデータ６３８は、例えば図１のプログラムデータ１１０を含む。
【０１６７】
コンピュータ６１０は、他の取り外し可能／取り外し不可能な揮発性／不揮発性コンピュータ記憶媒体も含むことができる。一例としてのみ、図６は、取り外し不可能な不揮発性磁気媒体から読み出し／に書き込むハードディスクドライブ６４１と、取り外し可能な不揮発性磁気ディスク６５２から読み出し／に書き込む磁気ディスクドライブ６５１と、ＣＤ  ＲＯＭまたは他の光媒体のような取り外し可能な不揮発性光ディスク６５６から読み出し／に書き込む光ディスクドライブ６５５とを示す。動作環境例で使用可能な他の取り外し可能／取り外し不可能な揮発性／不揮発性コンピュータ記憶媒体は、限定ではないが、磁気テープカセット、フラッシュメモリカード、デジタル多用途ディスク、デジタルビデオテープ、固体ＲＡＭ、固体ＲＯＭなどを含む。ハードディスクドライブ６４１は、通常、インターフェース６４０のような取り外し不可能なメモリインターフェースを介してシステムバス６２１に接続され、磁気ディスクドライブ６５１および光ディスクドライブ６５５は、通常、インターフェース６５０のような取り外し可能なメモリインターフェースによってシステムバス６２１に接続される。
【０１６８】
上記で説明し図６に示したこれらドライブおよびそれらの関連付けられたコンピュータ記憶媒体は、コンピュータ可読命令、データ構造、プログラムモジュール、および他のデータの記憶域をコンピュータ６１０に提供する。図６では、例えば、ハードディスクドライブ６４１は、オペレーティングシステム６４４、アプリケーションプログラム６４５、他のプログラムモジュール６４６、およびプログラムデータ６４８を記憶するように示されている。これらの構成要素は、オペレーティングシステム６３４、アプリケーションプログラム６３５、他のプログラムモジュール６３６、およびプログラムデータ６３８と同じであっても、異なるものであってもよいということに留意されたい。オペレーティングシステム６４４、アプリケーションプログラム６４５、他のプログラムモジュール６４６、およびプログラムデータ６４８には、これらが少なくとも別物であることを示すために、本明細書では異なる番号を付した。
【０１６９】
ユーザは、コマンドおよび情報を、キーボード６６２および一般にマウス、トラックボールまたはタッチパッドと呼ばれるポインティング装置６６１のような入力装置によってコンピュータ６１０に入力することができる。他の入力装置（図示せず）は、マイクロフォン、ジョイスティック、ゲームパッド、衛星放送用受信アンテナ、スキャナなどを含むことができる。これらおよび他の入力装置は、システムバス６２１に結合されたユーザ入力インターフェース６６０を介して処理装置６２０に接続されることがしばしばであるが、パラレルポート、ゲームポートまたはユニバーサルシリアルバス（ＵＳＢ）のような他のインターフェースおよびバス構造によって接続することもできる。
【０１７０】
モニタ６９１または他のタイプの表示装置も、ビデオインターフェース６９０のようなインターフェースを介してシステムバス６２１に接続される。モニタに加えて、コンピュータは、出力周辺インターフェース６９５を介して接続可能な、スピーカ６９８およびプリンタ６９６のような他の周辺出力装置を含むこともできる。
【０１７１】
コンピュータ６１０は、遠隔コンピュータ６８０のような１つまたは複数の遠隔コンピュータに対する論理接続を使用してネットワーク接続された環境で動作する。遠隔コンピュータ６８０は、パーソナルコンピュータ、サーバ、ルータ、ネットワークＰＣ、ピア装置または他の共通ネットワークノードであってよく、その特定の実施形態の機能に応じて、コンピュータ６１０に関して上記で説明した多くの要素または全ての要素を含むことができるが、図６には記憶装置６８１しか示さない。図６に示した論理接続は、ローカルエリアネットワーク（ＬＡＮ）６８１と広域ネットワーク（ＷＡＮ）６８３とを含むが、他のネットワークを含んでもよい。このようなネットワーク接続環境は、オフィス、企業規模コンピュータネットワーク、イントラネットおよびインターネットでは一般的なものである。
【０１７２】
ＬＡＮネットワーク接続環境で使用される場合、コンピュータ６１０はネットワークインターフェースまたはアダプタ６８０を介してＬＡＮ６８１に接続される。ＷＡＮネットワーク接続環境で使用される場合、コンピュータ６１０は、通常、モデム６８２またはインターネットのようなＷＡＮ６８３を介した通信を確立するための他の手段を含む。内蔵型であっても外付けであってもよいモデム６８２は、ユーザ入力インターフェース６６０または他の適切な機構を介してシステムバス６２１に接続することができる。ネットワーク接続環境では、コンピュータ６１０に関して図示したプログラムモジュールまたはその一部は、遠隔記憶装置に記憶することができる。限定ではなく一例として、図６は、遠隔アプリケーションプログラム６８５がメモリ装置６８１に常駐するように示している。図示したネットワーク接続は一例であり、コンピュータ間に通信リンクを確立する他の手段を使用することもできる。
【０１７３】
（開発ツールの完全性の例）
上記に鑑みて、図１〜６のシステムおよび方法は、安全な／信頼できるコンピューティングを提供する。このようなコンピューティングは、例えば、次に示すシステム１００分析動作を含むことができる。
・  静的単集合分析−単一プロジェクトおよびそれに関連付けられたサポートデータがある場合、所望のセキュリティ目標を満たすことができるか否かを判定し、機能停止または他の勧告を特定する。これは、サービスに対する明らかな攻撃を特定する。
・  静的グループ分析−２つ（またはそれ以上の）プロジェクトおよびそれらに関連付けられたサポートデータがある場合、所望のセキュリティ目標を満たすことができるか否かを判定し、機能停止または他の勧告を特定する。これは、別のプロジェクトを傷つけるために１つのプロジェクトを使用する間接的な攻撃のような、さらなる攻撃を特定する。
・  動的分析−あるサービスが別のサービスに接続しようとする際、そのサービスに対するサポートデータがリアルタイムで取得され（可能ならば、キャッシュから、または補助プロトコルを使用して）、その通信がｈａｖｅｄ目標を満たすか否かに関してセキュリティ評価が行われる。満たさない場合、例外を投入することができるか、またはそのコールをブロックすることができる。この分析は、異なる場所で起こる場合があり、２つの実施形態は、ＣＬＲランタイムおよび通信基盤を含む。
【０１７４】
これらの例およびサポートデータは変更されうる。サポートデータは、例えば、コード注釈、コード分析の結果、セキュリティデータ、構成情報、ポリシー情報、周知のサービス分析のライブラリ、周知の攻撃および攻撃パターンのライブラリなどを含む。データが多いほど、（通例として）評価は正確になるが、システム１００は、使用可能なデータがある場合に最高の評価を行い、またはデータの欠如に基づいてその評価を低くするように構成することができる。また、使用可能なデータの一部しか信頼できない場合がある。これらの場合、安全な評価が使用可能な／限定されたデータにより行われる。
【０１７５】
（代替形態−ポリシーアドバイザー例）
所与の構成１１８によって実現されたセキュリティ保証は、理解し難いものである。例えば、ＷＳＥ構成およびポリシーファイルは、主としてそれらの保証を特定するが、正確である可能性は低い。手書きのＷＳＥポリシーサンプルの内部セキュリティレビューは、僅かなエラーの範囲を示している。これに対処するために、システム１００は、ポリシーの集合が提供する肯定的セキュリティ保証に関する解説と、潜在的セキュリティ脆弱性に関するアドバイスの両方を提供するために、ポリシーアドバイザーを提供する。一実施形態では、ポリシーアドバイザーは、チェッカーモジュール１１６のそれぞれの部分である。別の実施形態では、ポリシーアドバイザーは「他のプログラムモジュール」１２０として示される。
【０１７６】
ポリシーアドバイザーは、どの要素が認証され暗号化されるかに関して、例えば各端点でエクスポートされる１つ以上のアクション、各アクションを目標とする方法およびポリシー、およびポリシーの要約のリストを含む、肯定的報告を生成する。肯定的表明は、例えば特定の脅威モデルなどに対して特定の状況でのみ適用されるか否かを示す。（肯定的報告に関するさらなる情報については、段落［０１６５］を参照されたい）。ポリシーアドバイザーは、例えばある種のヘッダーの署名またはチェックの失敗、メッセージ、共通の入力ミスなどをそれらの脆弱性の訂正方法に関するある種のアドバイスに関連付けることの失敗の指示を含む、否定的報告も生成する。潜在的脆弱性の報告は、提案された解決策を含む。すなわち、アドバイザーは、ウェブアプリケーションに対する既存の侵入ツールのＳＯＡＰへのいかなる拡張に対する防御でもある。説明のために、肯定的報告と否定的報告とを、「他のデータ」１２７のそれぞれの部分として示す。
【０１７７】
ポリシーアドバイザーは、構成１１８、ポリシーファイルのモデル１２２、またはポリシーファイルを表現するある種の他のオブジェクトに対して静的に実行される。説明のために、そのような他のオブジェクトは「他のデータ」１２７のそれぞれの部分によって表現される。そのような実行中、ポリシーアドバイザーは、ローカル証明書ストアおよびいかなる使用可能なメッセージログのような、他のデータ１２７を参照することができる。
【０１７８】
一実施形態では、ポリシーアドバイザーは開発業者、検査員、またはＷＳＥインストールのオペレータが使用するためのものである。例えば、修正した構成を製品に配置する前などに、設計者が異なるＷＳＥ設定を試みる際の即時フィードバックを提供する方法として、開発中のデバッグプロセスの一部として、および／またはセキュリティ評価および確認の一部として、このポリシーアドバイザーを設計プロセスの初期で使用することができる。一実施形態では、このポリシーアドバイザーは、新しい問題が検出された場合に、自動的に（かつ可能ならば遠隔に）チェックを実行し、アラートをトリガするためなどに、１つまたは複数のアプリケーションプログラミングインターフェース（ＡＰＩ）を公開する。一実施形態では、ポリシーアドバイザーは図形的な分散型システムデザイナーと統合される。
【０１７９】
（ポリシーアドバイザーアーキテクチャ例）
図７は、ポリシーアドバイザーのアーキテクチャ例を示す。解説のために、図７の構成要素は図１の構成要素を参照して説明する。図面では、構成要素の参照番号の一番左の数字は、最初にその構成要素が表示された特定の図を示す。例えば、ブロック７０２は、プログラムモジュール１２０にマッピングするポリシーアドバイザーを表す。コマンド行クライアント７０４とＡＳＰ．ＮＥＴウェブサービス７０６は、ポリシーアドバイザーが分析中の構成データ１１８を表す。ポリシーアドバイザーは、サーバ１０２とクライアント１０６それぞれの構成要素に対するアプリケーションについて、分散型システム１００のサーバ１０２とクライアント１０６に対して実行することのできる構成要素である。
【０１８０】
図７を参照すると、ポリシーアドバイザーは、ＷＳＥインストールを判定することのできるものを反映するように構築した内部データ構造（ブロック７０４の動作と図１の「他のデータ」のそれぞれの部分によって表される）に対して実行される照会のライブラリ７０８によってパラメータ化される。各照会は、優先され、関連する端点、アクションおよびウェブメソッドと相互に関係付けることのできる、ポリシーに関する１つ以上の肯定的または否定的報告／アドバイスを作成することができる。一般に、入力は、ＷＳＥを使用して実施される１つまたは複数のＳＯＡＰノードに関連付けられた、次に示すドット付きリストのタイプである。それら入力の一部は、ウェブサーバディレクトリツリーから、または双方向開発環境（ＩＤＥ）のプロジェクトファイルから収集することができる。次に示すリストに一部が示されているそれら入力の大部分は、任意選択であり、ポリシーアドバイザーは、使用可能な入力から可能な限り正確な報告を提供する。最も基本的なモードは、構成１１８またはモデル１２２の単一のＰｏｌｉｃｙＣａｃｈｅファイル（以下のドット付き項目の３を参照されたい）を分析するためのものである。
・  各ウェブサービスに対するＷｅｂ．ｃｏｎｆｉｇファイル
・  各コマンド行またはウィンドウズ（登録商標）アプリケーションに対するＡｐｐ．ｃｏｎｆｉｇファイル
・  ポリシーを含むＰｏｌｉｃｙＣａｃｈｅファイル
・  ウェブサービスの各アクションに対応するソースコードの判定基準となる、ウェブサービスに対するＡｓｍｘおよびＤＬＬファイル
・  クライアントに知られているノードの判定基準となる、ウェブサービスクライアントに対するＥｘｅファイル
・  入来および発信ＳＯＡＰメッセージの追跡を含んだファイル（通常、．ｗｅｂｉｎｆｏ）
・  チェックのために使用可能な主題名などの判定基準となりうる、ローカルにインストールされたＸ．５０９証明書、および／または
・  セキュリティ設定ツールによって収集され、ポリシーを生成するために使用されるパラメータ
【０１８１】
（照会例）
照会は、単純な構文チェックからさらに高度な妥当性検査まで、図７のボックス７０８に示す６つのカテゴリにグループ化される。一実施形態では、それらの照会のどれかが、実際には何も不正ではないのに「擬似肯定」を生成した場合、システム１００は、それらをチェックした後でユーザが擬似肯定を抑えるように単純なＵＩを提供する。これら６つのカテゴリを次に示す。
・  スキーマおよび範囲制限に関する照会（表１）
・  各ノード構成に関する照会（表２）
・  ポリシー発送に関する照会（表３）
・  各ポリシーに関する照会（表４および５）
・  ポリシー互換性に関する照会、および
・  カスタム照会
【０１８２】
表１は、ポリシーアドバイザーが使用するためのスキーマチェックおよび識別子の範囲制限に関する照会例を示す。
【０１８３】
【表２６】
2005322234.tif 000028
【０１８４】
【表２７】
2005322234.tif 000029
【０１８５】
【表２８】
2005322234.tif 000030
【０１８６】
【表２９】
2005322234.tif 000031
【０１８７】
表４の照会（個別ポリシーに関する照会）について、システム１００は、各３項目（要求、応答、障害）のメッセージパターンを次に示すように分類する。
・  そのｒｅｑｕｅｓｔＡｃｔｉｏｎが「ＲＳＴ／ＳＣＴ」である場合、それはＲＳＴ／ＲＳＴＲハンドシェークについて適用する
・  そうではなく応答がエンプティである場合、それは単発メッセージについて適用する
・  そうではない場合、それはＲＰＣハンドシェークについて適用する
【０１８８】
各３項目（要求、応答、障害）に対して、ポリシーアドバイザーは、その分類と、次に続く推奨からのいかなる逸脱をも報告する。単発メッセージの場合、ポリシーアドバイザーはＲｅｑｕｅｓｔ列を適用する。これ以外の場合、ポリシーアドバイザーは、ＲｅｑｕｅｓｔおよびＲｅｓｐｏｎｓｅ／Ｆａｕｌｔ列の両方を適用する。行Ｈ、列Ｐの下のＸは、ヘッダーＨが要素Ｐに含まれるべきであることを意味するが、そうでないならば、エラーある。一方、全てのＨが満たされている場合、少なくともインサイダー攻撃がないならば、メッセージパターンに対する相関関係により合意が達成されるべきである。
【０１８９】
【表３０−１】
2005322234.tif 000032
【０１９０】
【表３０−２】
2005322234.tif 000033
【０１９１】
ポリシー互換性に関する照会について、システム１００は、
・  任意の接続された２つの端点に対するポリシーの交点を計算し、それらの交点のプロパティを表明する。
・  互換性のないクライアントおよびサービスポリシーを警告する、かつ／または
・  編集されたポリシーを警告し、それらがポリシー生成中に収集されたセキュリティ目的を提供し続けるか否かをチェックする。
【０１９２】
カスタム照会について、システム１００は、
・  ある種のヘッダーを含めることを命令するため、またはある種のアルゴリズムに反対するために、カスタム照会を定義する構成、および／または
・  ログファイル内の個人特定情報（ＰＩＩ）を検出するためのプライバシーツール、例えば＜Ｐａｓｓｗｏｒｄ＞などの実行、
を可能にする。この実施形態では、ポリシーアドバイザーは、ユーザ名または証明書の主題として識別情報を開示するようなセキュリティヘッダー内のプライバシー問題を警告する。
【０１９３】
（肯定的報告例）
潜在的エラーを報告する照会に加え、ポリシーアドバイザーは、人間のユーザがその含意を理解し、エラーになりうる不規則性を突き止めるために役立つように陽性報告を作成するために、構成データ１１８を要約する。一実施形態では、ポリシーアドバイザーは、例えば次に示す項目の１つまたは複数を実行する。
・  ポリシーファイルの周知の端点およびアクションと、明示的に割り当てられるかディフォルトで割り当てられたポリシーを表示する。さらに、ポリシーアドバイザーは、メッセージ追跡により何が実行されたかも表示する。
・  追跡中に、メッセージの、署名され、暗号化された部分を強調表示する。
・  各メッセージが受け入れられた後で、端点およびアクションごとに、送信側と受信側の間でどのような合意が保たれるかの肯定的な表明を提供する。合意は、次のようないくつかの機構から続けることができる。
【０１９４】
要求を受け入れた後で、その要求の署名された内容に関する合意がある場合がある（すなわち、署名された要素と、その署名者の識別情報）。
【０１９５】
要求に対する応答を受け入れた後で、その応答の署名された内容と、相互に適切に関係付けられる場合はその要求の署名された内容と、に関する合意がある場合がある。
【０１９６】
ＲＳＴ／ＲＴＳＲハンドシェークによって確立されたセキュリティ状況がある場合、送信および受信されたメッセージの署名された内容と、さらにセキュリティ状況（送信側および受信側の識別情報を含む場合がある）とに関する合意がある場合がある。
・  メッセージ追跡中に発生するいかなる非標準ヘッダーを、それらが署名されているか暗号化されているかの指示と共に報告する。
・  メッセージ追跡中またはポリシーファイル内の全ての「識別情報」、例えば主題名、キー識別子、ユーザ名などを報告する。
【０１９７】
（ポリシーアドバイザー出力例）
表６は、入来メッセージ１３２の署名および暗号化を要求する単純なポリシーで構成されたサーバ１０２で実行される場合の、ポリシーアドバイザーの出力例を示す。
【０１９８】
表６
個別ポリシーに関する他の照会例
次に示すウェブメソッドをエクスポートする、マシンＭＳＲＣ−ＸＸＸのローカル構成に関する報告（．．．）。
・  サービスhttp://server/MyApp/MyAppService.asmxは、カスタムトークンマネージャＵｓｅｒｎａｍｅＳｉｇｎＰｏｌｉｃｙＳｅｒｖｉｃｅ．ＣｕｓｔｏｍＵｓｅｒｎａｍｅＴｏｋｅｎＭａｎａｇｅｒを使用する。
？  このクラスは、パスワード妥当性検査に関して完全な制御を有する
・  ディフォルト“ヌル”ポリシーは、http://server/MyApp/MyAppService.asmxおよびアクションhttp://contoso.com/MyRequestに送信されたメッセージに関する応答および障害メッセージについて適用する。
−  これらのメッセージは署名も暗号化もされていない。
−  誰もこれらのメッセージを偽造することはできない。
・  ｓｅｒｖｅｒＰｏｌｉｃｙＣａｃｈｅ．ｘｍｌの行１３のユーザ名−トークン−署名済み−ｘ５０９−暗号化済みポリシーは、アクションhttp://contoso/com/MyRequestでhttp://server/MyApp/MyAppservice.asmxに送信された要求メッセージについて適用し、ＭｙＡｐｐＳｅｒｖｉｃｅ．ａｓｍｘ．ｃｓの行８２でウェブメソッドＭｙＲｅｑｕｅｓｔを呼び起こす。
＋  ウェブメソッド引数を含む本体が署名される。
＋  ウェブメソッド引数を含む本体が暗号化される。
−  重要なヘッダー（＜Ｔｏ＞，＜Ａｃｔｉｏｎ＞）は任意選択であり、存在する場合だけ署名される。
−  ユーザ名トークンは暗号化されておらず、個人識別子を盗聴者に漏洩する危険性がある。−サンプルメッセージを参照のこと。
＋  ＜Ｃｒｅａｔｅｄ＞タイムスタンプは署名されている。
−  要求は、過去５分間に処理済みの要求の応答である場合がある。−署名された＜Ｃｒｅａｔｅｄ＞および＜ＭｅｓｓａｇｅＩｄ＞要素を使用して再生を防止する方法に関しては、ＷＳＥサンプルを参照されたい。
−  要求は暗号化されているが、応答は暗号化されていない。応答本体は、要求からの機密データを漏洩する危険性がある。
−  応答は署名されていないので、応答と要求を相互に関係付けることはできない。
【０１９９】
（結論）
ウェブサービス構成のセキュリティをチェックするシステムおよび方法を、構造上の特徴および／または方法上の動作またはアクションに特有の言語で説明したが、首記の特許請求の範囲で定義される実施形態は、説明されたその特有の特徴またはアクションに必ずしも限定されるものではないということが理解されよう。例えば、一実施形態では、モデル１２２はモデルとして記載される（例えば、ＴｕｌａＦａｌｅスクリプティングを使用して）。したがって、この特有の特徴およびアクションは、特許請求の対象を実施する形式例として開示されるものである。
【０２００】
（付録Ａ）
【０２０１】
【表３１】
2005322234.tif 000034
【０２０２】
【表３２】
2005322234.tif 000035
【０２０３】
【表３３】
2005322234.tif 000036
【０２０４】
【表３４】
2005322234.tif 000037
【０２０５】
【表３５】
2005322234.tif 000038
【０２０６】
（付録Ｂ）
【０２０７】
【表３６】
2005322234.tif 000039
【０２０８】
【表３７】
2005322234.tif 000040
【０２０９】
【表３８】
2005322234.tif 000041
【０２１０】
（付録Ｃ）
【０２１１】
【表３９】
2005322234.tif 000042
【０２１２】
【表４０】
2005322234.tif 000043
【０２１３】
【表４１】
2005322234.tif 000044
【０２１４】
（付録Ｄ）
【０２１５】
【表４２】
2005322234.tif 000045
【０２１６】
【表４３】
2005322234.tif 000046
【０２１７】
（付録Ｅ）
【０２１８】
【表４４】
2005322234.tif 000047
【０２１９】
【表４５】
2005322234.tif 000048
【０２２０】
【表４６】
2005322234.tif 000049
【０２２１】
【表４７】
2005322234.tif 000050
【０２２２】
【表４８】
2005322234.tif 000051
【０２２３】
【表４９】
2005322234.tif 000052
【図面の簡単な説明】
【０２２４】
【図１】ウェブサービス用のセキュリティポリシーを自動的に生成し、ウェブサービス構成のセキュリティをチェックするためのコンピューティング装置例を示す図である。
【図２】ウェブサービス構成のセキュリティをチェックするためにシステム記述を分析する際のデータフロー例を示す図である。
【図３】ウェブサービス構成のセキュリティをチェックするための、構成データファイル生成およびセキュリティポリシー分析のためのデータフロー例を示す図である。
【図４】ウェブサービス用のセキュリティポリシーを自動的に生成するための手順例を示す図である。
【図５】ウェブサービス構成のセキュリティをチェックするための手順例を示す図である。
【図６】ウェブサービス用のセキュリティポリシーを自動的に生成し、ウェブサービス構成のセキュリティをチェックするための、前述のシステム、装置および方法を完全にまたは一部実施することのできる、適切なコンピューティング環境例を示す図である。
【図７】ポリシーアドバイザーアーキテクチャ例を示す図である。
【符号の説明】
【０２２５】
１００  システム
１０６  ネットワーク
１３０、１３２  ＳＯＡＰエンベロープ
【図１】
2005322234.tif 000053
【図２】
2005322234.tif 000054
【図３】
2005322234.tif 000055
【図４】
2005322234.tif 000056
【図５】
2005322234.tif 000057
【図６】
2005322234.tif 000058
【図７】
2005322234.tif 000059
【外国語明細書】
2005322234000001.pdf