(57)【特許請求の範囲】
【請求項１】
コンピュータシステムによる方法であって、
前記コンピュータシステムが、１つ以上の抽象化を有するサーバサイドプログラムを生成するステップと、
前記コンピュータシステムが、前記１つ以上の抽象化を含む前記サーバサイドプログラムをセキュリティ基準に関して安全な方法で実行するように保証される目的コードに変換することによって、前記サーバサイドプログラムをコンパイルするステップと、を含み、
前記１つ以上の抽象化が、ウェブ入力抽象化、セッション管理抽象化、状態保持抽象化、および、履歴管理抽象化から構成される群からの１つ以上の抽象化を含み、前記ウェブ入力抽象化が、ウェブ入力から取得された値が良好にタイプされるものかどうかチェックするコマンドを含み、前記セッション管理抽象化が、プログラム状態をウェブインタラクションにわたって保持するコマンドを含み、前記状態保持抽象化が、目的コードのプログラムインスタンスを１つのクライアントのみにアクセスを許可するようにし、プログラムインスタンスの状態に影響を及ぼすコマンドを含み、前記履歴管理抽象化が、クライアント履歴の一部を削除する履歴管理コマンドを含み、
前記サーバサイドプログラムをコンパイルするステップが、コンパイル中に前記セキュリティ基準を強制実行するようにセキュリティ検査を挿入する工程を備える、方法。
【請求項２】
前記変換された抽象化が、前記目的コードが履歴管理において対応するコマンドを実行した場合に、将来の演算において処理するためのクライアント履歴におけるエントリを前記目的コードに受理させないことを実現させるためのものである、請求項１に記載の方法。
【請求項３】
前記１つ以上の抽象化が、少なくとも１つのドメイン固有言語の抽象化を含む、請求項１に記載の方法。
【請求項４】
前記１つ以上の抽象化が、悪用防止抽象化を含む、請求項１に記載の方法。
【請求項５】
前記ウェブ入力抽象化が、ユーザリクエストを受信するためのサービスインターフェースを暗に開くフォーム構成を含む、請求項１に記載の方法。
【請求項６】
前記フォーム構成が、エラーが発生される前に１回のみ前記サービスインターフェースが開かれる単一使用モード、または、前記サービスインターフェースが将来のリクエストのために開いたままである複数使用モードを指定することを実現させるためのものである、請求項５に記載の方法。
【請求項７】
前記フォーム構成が、引数としてＨＴＭＬ文書を取ることを実現させるためのものである、請求項５に記載の方法。
【請求項８】
前記フォーム構成が、ＨＴＭＬページをクライアントに提示し、前記ＨＴＭＬページに対するレスポンスにおいて前記クライアントから入力を取得することを実現させるためのものである、請求項５に記載の方法。
【請求項９】
前記サーバサイドプログラムがウェブプログラムであり、前記１つ以上の抽象化が、ウェブ入力、セッション管理、状態保持、履歴管理、および、悪用防止における抽象化の集合を含む、請求項１に記載の方法。
【請求項１０】
前記１つ以上の抽象化が、少なくとも１つのスクリプトを含む、請求項１に記載の方法。
【請求項１１】
サーバサイドプログラムを生成するステップが、前から存在するサーバプログラムに前記１つ以上の抽象化を挿入する工程を備える、請求項１に記載の方法。
【請求項１２】
前記サーバサイドプログラムがウェブプログラムを含む、請求項１に記載の方法。
【請求項１３】
前記サーバサイドプログラムをコンパイルするステップが、保持されている１つ以上のクライアントサイド状態が除去されることを引き起こすための１つ以上のプリミティブを追加する工程を備える、請求項１に記載の方法。
【請求項１４】
コンピュータシステムによって実行された場合に、
１つ以上の抽象化を有するサーバサイドプログラムを生成するステップと、
前記１つ以上の抽象化を含む前記サーバサイドプログラムをセキュリティ基準に関して安全な方法で実行するように保証される目的コードに変換することによって、前記サーバサイドプログラムをコンパイルするステップと、
を前記コンピュータシステムに実行させる命令を記憶する１つ以上の非一時的かつコンピュータ読み取り可能な記憶媒体であって、
前記１つ以上の抽象化が、ウェブ入力抽象化、セッション管理抽象化、状態保持抽象化、および、履歴管理抽象化から構成される群からの１つ以上の抽象化を含み、前記ウェブ入力抽象化が、ウェブ入力から取得された値が良好にタイプされるものかどうかチェックするコマンドを含み、前記セッション管理抽象化が、プログラム状態をウェブインタラクションにわたって保持するコマンドを含み、前記状態保持抽象化が、目的コードのプログラムインスタンスを１つのクライアントのみにアクセスを許可するようにし、プログラムインスタンスの状態に影響を及ぼすコマンドを含み、前記履歴管理抽象化が、クライアント履歴の一部を削除する履歴管理コマンドを含み、
前記サーバサイドプログラムをコンパイルするステップが、コンパイル中に前記セキュリティ基準を強制実行するようにセキュリティ検査を挿入する工程を備える、記憶媒体。
【請求項１５】
前記１つ以上の抽象化が、少なくとも１つのドメイン固有言語の抽象化を備える、請求項１４に記載の記憶媒体。
【請求項１６】
前記１つ以上の抽象化が、悪用防止抽象化を含む、請求項１４に記載の記憶媒体。
【請求項１７】
前記サーバサイドプログラムがウェブプログラムを備える、請求項１４記載の記憶媒体。
【請求項１８】
前記サーバサイドプログラムをコンパイルするステップが、１つ以上のクライアントサイド状態が除去されることを引き起こすための１つ以上のプリミティブを追加する工程を備える、請求項１４に記載の記憶媒体。
【請求項１９】
前記変換された抽象化が、前記目的コードが履歴管理において対応するコマンドを実行した場合に、将来の演算において処理するためのクライアント履歴におけるエントリを前記目的コードに受理させないことを実現させるためのものである、請求項１４に記載の記憶媒体。
【発明の詳細な説明】
【優先権】
【０００１】
[0001]本願は、２００７年７月１３日に出願された対応する仮特許出願第６０／９４９，５６８号、発明の名称「Ｄｏｍａｉｎ−Ｓｐｅｃｉｆｉｃ  Ｌａｎｇｕａｇｅ  Ａｂｓｔｒａｃｔｉｏｎｓ  ｆｏｒ  Ｓｅｃｕｒｅ  Ｓｅｒｖｅｒ−Ｓｉｄｅ  Ｓｃｒｉｐｔｉｎｇ」に対する優先権を主張し、参照することによってこれを組み込む。
【技術分野】
【０００２】
[0002]本発明は、サーバサイドプログラミングの分野に関し、特に、本発明の実施形態は、インタラクティブウェブアプリケーションのためのセキュアサーバサイドプログラム作成分野に関する。
【背景技術】
【０００３】
[0003]ウェブベースのアプリケーションのキーコンポーネントは、ウェブサーバ上で実行するプログラムである。（本願明細書においては「サーバプログラム」と称される）これらのサーバサイドプログラムは、ＨＴＴＰリクエストの形式でクライアントの入力を取り込み、演算を実行してアプリケーションのビジネスロジックを強制実行し、ＨＴＭＬページの形式でクライアントのための出力を生成する。
【０００４】
[0004]特に機密データを管理して重大な機能（例えばオンラインバンキング）を実行するもの等、ウェブアプリケーションの人気の高まりにともない、サーバプログラムの安全性は、大きな懸案事項になっている。実際に、ウェブアプリケーションは、従来のデスクトップアプリケーションよりも多くのセキュリティ脅威のいくつかに直面している。一部の代表的なものは、以下により詳細に記載されるコマンドインジェクション、クロスサイトスクリプティング（ＸＳＳ）、クロスサイトリクエストフォージェリ（ＣＳＲＦ）、および、セッションの固定化を含む。これらのいずれかは、機密ユーザ情報が盗まれることがあり、データおよび関連所有物が損傷されることがあるか、または、サービスアベイラビリティが危険に晒されることがある、という深刻な結果を引き起こすことがある。
【０００５】
[0005]そのようなセキュリティ脅威に応じて、サーバサイドスクリプティングのための既存の言語およびフレームワークは、ウェブアプリケーションセキュリティコミュニティと同様に、大部分は、セキュアコーディングの実務（例えば入力認証）を奨励し、裏付けとしての有用なライブラリー関数（例えばフィルタリング関数）を提供する。しかしながら、プログラマが仮に勧告にしたがう場合、プログラマが正確に勧告にしたがうという保証がない。さらにまた、全てのプログラムが厳密に強制されたセキュリティ実務を有して作成されたとしても、プログラマが脆弱性の防止に費やすという格別の注意は、意図されたビジネス機能から注意を逸らすことになる。例としてオンライン決済の実装を取り上げる。「支払明細書の取得」というウェブインタラクションを安全にコード化するために、入力認証を正確に実行し、インタラクションにわたってプログラム状態を保持し、リクエストフォージェリを防止しなければならない。これらの操作は、以下に例とともに記載される。
【０００６】
理想的な視点
[0006]セキュアサーバプログラムの作成に何が関与しているかを実証するために単純なオンラインバンキングの例が使用される。本特許出願は、アカウント残高を示すこと（「残高」サービス）および支払いを設定すること（「支払い」サービス）という２つの主要サービスを提供する。サービスにアクセスするために、ユーザは、最初に自身のアカウントにログインしなければならない。
【０００７】
[0007]複数のユーザに役立つにもかかわらず、このウェブアプリケーションは、論理的に、１度に１つのクライアントを取り扱う。理想的な視点において、実行するサーバプログラムの複数の直交インスタンスがあり、それぞれは、単一のクライアントの処理を行う。プログラムの１つ１つのインスタンスは、従来のアプリケーションの逐次プログラムとして考えられることができる。この理想的な視点に続くワークフロー図が図１Ａにおいて示されている。
【０００８】
制限された構造
[0008]上述した理想的な視点は、ウェブインタラクションについての根本的なＨＴＴＰ構造のいくつかの制限のために、直接実装されることができない。特に、クライアントから入力を取得するサーバプログラムのための持続的なチャネルがない。その代わり、ＨＴＴＰは、クライアントがＵＲＬによって識別されるいくつかのリソースをリクエストし、且つ、リクエストが受理された場合にサーバがリソースとともに応答する単発のリクエスト・レスポンスモデルをサポートしている。ＨＴＴＰを使用することにより、ウェブインタラクションは、通常、以下のようにリクエストがユーザ入力を規定し且つレスポンスがユーザに情報を提示する一連のリクエスト（フォーム送信）およびレスポンス（ウェブページ）として実行される。
HTTP0→HTML 0→HTTP 1→HTML 1→HTTP 2→HTML 2  ．．．
【０００９】
[0009]このモデルを使用することにより、サーバプログラムは、多くの場合、複数のフラグメントに分割される。各フラグメントは、ＨＴＴＰリクエストを解釈し、ＨＴＭＬレスポンスを生成する。レスポンスにおいて、次のリクエストが正確に対象とされるように、次のフラグメントを指し示す埋め込みＵＲＬを有するウェブフォームがあることがある。したがって、図１Ｂにおけるように、本発明者らのバンキングアプリケーションのサーバワークフローがより正確に記載される。ここでは４つのプログラムフラグメントが含まれる。破線によって示されているように、プログラムフラグメントは、適切なＵＲＬ埋め込みと接続される。特に、支払いサービスがユーザ入力を必要とすることから、理想的な視点におけるサービスループの構造は、もはや明確なループとしてコーディングされることができない。その代わり、ｇｏｔｏスタイルの構造がＵＲＬ埋め込みによって示される。そのようなフラグメンテーションおよび低水準の制御構造は、サーバプログラムの制御フローを曖昧にする。
【００１０】
[0010]曖昧であると共に、ＨＴＴＰは処理状態を把握しておらず、したがって、サーバプログラムは単独でプログラム状態を保持しなければならないという、より大きな問題がある。この例において、ログイン入力から取得されたユーザ名は、後のウェブインタラクションにわたって明確に保存されて復元されなければならない。さらに、複数のクライアントが、論理的に別個のトランザクションにおいてではあるものの、サーバと同時に交信していることがあるため、サーバプログラムは、何らかの形で、到来するリクエストを特定のクライアントと相互に関連付けなければならない。
【００１１】
[0011]実際に、ウェブアプリケーションは、ＨＴＴＰよりも上位のレベルにおいて状態を符号化することを必要とする。異なる状況に適用可能ないくつかの代替例がある。通常、「セッション」の仮想的な概念は、論理トランザクションに言及するために使用される。あらゆるセッションは、ＳＩＤと称される固有のＩＤと関連している。保存されたプログラム状態および到来するクライアントリクエストは、双方とも、ＳＩＤによって識別される。
【００１２】
[0012]結果として、サーバプログラムにおける多くのコードは、セッションを操るために割り当てられる。レスポンスを生成する前に、サーバプログラムは、状態を保存してレスポンスにＳＩＤを埋め込まなければならない。リクエストを受信すると、サーバプログラムは、リクエストからＳＩＤを取得して状態を読み込まなければならない。アプリケーションに基づいて、一部の状態は、サーバ上に保存されるべきであるのに対して、他はクッキーまたはＵＲＬ埋め込みを介してクライアント上に保存されるべきである。これらのルーチン操作は、サーバプログラムの複雑性を増加させ、生産性を低減し、プログラミングエラーの可能性を拡張する。
【００１３】
危険な世界
[0013]プログラマが上述した問題の全てに正確に対処すると仮定しても、結果として生じるプログラムは、なおも配置の準備が整わないことがある。問題は、セキュリティである。すなわち、現実世界におけるクライアントは悪意のあることがあり、または、攻撃者は無知なクライアントに過ちを犯させることがある。
【００１４】
[0014]実際に、識別される多くの共通のウェブセキュリティの脆弱性があった。したがって、セキュアプログラミング解決策が提案されている。それにもかかわらず、プログラマは、関与する全ての問題および関連する防御の実装に気付かなければならない。これらの防御の大部分は、特定のウェブアプリケーションのビジネスロジックに直交している。
【００１５】
[0015]以下において、いくつかの代表的なセキュリティ問題の概要が与えられる。目的は、全体リストを与えることではなくウェブプログラミングの複雑性を実証することである。これらのセキュリティ問題は、ＣＳＲＦ、ＸＳＳ、セッションの固定化等を含む。
【００１６】
[0016]ＣＳＲＦ  −  攻撃者は、あたかもユーザがそれに気付くことなく他のユーザによって意図されたかのように、リクエストを偽造することがある。これは、ＳＩＤがクッキーに格納された場合に主に適用される。上述したバンキング例が安全にコーディングされないと仮定する。ユーザが、ログインするとともに、巧妙に作り上げられた画像リンクを含む悪意のある電子メールを開封した場合に、そのような攻撃が開始されることができる。画像を読み込もうとすると、ユーザのブラウザは、リンクに追従することができて、攻撃者に設定されるように支払いを求めるバンキングサーバに対してリクエストを送信することがある。代表的な防御は、重大な機能に対していくつかの秘密のトークンをＵＲＬに埋め込むことであり、偽造されたリクエストは、トークンを有さず、したがって、サーバサイドで処理されない。
【００１７】
[0017]ＸＳＳ  −  攻撃者は、サーバプログラムが被害ユーザに対して送信するＨＴＭＬページ内に悪意のあるコードを投入することがある。１つの代表的な状況において、攻撃者は、悪意のあるＪａｖａＳｃｒｉｐｔコードが埋め込まれた巧妙に作り上げられたリンクを被害者に対して送信し、被害者がリンクを読み込んだ場合に、脆弱なサーバプログラムは、ＨＴＭＬレスポンス内に埋め込みコードを伝播することがある。ここでサーバから到来する悪意のあるコードは、サーバドメインの特権を得る。例えば、それは、サーバによって設定されたクッキーを読み取ることがあり、クッキーを攻撃者に対して送信することがある。この状況は、何らかの形でＣＳＲＦに関連している。しかしながら、偽造されたリクエストの使用を必要としない二次攻撃もまたある。代表的な防御は、ウェブ入力を処理する前にウェブ入力にフィルタをかけることである。
【００１８】
[0018]セッションの固定化  −  攻撃者は、事前にＳＩＤを固定し、ユーザにその固定されたＳＩＤを使用してサーバと通信させることがある。これは、主に、ＳＩＤがＵＲＬに埋め込まれた場合に適用される。無知なユーザは、本発明者らのバンキングサイトからのものであると主張する悪意のある電子メールにおけるリンクをクリックすることがある。リンクは、本願明細書に記載されたバンキングサイトにユーザを連れていくが、攻撃者によって固定されたＳＩＤを使用している。ユーザがログインした後のウェブインタラクションについて同じＳＩＤが本発明者らのサーバプログラムによって使用された場合、ＳＩＤの攻撃者の知識は、ユーザの完全な特権を得る。代表的な防御は、特権が変化した場合（例えば成功したログイン照合時）にＳＩＤを再生することである。
【００１９】
[0019]その他  −  セキュリティに影響を及ぼす多くの他の態様がある。ウェブアプリケーションが複数のプログラムフラグメントとして実装されるという事実を考える。各フラグメントは、サービスインターフェースとして開かれる。攻撃者は、サーバレスポンスに提供されたリンクに厳密にしたがうことなく、これらのインターフェースに対してリクエストを形成することができる。巧妙に作り上げられたリクエストを使用することにより、攻撃者は、（例えばクライアントサイド状態の甘い実装を変更することによって）潜在的にプログラム状態を汚染することができるか、（例えば不十分な入力認証につけ込むことによって）不正な形式の入力を投入するか、または、（例えば予期しない「戻る」ボタンの使用によって）意図されたワークフローを巧妙に逃れる。
【００２０】
[0020]プログラマは、これらの全ての問題に気付き、関連するセキュリティ実務にしたがうことを必要とする。結果のコードにおいて、ビジネスロジックは、セキュリティ操作と結び付けられる。したがって、セキュアウェブプログラミングは困難であり、ウェブプログラムは保持することが困難である。宣言型ウェブプログラミングの分野において、ドメイン固有言語構成は、ウェブアプリケーションをプログラミングするために使用されている。そのような場合、ウェブアプリケーションは、フォームベースのサービスとして考えられ、抽象化は、ウェブ入力および状態管理等のいくつかの重要な態様に提供される。これらの抽象化は、実装の細部（例えば、入力認証、ＵＲＬへの継続および状態の埋め込み）を隠蔽し、したがって、特定のプログラミングエラーを防止する。それらはまた、ユーザインターフェース（ＨＴＭＬページ）から制御フロー（ビジネスロジック）を分離するのに役立つ。しかしながら、従来の技術は、セキュリティ保証をともなういかなる形式的意味論も提供しない。それにもかかわらず、セキュリティは、宣言型ウェブプログラミングについて見逃されることができない−ウェブインタラクションの細部が新たな抽象化によって隠蔽されるからには、プログラマは、もはや単独でセキュアコーディング実務を実行することができない。結果として、新たな抽象化の甘いアプリケーションは、セッションの固定化およびＣＳＲＦ等のセキュリティ脆弱性に苦しむことになる。
【００２１】
[0021]既存のタイプの安全言語のライブラリーとして、ウェブプログラミングのためのドメイン固有言語またはフレームワークを開発する作業もまたある。いくつかの著名な例は、Ｃｕｒｒｙベースのサーバサイドスクリプト言語、ＨａｓｋｅｌｌベースのＷＡＳＨ／ＣＧＩ、および、ＳｍａｌｌｔａｌｋベースのＳｅａｓｉｄｅである。これらは、構造化ＨＴＭＬ生成、セッション管理、および、クライアント・サーバ通信等、ウェブプログラミングのいくつかの共通の態様を処理するためにライブラリーの形式で有用な抽象化を提供する。しかしながら、それらは、本願明細書に記載される全ての形式的なセキュリティ保証を提供するというわけではない。さらにまた、原則として、正確な動作はホスト言語の実装および意味論から推察されることができるものの、新たな抽象化についてのスタンドアローンの形式的意味論がない。最後に、それらはホスト言語に関連し、したがって、着想は他の言語に容易に適用されない。
【００２２】
ウェブプログラムのモデル
[0022]既存のウェブプログラミングモデルが何か、およびその範囲内でセキュアプログラムを作成する方法を理解することもまた重要である。トピックに利用可能な多くのセキュリティ勧告およびコーディング実務があるにもかかわらず、ウェブプログラミングは、滅多に言語原理から形式的に研究されていない。１つの例外において、ウェブインタラクションは、良かれと思ってなされた（悪意のない）ユーザの気まぐれなナビゲーション動作の存在下でモデル化され、エラーの２つのクラス（フォームフィールドの不整合、クライアント・サーバ状態の不整合）が識別され、静的型システム（型付きウェブフォーム）および動的チェック（タイムスタンプがつけられた状態）によってエラーを見つけることが提案される。この例外は、サーバと交信する複数のクライアントがあり、クライアントの一部が悪意のあることがある、より広いセキュリティ問題に対処しない。具体的には、それは、サーバサイドの演算におけるセキュリティ関連のプリミティブを有さず、単一のクライアントの存在下でウェブプログラムをモデル化し、遷移は、本願明細書に記載されたいくつかの偽造およびだましの動作の対照を欠いている。
【発明の概要】
【課題を解決するための手段】
【００２３】
[0023]セキュアサーバサイドプログラミングのための方法および装置が本願明細書に開示される。一実施形態において、本方法は、１つ以上の抽象化を有するサーバサイドプログラムを生成するステップと、上記１つ以上の抽象化を含む上記サーバサイドプログラムをセキュリティ基準に関して安全な方法で実行するように保証される目的コードに変換することによって、上記サーバサイドプログラムをコンパイルするステップとを備える。
【００２４】
[0024]本発明は、以下に与えられる詳細な説明および本発明の様々な実施形態の添付図面からより完全に理解される。しかしながら、それらは、本発明を特定の実施形態に限定するように解釈されるべきではなく、説明および理解のみのためのものである。
【図面の簡単な説明】
【００２５】
【図１Ａ】オンラインバンキングの理想的なワークフローを図示している。
【図１Ｂ】オンラインバンキングの現実のワークフローを図示している。
【図２】サーバサイドスクリプティングについての処理の一実施形態のフロー図を図示している。
【図３】ＢＡＳＳにおける単純なバンキングを図示している。
【図４】実行環境の仮想図を図示している。
【図５】ＢＡＳＳ構文を図示している。
【図６】ＢＡＳＳ操作的意味論を図示している。
【図７】ＢＡＳＳタイピング規則を図示している。
【図８】ウェブプログラミングのモデルを図示している。
【図９】ＭＯＳＳ構文を図示している。
【図１０】ＭＯＳＳ表現の評価を図示している。
【図１１】ＭＯＳＳ世界の実行の１／２部分を図示している。
【図１２】ＭＯＳＳ世界の実行の２／２部分を図示している。
【図１３】変換を図示している。
【図１４】例示的なコンピュータシステムのブロック図である。
【発明を実施するための形態】
【００２６】
[0040]本発明の実施形態は、インタラクティブウェブアプリケーションのためのセキュアサーバサイドプログラムを作成する分野に関する。ウェブアプリケーションは、従来のソフトウェアとは異なる演算モデルを反映し、その中のセキュリティ問題は、言語原理および実際の実装の双方から注意深く検討するに値する。本願明細書に記載される技術は、セキュアサーバサイドスクリプティングのための形式的基礎を構築するのに役立つ。特に、トピック上の２つの自己完結型形式化が記載される。
【００２７】
[0041]第１は、サーバサイドスクリプティングのための宣言型言語ＢＡＳＳである。ＢＡＳＳは、ウェブ入力を取得してクライアント履歴を操作するためにいくつかの専用の構成を使用して、サーバが単一のクライアントと交信するプログラミングモデルを提供する。ＢＡＳＳのメタ特性および形式的な保証は、プログラマが共通の実装細部によって注意を逸らされることなくアプリケーションロジックに集中することを可能とし、したがって、生産性およびセキュリティを改善する。
【００２８】
[0042]第２は、現実的なウェブプログラミング概念を特徴付けるモデルＭＯＳＳである。ＭＯＳＳは、脆弱なものと同様にセキュアプログラムを作成するために使用されることができる。ＢＡＳＳからＭＯＳＳへの形式的な変換が提示され、どのようにしてＢＡＳＳ抽象化およびセキュリティ保証がセキュリティ概念を操作するための数個の共通プリミティブを使用して実際に強制実行されることができるかを実証する。
【００２９】
[0043]以下の記載において、本発明のより完全な説明を提供するために多数の詳細が説明される。しかしながら、本発明がこれらの特定の詳細なしで実施されてもよいことは当業者にとって明らかである。他の例においては、本発明の不明瞭化を回避するために、周知の構造および装置が詳細にではなくブロック図形式で示される。
【００３０】
[0044]以下の詳細な説明の一部は、コンピュータメモリ内におけるデータビット上の操作のアルゴリズムおよびシンボル表現の観点で提示される。これらのアルゴリズム的記載および表現は、それらの作業の内容を他の当業者に最も効果的に伝えるために、データ処理技術における当業者によって使用される手段である。アルゴリズムは、ここでは、そして一般に、所望の結果をもたらすステップの首尾一貫したシーケンスであると考えられる。ステップは、物理量の物理的な操作を必要とするものである。通常、必ずではないが、これらの量は、記憶され、転送され、結合され、比較され、操作されることができる電気または磁気信号の形式をとる。これらの信号をビット、値、要素、シンボル、キャラクタ、項目、数等と称することは、主に一般的な用法の理由で時には便利であることがわかっている。
【００３１】
[0045]しかしながら、これらのおよび同様の用語の全てが適切な物理量と関連付けられることになっており、これらの量に付されるラベルに単に都合がよいということを念頭におかなければならない。以下の説明から明らかであるとして明確に述べた場合を除き、当然のことながら、記載のはじめから終りまで、「処理」または「演算」または「計算」または「決定」または「表示」等の用語を利用する説明は、コンピュータシステムのレジスタおよびメモリ内の物理（電子）量として示されるデータを操作し、コンピュータシステムのメモリもしくはレジスタまたは他のそのような情報記憶装置、伝送または表示装置内の物理量として同様に示される他のデータに変換する、コンピュータシステムまたは同様の電子計算機の作用および処理に言及する。
【００３２】
[0046]本発明はまた、本願明細書における動作を実行するための装置にも関する。この装置は、必要な目的のために特別に構成されてもよく、または、コンピュータに記憶されたコンピュータプログラムによって選択的に起動されるもしくは再設定される汎用コンピュータを備えてもよい。そのようなコンピュータプログラムは、限定されるわけではないが、フロッピーディスク、光ディスク、ＣＤ−ＲＯＭ、および、光磁気ディスクを含む任意のタイプのディスク、読み出し専用メモリ（ＲＯＭ）、ランダムアクセスメモリ（ＲＡＭ）、ＥＰＲＯＭ、ＥＥＰＲＯＭ、磁気もしくは光カード、または、電子命令を記憶するのに適し且つコンピュータシステムバスとそれぞれ連結される任意のタイプの媒体等のコンピュータ読み取り可能な記憶媒体に記憶されてもよい。
【００３３】
[0047]本願明細書に提示されるアルゴリズムおよび表示は、本質的に、任意の特殊なコンピュータまたは他の装置に関連がない。様々な汎用システムが本願明細書における教示にかかるプログラムを用いて使用されてもよく、または、必要な方法ステップを実行するためにより特殊化した装置を構成することは都合がよいと証明してもよい。様々なこれらのシステムのために必要な構造は、以下の記載から明らかになる。さらに、本発明は、任意の特定のプログラム言語に関して記載されない。当然のことながら、本願明細書に記載されているように、様々なプログラム言語が本発明の教示を実装するために使用されてもよい。
【００３４】
[0048]機械読み取り可能な媒体は、機械（例えばコンピュータ）によって読み取り可能な形式で情報を記憶または伝送するための任意の機構を含む。例えば、機械読み取り可能な媒体は、読み出し専用メモリ（「ＲＯＭ」）、ランダムアクセスメモリ（「ＲＡＭ」）、磁気ディスク記憶媒体、光記憶媒体、フラッシュメモリ装置等を含む。今日のウェブは、高度なアプリケーションおよびサービスのホスティングのためのプラットフォームとして一般に使用される。
【００３５】
概要
[0049]上述したように、確実なウェブアプリケーションをプログラミングするのはよく知られているように困難である。ウェブインタラクション、状態保持、および、気まぐれなユーザナビゲーション動作に対処する他に、プログラマはまた、セキュリティ脆弱性の地雷原を回避しなければならない。問題は、基本的に２つの要素からなる。一方は、ウェブアプリケーションの根本的な新たな演算モデルの本質の確実な理解の不足がある。他方は、特定のウェブアプリケーションのビジネス機能に直交している共通で巧妙なコーディングの細部を隠蔽するための適切な抽象化の不足がある。
【００３６】
[0050]双方の問題は、本願明細書において対処される。第１に、高水準言語ＢＡＳＳが宣言型サーバサイドスクリプティングのために提示される。ＢＡＳＳは、共通であるがウェブプログラミングの問題のある態様に取り組むためにいくつかの新たな抽象化を使用して理想的な世界において、プログラマが作業することを可能とする。ＢＡＳＳの形式的意味論およびメタ特性は、有用なセキュリティ保証を提供する。第２に、その形式的意味論が現実的なウェブプログラミング概念および状況を反映し、したがってウェブプログラミングの後に演算モデルを統合する低水準言語ＭＯＳＳが提示される。最後に、ＢＡＳＳからＭＯＳＳへの厳密な変換が提示され、どのようにしてＢＡＳＳの理想的なプログラミングモデルおよびセキュリティ保証が実装されて実際に強制実行されることができるかを実証する。
【００３７】
[0051]セキュリティ問題の多くがウェブアプリケーションの特定のビジネスロジックに直交していることを観察することにより、セキュアサーバプログラムを作成するためのいくつかの新たな抽象化が本願明細書に開示される。これらの抽象化は、（例えば「クライアントから数を得るために」）ウェブプログラミングのいくつかの重要な態様の理想的な視点を提供し、共通のセキュリティ取り扱い（例えば、入力認証、セッション状態の保持、および、リクエストフォージェリの防止）を隠蔽する。
【００３８】
[0052]これらの抽象化を使用して、サーバサイドスクリプティングのための言語は、一度限りで確立されたセキュリティ実務にしたがう基礎言語の実装によって処理される意味論の正確な強制実行をともなって有用で安全なウェブ操作を反映する、高水準構文および意味論を与えられることができる。結果として、その言語で作成された全てのプログラムは、低水準のセキュリティ構成を直接取り扱わないにもかかわらず、所定のセキュリティ脆弱性がないことが保証される。さらに、高水準意味論の観点から、プログラマは、よりビジネスロジックに集中することができ、より良好なセキュリティおよびより高い生産性をもたらす。ある程度は、新たな抽象化は、オブジェクト指向言語におけるオブジェクト生成プリミティブが低水準のメモリ管理の細部を隠蔽するのと同様にして、セキュリティの細部を隠蔽する。
【００３９】
[0053]どのようにして開示された抽象化が正確に実装されることができるかを実証するために、（「サーバサイドスクリプティングのモデル」におけるような）低水準言語ＭＯＳＳは、サーバサイドスクリプティングのための既存の言語のプログラミングモデルを反映する。ＭＯＳＳは、良好に動作されるクライアントリクエストおよび悪意のある攻撃者の悪用の双方を含む代表的なクライアントおよびサーバ動作を統合することから、独自の関心からなる。ＢＡＳＳは、ＭＯＳＳに変換され、ＢＡＳＳの理想的なモデルは、セキュリティ概念を操作するための適切なＭＯＳＳプリミティブの助けを借りて強制実行される。ＢＡＳＳのセキュリティ保証が保持される方法もまた説明される。
【００４０】
[0054]図２は、サーバサイドスクリプティングのための処理の一実施形態のフロー図である。処理は、ハードウェア（例えば、電気回路、専用ロジック）、（汎用コンピュータシステムまたは専用機械上で実行されるような）ソフトウェア、または、双方の組み合わせを備えてもよい処理ロジックによって実行される。
【００４１】
[0055]図２を参照すると、処理は、１つ以上の抽象化を有するサーバサイドプログラム（例えばウェブプログラム）を作成する処理ロジックによって開始する（処理ブロック２０１）。一実施形態において、抽象化は、少なくとも１つのドメイン固有抽象化を含む。一実施形態において、抽象化は、ウェブ入力抽象化、セッション管理抽象化、状態保持抽象化、および、悪用防止抽象化からなる群からの１つ以上の抽象化を含む。一実施形態において、抽象化は、少なくとも１つのスクリプトを含む。
【００４２】
[0056]一実施形態において、ウェブ入力抽象化は、暗にユーザリクエストを受信するためのサービスインターフェースを開くフォーム構成を含む。一実施形態において、フォーム構成は、エラーが発生される前に１回のみサービスインターフェースが開かれる単一使用モード、または、サービスインターフェースが将来のリクエストのために開いたままである複数使用モードを指定する。一実施形態において、フォーム構成は、引数としてＨＴＭＬ文書を取る。一実施形態において、フォーム構成は、クライアントに対してＨＴＭＬページを提示し、それに対するレスポンス内のクライアントからの入力を取得する。
【００４３】
[0057]一実施形態において、抽象化は、クライアント状態が解除されることを引き起こすための消去コマンドを含む。一実施形態において、クライアント状態は、クライアント履歴を含む。
【００４４】
[0058]一実施形態において、サーバサイドプログラムは、ウェブプログラムであり、１つ以上の抽象化は、ウェブ入力、セッション管理、状態保持、および、悪用防止における抽象化の組を含む。
【００４５】
[0059]一実施形態において、サーバサイドプログラムを作成することは、１つ以上の抽象化を既存のサーバプログラムに挿入することを含む。
【００４６】
[0060]サーバサイドプログラムを作成した後に、処理ロジックは、１つ以上の抽象化を含むサーバサイドプログラムをいくつかのセキュリティ基準に関して安全な方法で実行するように保証される目的コードに変換することによって、サーバサイドプログラムをコンパイルする（処理ブロック２０２）。一実施形態において、サーバサイドプログラムをコンパイルすることは、コンパイル中にセキュリティ基準の意味論を強制実行するためにセキュリティ検査を挿入することを含む。一実施形態において、サーバサイドプログラムをコンパイルすることは、１つ以上のクライアントサイド状態が除去されることを引き起こすために１つ以上のプリミティブを追加することを含む。
【００４７】
[0061]本発明の実施形態は、シーン後にいくつかの共通セキュリティ態様を取り扱う高水準言語を使用してウェブアプリケーションをプログラミングする。この言語は、ウェブプログラミングのために設計された新たな抽象化から利益を得る。この言語におけるプログラムは、対象アプリケーションのビジネスロジックをより直接反映し、したがって、作成し、論証し、保持することがより容易である。言語実装（コンパイラ）は、確立されたセキュリティ実務の後に安全な目的コードを発生させる。
【００４８】
ウェブインタラクションの抽象化
[0062]上述した説明から、複雑性の多くは、ユーザ入力を取得する必要性に起因する。したがって、ウェブインタラクションをサポートすることは重要である。本発明の実施形態は、この目的のために専用の構成フォームを使用する。
ｆｏｒｍ（ｐ：「ユーザ名」，ｑ：「パスワード」）
フォーム構成の目的は、クライアントに対してＨＴＭＬページを提示し、いくつかの入力を取得することである。現実的な配置において、そのような構成は、場合によっては動的に生成されるおよび／または複数のコンポーネントフォームを含む、本格的なＨＴＭＬ文書を引数として取る。本発明を不明瞭化しないために、フォーム構成は、単一のウェブフォームの入力パラメータを記述するための引数を取る。上述した例において、フォーム構成は、ユーザ名およびパスワードという２つのフィールドから構成される単純なフォームをクライアントに対して提示する。クライアントがフォームに記入してそれを送信した後、フォーム構成は、２つの変数ｐおよびｑに対してフィールドに提供された値を割り当てる。
【００４９】
[0063]基本的な実装によって暗に処理される数個の問題がある。第１に、サーバプログラムがフォーム構成によって分割され、適切なＵＲＬ埋め込みが制御フローを接続するためにウェブページにおいて使用される。第２に、変数の入力値がフォーム送信から解析され、入力認証が宣言された変数型にしたがって実行される。第３に、セッションを管理し、状態を保持し、共通の悪用に対して防御するように、標準のセキュリティ実務にしたがう。実装の細部は、以下により詳細に説明される。差しあたって、制御フローを中断しない抽象および安全なウェブ入力操作としてのプログラマの観点からこの構成を理解するのに十分である。
【００５０】
ユーザナビゲーションのサポート
[0064]一実施形態において、そのようなフォーム構成は、暗にユーザリクエストを受信することができるサービスインターフェースを開く。適切に処理されない場合、または、その処理がプログラマによって十分に理解されていない場合には、脆弱性がある。ウェブインタラクション抽象化における従来のアプローチは、インターフェースが１回のみ「開く」ことを必要とする−インターフェースに対する第２のリクエストは受理されない。これは、著しくユーザナビゲーションを制限する。実際に、ユーザが「戻る」ボタンを使用して先のナビゲーション段階に戻るのはよくあることである。一般に、ブラウザ履歴における任意の項目は、ユーザによって再閲覧されることができる。そのような操作の有効性は、一斉に却下されるのではなく、アプリケーションによって決定されるべきである。与えられたバンキング例について、ユーザがサービス選択ページを複製して「残高」および「支払い」の双方を平行して進めることを可能とすることは妥当である。
【００５１】
[0065]この目的のために、本発明のいくつかの実施形態において、単一使用モード（ｆｏｒｍＳ）および複数使用モード（ｆｏｒｍＭ）というウェブインタラクションの２つのモードが許容される。単一使用モードにおいて、インターフェースは、リクエストのために１回のみ開かれ、（例えばブラウザのブックマークを起動することによって）インターフェースを再閲覧することは、エラーをもたらす。複数使用モードにおいて、インターフェースは、将来のリクエストのために開かれたままである。ＢＡＳＳの意味論は、双方の場合においてプログラムの動作を統合し、したがって、プログラマは、アプリケーションに基づいて適切なものを選択することができる。いずれの場合においても、インターフェースに対するサーバプログラムの意図された制御フローにしたがう場合にのみリクエストは受理される。与えられたバンキング例を考える。ユーザがサービス選択ページに到達してそれをブックマークし、ログアウトする前にそれを再利用した場合には承認される。しかしながら、ユーザが最初にログインおよびサービス選択ページを経由しないで支払いリクエストを偽造した場合には承認されない。
【００５２】
プログラム状態の保持
[0066]任意の動作がブラウザ履歴における地点を再閲覧するとして考えられることができるため、複数使用フォームは、全ての可能なクライアントナビゲーション動作に適合するのに十分である。プログラマの観点から、プログラムは、全ての適切なプログラム状態とともに、複数使用フォーム命令文において複数の平行な「スレッド」に事実上分岐される。そこでのプログラム状態の処理は簡単ではない。状態の一部は、個々のスレッドに対してローカルであることができる一方で、他は全てのスレッドに対してグローバルであることができる。スレッドの「ローカルな」状態は、他のスレッドによって影響を受けないのに対して、「グローバルな」状態は、他によって影響を受けることがある。状態の不注意な処理は、論理エラーをもたらすことがある。
【００５３】
[0067]状態の正確な分割は、アプリケーションによって決定されるべきである。一実施形態において、プログラマは、揮発性または不揮発性のいずれかとして変数を宣言することが可能とされる。例えば、揮発性状態は、ウェブインタラクションにわたってサーバ上のデータベースに記憶されることができ、したがって、全ての分岐されたスレッドは、同じ揮発性状態を参照する。対照的に、（クライアント変更に対する適切な保護の後の）不揮発性状態は、ウェブインタラクションによってウェブフォームのＵＲＬに埋め込まれることができ、したがって、あらゆる分岐されたスレッドは、それ自体の不揮発性状態を有する。
【００５４】
クライアント履歴の操作
[0068]いくつかの先に分岐されたスレッドを無効にすることが有用である場合がある。ユーザが上述したバンキングアプリケーションからのログアウト後にサービス選択ページを再読み込みしようとすると仮定する。サーバプログラムは、処理されるべきではないリクエストを受信する。一実施形態において、機構は、クライアント履歴におけるエントリの一部を無効にするために含まれる。既存のウェブアプリケーションにおいて、これは、ウェブフォーム内に特別なトークンを埋め込み、リクエストによってそれらを照合することによって処理される場合がある。ログアウトすると、サーバプログラムは、対応するトークンを失効し、したがって、サービス選択ページに対するさらなるリクエストは、もはや処理されない。
【００５５】
[0069]プログラマに対してトークン埋め込みの詳細を露呈することを回避するために、単純な消去コマンドが同様の目的のために使用される。プログラマの観点から、全ての先に分岐されたスレッドが破棄されるように、消去は単にクライアント履歴をリセットする。これは、多くのウェブアプリケーションの「セッションタイムアウト」動作に対応する。しかしながら、ＳＩＤのトークンを無効にする観点からの考えの代わりに、ＢＡＳＳは、プログラマがクライアント履歴の観点から考えることを奨励する。クライアント履歴を操作するよりも一般的な方法が確かにある。１つの可能性は、特権レベルをあらゆるウェブフォームに付随させ、レベルによって分岐されたスレッドを操作することである。ここで留意すべきは、そのようなレベル管理が、ウェブ入力、揮発性状態、および、不揮発性状態の提供された抽象化を使用して、プログラマによって容易に実装されることができるということである。より具体的には、現在レベルは、グローバルレベルとしてサーバ上の揮発性変数に記憶されることができる。ウェブインタラクションにより、現在レベルは、ローカルレベルとして不揮発性変数を使用して現在のスレッドに付随されることができる。グローバルおよびローカルレベルならびに適切な処理の比較は、いかなるユーザリクエストに対しても行われることができる。言語の表現力を増加させないにもかかわらず、レベルに基づく特権管理のための抽象化は、所定のアプリケーションにとって都合がよいと証明してもよい。しかしながら、その処理が容易であることから、それは省略され、単純な消去コマンドが実証のために使用される。
【００５６】
再閲覧される例
[0070]上述した導入された抽象化の魅力が、図３において実施されるようにバンキング例を再閲覧することによって実証される。
【００５７】
[0071]新たな抽象化を使用することにより、プログラマは、１つのクライアントのみがあってクライアントが良好に動作する理想的な世界で作業する。図３を参照すると、コードは、クライアントからログイン情報を取得し、ログイン照合を実行し（照合が失敗した場合に、ログイン照合はプログラムを終了する）、サービスループを進める。クライアントのサービス選択に基づいて、サービスループにおけるコードは、残高サービス（残高表示）もしくは支払いサービス（支払い実行）を実行するか、または、ユーザをログアウトさせる。サービス選択入力は、複数使用フォームを使用してコーディングされ、したがって、ユーザは、対応するウェブページを複製して２つのサービスを平行して進めてもよい。さらに、ユーザがログアウトした場合に、全てのサービススレッドを無効にするために消去が使用される。この例において、ユーザ変数のみがウェブインタラクションにわたって生きている。その値は、単一使用フォームから取得され、ログイン処理後に更新されない。したがって、それは、揮発性または不揮発性のいずれかとして宣言されることができる。
【００５８】
[0072]このコードは、図１のワークフローによく対応しており、既存の言語において直接作成されるバージョンよりも非常にきれいである。さらに重要なことに、新たな抽象化の実施が透過的に「配管」の処理を行うことから、それはセキュリティを犠牲にしない。−それは、プログラムを複数のフラグメントに分割し、ウェブインタラクションにわたってプログラム状態を保持し、変数型に基づいて入力にフィルタをかけ、秘密のトークンの埋め込み等の関連するセキュリティ操作を実行する。
【００５９】
[0073]勿論、これらの抽象化が、全てのプログラミングタスクのために適していなくてもよい。動的な操作および状態保持をほとんど必要としないアプリケーションについて、セキュリティの細部を直接コーディングすることが大きな負担としなくてもよい。しかしながら、特に重大領域においてウェブアプリケーションの人気および複雑性の高まりを観察すると、そのような抽象化は、多くの恩恵をもたらす。
【００６０】
ＢＡＳＳ
[0074]上述した着想は、高水準言語ＢＡＳＳにおいて形式化される。ＢＡＳＳは、上述した低水準細部について心配することなくセキュアプログラムを作成するために宣言型視点をプログラマに提供する。ＢＡＳＳのメタ特性は、有用なセキュリティ保証を提供する。意味論が基本的な実装によって正確に強制実行されると仮定すると、全てのよくまとめられたＢＡＳＳプログラムはある意味では安全である。例えば、ウェブ入力から取得される値は、常に予期される型を有し、攻撃者からの偽造されたリクエストは却下され、プログラムの制御フローは強制実行される。これらの特性は、ＢＡＳＳ構文および意味論の後に、以下により詳細に述べられる。
【００６１】
構文
[0075]ＢＡＳＳの仮想実行環境の図描写が図４において与えられる。図がどのようしてＢＡＳＳが実装されるのかを定めないことから、語句「仮想」が使用され、それは単に取り扱うプログラマに扱いやすい世界を提供する。
【００６２】
[0076]図４を参照すると、この世界において、単一のサーバ４０１および単一のクライアント４０２がある。サーバ４０１は、揮発性変数４１０についてのグローバル環境および現在の実行のクロージャから構成される。クロージャは、不揮発性変数４１２についてのローカル環境およびいくつかのコード４１１から形成されている。実行中に、サーバ４０１は、グローバル変数４１０およびローカル変数４１２という２つの変数環境に関してコードを実行する。ウェブインタラクションにより、サーバ４０１は、適切なクロージャをクライアント４０２に対して送信し、クライアント４０２は、その後に起動される。
【００６３】
[0077]クライアント４０２は、単にクロージャのリストを含む。これらのクロージャは、クライアント４０２の閲覧履歴を反映する。クライアント４０２がアクティブである場合に、クライアント４０２は、閲覧履歴における任意のクロージャを選択して対応するウェブフォームに記入し、結果をサーバ４０１に対して送信する。多くのコード要素がクライアントサイドにおけるクロージャのリストに現れるにもかかわらず、それらは、実際に、基本的な実装におけるフォームに埋め込まれるプログラムポインタとして実現される。同様に、ローカル環境はまた、フォームにおいて実現されることができる。
【００６４】
[0078]図５は、ＢＡＳＳ構文の一実施形態を図示している。ベクトル表記法
【数１】
0005409620.tif 000002
が［κ１．．．κｎ］のリストを参照するために使用される。同様の表意法はまた、他のメタ変数のために使用される。
【００６５】
[0079]図５を参照すると、完全世界は、３個の要素
【数２】
0005409620.tif 000003
からなる。第１の要素Σは、基本的に揮発性変数からそれらの型および値への写像であるグローバル変数環境である。第２の要素κは、サーバ上で現在アクティブなクロージャである。第３の要素
【数３】
0005409620.tif 000004
は、クライアント閲覧履歴である。
【００６６】
[0080]クロージャは、通常、一対のローカル環境およびコマンドである。コマンドなしの環境もまた、クロージャを作り出す場合がある。そのようなクロージャは、実行されることができないが、その中の情報は、他のクロージャに伝播されることがある。ローカル環境は、不揮発性変数から型および値への写像である。揮発性および不揮発性変数の名称は、互いに素であると考えられる。一実施形態において、慣習により、揮発性変数について以下のａ，ａ’，ａ１，．．．が、不揮発性変数についてｘ，ｘ’，ｘ１，．．．が使用される。一実施形態において、整数（ｉｎｔ）および文字列（ｓｔｒ）という２つの型のみが使用される。ブールは、整数によってシミュレートされる。
【００６７】
[0081]コマンドは、上述したようにウェブインタラクション（ｆｏｒｍＳ，ｆｏｒｍＭ）および履歴クリーニング（ｃｌｅａｒ）を除いて共通である。簡便化のために、ウェブフォームは、揮発性変数を入力するのみであり、入力値が割り当てによって不揮発性変数に伝えられることができるため、これは表現力に影響を及ぼさない。表現および値は、予想通りである。表記法ｏｐは、文字列連結および比較等の副次的作用がない動作全体にわたって抽象化するために使用される。関数呼び出しは、標準的であり、新たな問題を導入せず、簡潔性のために省略される。
【００６８】
操作的意味論
[0082]一実施形態において、大きいステップ意味論が表現のために使用される。詳細は標準的であり、したがって省略される。図６は、小さいステップスタイルにおける世界の実行の一実施形態を図示している。換言すれば、ＢＡＳＳ操作的意味論が提示される。図６において使用される表記法は、当業者に理解されるであろう。キーコンセプトは、「世界ステップ」関係
【数４】
0005409620.tif 000005
である。世界ステップの反射推移クロージャとして定義される複数ステップ関係
【数５】
0005409620.tif 000006
がある。
【００６９】
[0083]世界ステップにおいて、いくつかの規則は、サーバサイドの演算を反映するのに対して、他はクライアントサイドの入力を反映する。規則（１）は、単一スレッドステップ関係
【数６】
0005409620.tif 000007
を参照することによってサーバ演算ステップを記述する。これは、現在のコマンドが、スキップ、割り当て、条件節、または、ループによって開始する場合にのみ適用可能である（単一スレッドステップ関係は、他の場合には未定義である）。現在のコマンドが消去である場合には、規則（２）および（３）がクライアントサイドから全てのクロージャを除去するように適用される。この報告のこれらの規則および残りにおいて、表記法εが空ベクトルを記載するために使用される。任意のフォームコマンドにより、規則（４）がクライアントサイドに対してクロージャを転送するように適用される。表記法
【数７】
0005409620.tif 000008
は、シングルトンベクトル［κ］を
【数８】
0005409620.tif 000009
と結合することを意味する。
【００７０】
[0084]単一使用フォームを介したクライアント入力は、規則（５）および（６）において捕獲される。ここで留意すべきは、一実施形態において、サーバ上で実行するためのさらなるコマンドがないということであり、したがって、クライアントは制御する。規則（５）において、クライアントは、クロージャκｉを次に手続きをするために選択する。これは、閲覧履歴における任意の点を採取することに対応する。クライアントは、それらが正当な型
【数９】
0005409620.tif 000010
からなる限り、フォームに任意の値を入力してもよい。入力値に基づいて、グローバル環境は、変数
【数１０】
0005409620.tif 000011
が値
【数１１】
0005409620.tif 000012
を有するようにΣを更新するマクロ
【数１２】
0005409620.tif 000013
を使用して更新される。ステップの結果として、グローバル環境は更新され、選択されたクライアントクロージャは、実行のためにサーバに移動される。表記法
【数１３】
0005409620.tif 000014
は、
【数１４】
0005409620.tif 000015
からκｉを除去することを意味する。規則（５）の自明な変形として、規則（６）はフォーム入力の後に実行するために選択されたクロージャにおけるさらなるコマンドがない場合を記述する。この場合、選択されたクロージャは、単にクライアントから除去される。
【００７１】
[0085]規則（７）および（８）は、複数使用フォームを介したクライアント入力のためのものである。単一使用のものと比較した差異は、閲覧履歴の結果にある。単一使用フォームについて、選択されたクロージャは、それが再閲覧されることができないように履歴から除去される。複数使用フォームについて、閲覧履歴は、同じままである。全てのクライアントリクエスト規則は、クロージャ選択上の非決定性である。クライアントが決してそれを選択しないことによってクロージャを「放棄する」ことは可能である。
【００７２】
[0086]単一スレッドステップ関係は、記録（９）−（１６）において直接記述される。ここで、マクロｕｐｄａｔｅは、グローバルおよびローカル環境の双方を更新するようにオーバーロードされる。
【００７３】
タイピング規則
[0087]図７は、一実施形態において使用するためのいくつかの非標準タイピング規則を図示している。規則（１７）において、世界
【数１５】
0005409620.tif 000016
は、全てのクロージャ
【数１６】
0005409620.tif 000017
がグローバル環境（Σ）に関して適格である場合には適格であり、クライアントサイド上のあらゆるクロージャ（κｉ）は、ウェブフォームによって開始するコードを含む。クロージャの適格性は、規則（１８）および（１９）において定義される。自明なクロージャσは、常に適格である。自明でないクロージャ（σ，Ｃ）は、ＣがΣおよびσに関して適格である場合にはΣに関して適格である。コマンドおよび表現の適格性における標準の取り扱いは省略されており、変数の型は対応する環境から呼び戻される。
【００７４】
メタ特性
[0088]ＢＡＳＳは、ｐｒｅｓｅｒｖａｔｉｏｎおよびｐｒｏｇｒｅｓｓを介して標準型の安定性を享受する。
【数１７】
0005409620.tif 000018
【数１８】
0005409620.tif 000019
【００７５】
[0089]これらの補助定理は、適格なプログラムが（さらなるステップが操作的意味論にしたがってなされることができない状態に入って）固まることなく終了するまで実行することを意味する。一見したところ興味が湧かないものの、これは、実際に、有用な保証をサーバサイドスクリプティングに提供する。それは、基本的に、プログラムの実行が操作的意味論によって限定されることを保証する  −  操作的意味論によって定義される推移のみが起こることがある。したがって、操作的意味論によって反映される全ての動作が保証される。例えば、一実施形態において、そのような動作は、以下を含む。
１．制御フローが明確な高水準構造にしたがう
２．ウェブ入力から取得された値が良好にタイプされる
３．プログラム状態がウェブインタラクションにわたって保持される
４．クライアント履歴におけるエントリが消去によって無効にされる
５．プログラムインスタンスと交信する１つのクライアントのみがある
【００７６】
[0090]これらの保証により、一実施形態において、プログラマは、以下のような所定の共通の低水準の策略についてもはや心配する必要はない。
１．制御フローの埋め込みおよび強制実行
２．ウェブ入力パラメータの名称および型の認証
３．ウェブインタラクションにわたるプログラム状態の回復
４．予期しないユーザナビゲーション動作の対処
５．複数のクライアントを含む悪意のあるつけ込みからの保護（例えば、ＣＳＲＦ、一次ＸＳＳ、および、セッションの固定化）
【００７７】
[0091]一実施形態において、ＢＡＳＳは、意味論によって直接保証される所定の望ましい特性についてウェブプログラミングの高水準視点を提供する。ＢＡＳＳにおける全ての適格なプログラムは、それらの特性を享受し、したがって、プログラマは、改善された生産性および共通のセキュリティ保護を得る。セキュリティにおいてより具体的には、ＢＡＳＳ意味論は、ＣＳＲＦ、一次ＸＳＳ、セッションの固定化、セッションの汚染、不適切にタイプされた入力、および、ワークフロー迂回の余地がないままにする。勿論、操作的意味論は、基本的な実装によって適切に強制実行されなければならない。これは、次の２つのサブセクションの主題であり、ＭＯＳＳは、現実的なウェブプログラミングモデルにしたがって形式化され、ＢＡＳＳは、ＢＡＳＳ操作的意味論が正確に実行されるような方法でＭＯＳＳに変換される。
【００７８】
ＭＯＳＳ
[0092]以下は、サーバサイドプログラムの実行およびクライアントサイド動作を明瞭にするウェブプログラミングの形式モデルを提示する。このモデルは、現実的なウェブインタラクションを反映し、良好に動作されるクライアント／サーバアクティビティおよび悪意のあるつけ込みの双方を具体的に説明するために使用されることができる。このモデルは、主に、どのようにしてＢＡＳＳ抽象化が実現されることができるかについて実証するために厳密なコンパイル対象として使用される。それにもかかわらず、それはまた、ウェブプログラミング上の他の研究に対して独立した値からなる。本発明者らは、このモデルにおける概念がどの程度セクションの全体にわたって現実世界のエントリに対応するかについて説明する。
【００７９】
構文
[0093]図８は、ウェブプログラミングのモデルの図描写を示している。サーバ８０１側において、所望のアプリケーションロジックを実装するために協働するプログラム８０２１−８０２Ｎの群がある。それらは、複数のウェブクライアントに属するデータにアクセスして更新する。サーバ８０１は、別個の論理トランザクションにおいてではあるものの、同時に複数のクライアント８０３１、８０３２、８０３３．．．と交信する。あらゆるクライアントは、それ自身のクッキー（例えば８１３１、８１３２等）を有し、閲覧履歴としてフォームのリストを保持する。フォームがウェブインタラクションを介してサーバサイドから取得されると予期されるにもかかわらず、クライアントはまた、（図示されるように、どこからともなく到来するように見えるＦｏｒｍｘ８３１およびＦｏｒｍｙ８３２を使用して）それ自身におけるフォームを偽造することがある。これは、クライアントが意図されたアプリケーションロジックを経由することなくＨＴＴＰリクエストを作り出す現実世界の悪用を反映する。さらに、悪意のあるクライアント８０３２は、（図示されるようにＦｏｒｍｚ８５０を使用して）クライアント８０３１の履歴に（一部が偽造されることがある）クライアント８０３２の履歴からのフォーム８５０を挿入することによって、無知なクライアント８０３１をだますことがある。現実世界の対照において、攻撃者は、巧妙に作り上げられたリンクを電子メールにおける被害者に対して送信することがあり、これらのリンクは、ブラウザによって自動的に読み込まれることがある画像リンクである場合もある。
【００８０】
[0094]図４の仮想実行環境が理想的な視点を作業するプログラマのために提供するのに対して、ここでのモデルは、現実世界のウェブアプリケーション状況を反映し、サーバプログラムは、複数のクライアントについてデータを交信して保持する。さらに、クライアントは、もはや常に良好に動作されない。このモデルにおいてセキュアウェブアプリケーションを実装するために、サーバプログラムは、セキュリティ概念および構成を操作するためにいくつかの特別なプリミティブを必要とする。例えば、特別なトークン（例えばＳＩＤ）は、ユーザおよび論理トランザクションを識別するために使用されることができ、それらのトークンは、クライアントサイドにおけるクッキーおよびフォームに埋め込まれることができる。
【００８１】
[0095]以下の説明は、低水準言語ＭＯＳＳとしてこのモデルの詳細を提示する。簡潔性のために、ＭＯＳＳは、タイプされないままにされるが、それに標準のタイピングを与えることは容易である。ＭＯＳＳ構文は、図９において与えられる。ベクトル表記法
【数１９】
0005409620.tif 000020
が項目（例えば、［Φ１．．．Φｎ］）のリストを参照する場合に使用されることがある。所定の言語構成を参照するためのいくつかのシンボルは、基本的な概念の対応を示すためにＢＡＳＳから取り入れられるが、軽微な変更は、混同を回避するために適用される。特に、異なるフォントが英文字（Ｗ、Ｃ、Ｅおよびｖ）を再利用するために使用され、ドットがギリシャ文字
【数２０】
0005409620.tif 000021
を再利用するために頂部に追加される。
【００８２】
[0096]一実施形態において、この言語における世界Ｗは、３つの要素から構成される。第１は、サーバ上のグローバル環境
【数２１】
0005409620.tif 000022
である。第２は、サーバ上の現在アクティブなクロージャ
【数２２】
0005409620.tif 000023
である。第３は、それぞれが異なるクライアントに属する閲覧履歴
【数２３】
0005409620.tif 000024
のリストである。
【００８３】
[0097]グローバル環境
【数２４】
0005409620.tif 000025
は、データおよびコードの双方を含む。データ部は、基本的に、セッション（すなわちＳＩＤ）を識別するためのいくつかのトークンιによって体系化されたセッション環境ζのリストである。あらゆるセッション環境ζは、セッションについての揮発性変数（例えばａ、ａ’、ａ１）の値を捕獲する。コード部は、単に、名称ｆ、入力パラメータ「ベクトルａ」のリスト、および、ボディコマンドＣから構成されるあらゆる関数を有する関数の集合である。ここで、シンボル［］は、ＭＯＳＳの一部としてではなくメタ言語の挿入語句として使用される。
【００８４】
[0098]クロージャ
【数２５】
0005409620.tif 000026
は、通常、クライアント識別子ｉ（現在の演算がｉ番目のクライアントについてのものであることを示し、これは、過渡状態であるが、ＨＴＴＰリクエスト・レスポンスのためにクライアントとサーバとの間に確立された専用の接続に対応する）、（リクエストにおいてクライアントからサーバに対して転送されて、レスポンスにおいてクライアントに対して戻される）クッキーの内容としての値ｖ、ローカル環境
【数２６】
0005409620.tif 000027
、および、コマンドＣから構成されるタプルである。一対のクッキー値およびローカル環境はまた、クロージャを形成する場合があり、そのようなクロージャは、実行されることができないが、その中の情報は、他のクロージャに伝播されることができる。ローカル環境
【数２７】
0005409620.tif 000028
は、単に、不揮発性変数の値（例えばｘ、ｘ’、ｘ１）を収集する。
【数２８】
0005409620.tif 000029
は、基本的なセッションのＳＩＤを記憶するために専用とされる特殊変数ｘｓｉｄを含むと考えられる。あるいは、ＳＩＤをクッキーに格納することを望むことがある。クッキーがクライアント上の全てのフォームによって共有されることから、それは、同じクライアントが同時に複数のセッションにアクセスすることを防止する。したがって、以下の説明において、ＳＩＤは、個々の「スレッド」のローカル環境において記憶される。
【００８５】
[0099]クライアントベクトル
【数２９】
0005409620.tif 000030
は、注意に値する。ＢＡＳＳにおいて、単一のクライアントは、クロージャのリストとして理想化される。ＭＯＳＳにおいて、世界は、複数のクライアントを含み、それぞれは、値ｖを有するクッキーおよびフォーム
【数３０】
0005409620.tif 000031
のリストから構成される。フォームφは、入力パラメータ
【数３１】
0005409620.tif 000032
およびそれらの原文の解釈
【数３２】
0005409620.tif 000033
およびデフォルト値
【数３３】
0005409620.tif 000034
（すなわち、ウェブフォームにおける入力フィールド）、ターゲットｆ（すなわち、「送信」ボタンの後のウェブリンク）、ならびに、いくつかの封印されたクライアントサイド状態ψから構成されている。ここで留意すべきは、一実施形態において、ψがクライアントによって変更されるわけではないということである。この制限は、操作的意味論において強制実行される。構文において、表記法＜．．．＞は、それがクライアントによって分解されることができない「パッケージ」であることを示すために使用される。現実の言語において、そのような封印された状態は、クライアント変更を防止するためにサーバによって暗号化／署名されることができる。クライアントが異なるブラウザウィンドウにおいて異なるセッションを開始することがあることから、クライアントにおけるフォームは、異なるセッションに属することがある。セッション識別のためのローカル環境における専用の変数ｘｓｉｄを用意するにもかかわらず、ＭＯＳＳは、自動的に、ウェブインタラクションにわたって変数ｘｓｉｄ（または他の任意の不揮発性変数）を保持しない。現実のウェブプログラミングの場合のままで、プログラマは、封印された状態における関連した情報を保持してもよい。
【００８６】
[0100]コマンドＣは、共通のものと新たなプリミティブとを含む。全ての新たなプリミティブは、セキュアサーバサイドスクリプティングのための現実世界のエントリから適応される。ＢＡＳＳとの差異について、異なる構文が、スキップ（ｓｋ）、割り当て（ａ←Ｅ）、逐次合成（Ｃ；；Ｃ）、条件節（ｃｏｎｄ（Ｅ，Ｃ，Ｃ））、および、ｗｈｉｌｅループ（ｌｏｏｐ（Ｅ，Ｃ））という共通コマンドのために使用される。
【数３４】
0005409620.tif 000035
は、引数
【数３５】
0005409620.tif 000036
によるｆに対する関数呼び出しである。サーバプログラムがウェブ入力を必要とする場合、入力（Ｅ）は、Ｅからクライアントに対して演算されたフォームを送信するために使用される。ｓｅｔＣｋ（Ｅ）は、現在のクロージャのクッキーについての新たな値を設定する。ｕｎｐａｃｋ（Ｅ）は、Ｅから封印された状態を解凍する。
【数３６】
0005409620.tif 000037
は、ＢＡＳＳ型
【数３７】
0005409620.tif 000038
に対する
【数３８】
0005409620.tif 000039
を認証する。最後に、ｅｒｒは、エラーによってプログラムを終了する。この突然のプログラム終了は、簡便化のために使用されるが、現実のウェブアプリケーションは、通常、より高度なエラー処理（例えば、エラーメッセージを与える、他のページにリダイレクトする）を実行する。これらのコマンドの正確な意味は、操作的意味論によって定義される。
【００８７】
[0101]ＭＯＳＳは、変数ａおよびｘ、整数ｉ、文字列ｓ、ならびに、以下に説明される変換の説明の容易化のためのＢＡＳＳの抽象化操作
【数３９】
0005409620.tif 000040
を再利用する。それはまた、以下のいくつかの表現の集合を導入する。
【数４０】
0005409620.tif 000041
は、要素
【数４１】
0005409620.tif 000042
を有する集合であり、ｉｎ（Ｅ，Ｅ’）は、Ｅが集合Ｅ’に属するかどうかを照合し、ｉｎｓ（Ｅ，Ｅ’）は、Ｅを集合Ｅ’に挿入し、ｄｅｌ（Ｅ，Ｅ’）は、Ｅを集合Ｅ’から消去し、ｆｏｒｍは、いくつかの入力パラメータ、目的関数、および、封印された状態を持つ表現をまとめることによってフォームを構成する。ｇｅｔＣｋ（）は、クッキー値を取得する。ψは、封印された状態であり、それは、通常、ｐａｃｋ（）を使用して生成される。最後に、トークンιは、固有であり、ｎｅｗＴｋ（）を使用して生成された偽造できないエントリである。一実施形態において、ｎｅｗＴｋ（）は、決して２つの同一のトークンを生成せず、生成されたトークンは、クライアントによって推測／偽造されることができない。トークンの正確なフォームは、ＭＯＳＳにおける抽象である。本発明者らは、既にＳＩＤとしてのトークンの使用を述べている。後でＢＡＳＳを変換する場合、トークンはまた、クライアントを識別し、制御フローを強制実行し、リクエストフォージェリを防止するために使用される。
【００８８】
操作的意味論
[0102]図１０は、ＭＯＳＳ表現評価についての表現の意味論の一実施形態を図示している。評価は、セッション環境ζ、クッキー値ｖｃｋ、および、ローカル環境
【数４２】
0005409620.tif 000043
という３つのエントリに関して実行される。揮発性および不揮発性変数についての値は、規則（２０）および（２１）において、それぞれ、それらの環境から呼び戻される。値は、さらなる評価を必要としない（規則（２２））。規則（２３）において、表記法
【数４３】
0005409620.tif 000044
は、ｏｐのメタ水準演算を参照する。集合表現は、規則（２４）−（２７）において予想通りに評価され、整数は、ブールをシミュレートするために使用される。規則（２８）は、封印された状態であると思われてフォーム値を構成するフォームの表現要素を評価する。規則（２９）は、単に、ｇｅｔＣｋ（）の評価結果としてクッキーを提供する。規則（３０）は、ローカル環境に基づいて封印された状態を生成する。最後に、規則（３１）は、新たなトークンを作り出す。
【００８９】
[0103]操作的意味論の残りが図１１および図１２において与えられる。ＢＡＳＳと同様に、１つの概念は、「世界ステップ」関係
【数４４】
0005409620.tif 000045
である。複数のステップ関係
【数４５】
0005409620.tif 000046
は、世界ステップ関係の反射推移クロージャとして定義される。
【００９０】
[0104]サーバサイド演算の大部分は、単一スレッドステップ関係
【数４６】
0005409620.tif 000047
にタスクを委任する規則（３２）において捕獲される。入力（Ｅ）コマンドにより（規則（３３））、表現Ｅはフォームφに評価され、結果はクライアントに対して転送される。ここで留意すべきは、特殊変数ｘｓｉｄがＳＩＤιを取得するために使用されるということであり、ιは、セッション環境を位置付けるために使用される（本発明者らは、
【数４７】
0005409620.tif 000048
においてιによって識別されるセッション環境を参照するために
【数４８】
0005409620.tif 000049
を使用する）。さらに、クライアント識別子ｉがクライアント履歴Φｉを位置付けるために使用される。サーバが現在のクロージャ
【数４９】
0005409620.tif 000050
においてクッキーｖｃｋを更新することがあることから、Φｉは、異なるクッキー値ｖを含むことがある。クライアント履歴は、新たなクッキーｖｃｋおよびフォームφを使用してΦｉからΦｉ’に更新される。ステップの結果において、クライアントベクトルは、古いΦｉを除去し、更新されたΦｉ’を挿入することによって更新される。入力（Ｅ）の後の任意のコマンドＣは到達できず、したがって破棄される。これは、サーバの実行がクライアントに対してレスポンスを送信した後に停止し、次のリクエストを受信した後に再開する場合を反映する。制御フローは、他のコマンドＣによって順序付けることによってではなくウェブフォームＥに埋め込まれたリンクによって接続される。この規則（３３）は、入力（Ｅ）コマンドによる実行を記述する唯一のものである。したがって、ＭＯＳＳプログラムの実行は、Ｅがフォームでない場合、ιが
【数５０】
0005409620.tif 000051
によって認識されない場合、または、ｘｓｉｄが正当なトークンを全く含まない場合には固まる。同様の所見が他の規則に適用される。
【００９１】
[0105]世界ステップ関係の残りの規則は、クライアントサイドから開始されるものに関する。理想的な場合は、クライアントが任意の値でフォームに記入してよいということである。しかしながら、ウェブフォームの現実世界の処理において、目的関数名および入力フィールドは、ブラウザがそれらを認識してＨＴＴＰリクエストを生成することができるようにそれらが「送信」ボタンの後に直接埋め込まれることから、悪意のある変更を受ける。そのような状況は、クライアントΦｉが新たなフォームφ’を偽造する（理想的なフォーム記入は単にこれの特殊な場合である）規則（３４）において捕獲される。一実施形態において、クライアントは、関数名および入力フィールドにおいて任意のものを構成してもよい。しかしながら、封印された状態ψは、任意に構成されることができず（例えば、クライアントは、サーバの署名を偽造することができない）、それは、Φｉの履歴においていくつかの他のフォームφから到来しなければならない。さらに、クッキー値はまた、クライアントによってｖｃｋからｖ’に変更されることがある。推移の結果として、新たなクライアントΦｉ’は、偽造されたフォームφ’およびクッキーｖ’を含み、したがって、クライアントベクトル
【数５１】
0005409620.tif 000052
は更新される。サーバサイドは、変化しないままである。
【００９２】
[0106]規則（３５）において、ｉ番目のクライアントは、任意のフォームを履歴から採取し、適切な数の入力値を選択し（
【数５２】
0005409620.tif 000053
は、２つのベクトルが同じ長さを有することを意味する）、フォームを送信する。サーバサイドにおいて、関数ｆは、グローバル環境によって認識され、関数は、適切な数の引数を予想する（ａｓｒｌは、封印された状態についての特殊引数である）。ステップの結果において、新たなクロージャが実行のために構成され、クッキーは、クライアントから取得され、関数ｆは、封印された状態および入力値に適用される。ここで留意すべきは、引数型における入力認証がこの規則において行われないということである。したがって、単独で適切な入力認証を実行しないプログラムは、後の演算において固まることがある。
【００９３】
[0107]攻撃者は、被害者をだまして攻撃者によって構成されたリクエストを送信させる場合がある。規則（３６）において、攻撃者クライアントｉは、任意のフォームφをΦｉから採取し、それを被害者クライアントｊの履歴に挿入する。サーバサイドは、変化しないままである。ここで留意すべきは、フォームが被害者クライアントに投入され、規則（３５）の後のリクエストがそれをサーバに対して送信することがあり、したがって攻撃を完了するということである。
【００９４】
[0108]既存のクライアントは、規則（３７）を使用して新たなセッションを開始することがある。サーバサイドにおいて、新たなトークンιがＳＩＤとして生成され、空のセッション環境がグローバル環境
【数５３】
0005409620.tif 000054
に追加され、新たなクロージャ
【数５４】
0005409620.tif 000055
が構成される。クロージャ
【数５５】
0005409620.tif 000056
において、ローカル環境は、ｘｓｉｄがιに結合され、コードがＭＯＳＳプログラムの開始点として用意された特殊関数であるｆｓｔａｒｔから開始するように開始される。セッション環境およびローカル環境は、まだプログラマ定義の変数についてのエントリを含まない。その代わり、それらの変数は、それらの最初の使用によって暗に宣言され、割り当てを実行するための後の規則において統合される。
【００９５】
[0109]最後のクライアントによって開始された推移、規則（３８）は、新たなクライアントがインタラクションに酸化した場合に適用される。規則（３７）と同様に、ＳＩＤιを有する新たなセッションが生成される。さらに、他の新たな特殊トークンι’がクライアントを固有に識別するためのＩＤ（本願明細書において「ＣＩＤ」と称される）として生成される。ι’は、新たなクロージャκ・のクッキーに格納され、規則（３３）を使用してさらなるウェブインタラクションによってクライアントに伝播される。推移の結果として、グローバル環境が更新され、新たなクロージャが実行のために起動され、クライアントベクトルが、一時的なクライアント識別子ｎ＋１、特殊値・によって示される空のクッキー、および、空の履歴ベクトルεを有する新たなクライアントを含むために更新される。
【００９６】
[0110]図１２は、単一スレッドステップ関係
【数５６】
0005409620.tif 000057
を定義する。スキップ（規則（３９））、順序制御（規則（４２））、条件節（規則（４３）および（４４））、ならびに、ｗｈｉｌｅループ（規則（４５）および（４６））についての場合は標準である。割り当ては、規則（４０）および（４１）において定義され、マクロｕｐｄａｔｅは、セッション環境ζ及びローカル環境
【数５７】
0005409620.tif 000058
の双方を更新するためにオーバーロードされる。更新される変数が環境にない場合、マクロは、新たなエントリを生成し、したがって、変数は、最初の使用によって暗に宣言される。
【００９７】
[0111]規則（４７）は、引数の数を照合して評価した後に、捕獲回避置換を使用して関数呼び出しを実行する。規則（４８）は、現在のクロージャのクッキーを更新する。規則（４９）は、封印された状態に対するＥを評価し、したがって、ローカル環境σ・を更新する。最後に、規則（５０）は、ＢＡＳＳ型
【数５８】
0005409620.tif 000059
に対して
【数５９】
0005409620.tif 000060
を認証する。認証が失敗した場合の規則はない−実行は認証の失敗によって動けない。
【００９８】
例
[0112]ＭＯＳＳは、非常に柔軟な言語であり、いくつかの構文的に正確なプログラムは、実行中に固まる結果をもたらすことがある。そのような固まりの発生は、認識されていないＳＩＤまたは関数名、関数パラメータの不一致数、値の不正／不適切な型の使用（例えば整数の解凍）、および、失敗した入力認証を含む。実際に、ＭＯＳＳは、制限された意味論または型システムを使用するウェブプログラム動作を制限するためではなく、現実のウェブアプリケーション状況を反映するように意図される。既存のウェブプログラミング言語の場合と同様に、ＭＯＳＳは、脆弱なものと同様にセキュアウェブプログラムを作成するために使用されることができる。
【００９９】
[0113]以下において、ＭＯＳＳは、あたかも被害者クライアントＡがログインした場合にそれがＡによって意図されたかのように、支払いリクエストを処理するために攻撃者Ｂが脆弱なバンキングアプリケーションにつけ込むＣＳＲＦ攻撃を具体的に説明するために使用される。
φ＝＜＞を有するフォームｆｐａｙ（「ｐａｙｅｅ」ｐ＝「Ｂ」，「ａｍｎｔ」ａ＝１００）
アプリケーションがクライアントクッキーにおけるＳＩＤを記憶すると考えられる。
【数６０】
0005409620.tif 000061
【０１００】
[0114]上述したように、攻撃者Ｂは、第１のステップにおいてフォームφを偽造し、第２のステップにおいて（例えばリンクを電子メールで送信することによって）それをＡに投入する。第３のステップにおいて（例えばリンクにしたがうことによって）Ａがフォームを送信した場合には、サーバプログラムは、ＡのクッキーにおけるＳＩＤιＡに基づいてセッションを識別し、リクエストがＡからのものであると認識する。したがって、クロージャκ・ｐａｙは、Ａからの支払いを手配するように構成される。
【０１０１】
[0115]同様に、ＭＯＳＳは、一次ＸＳＳ、セッションの固定化、セッションの汚染、不適切にタイプされた入力、および、ワークフロー迂回を含む、多くの他の攻撃状況を具体的に説明するために使用されることができる。対照的に、これらの攻撃のいずれも、そのメタ特性にしたがってＢＡＳＳにおいて発生しないことがある。以下は、どのようにしてＢＡＳＳ意味論が強制実行されることができるかについて説明する。
【０１０２】
変換
[0116]ＢＡＳＳプログラムは、ＢＡＳＳの意味論を強制実行するためにセキュアコーディング実務にしたがってＭＯＳＳに変換される。ＢＡＳＳは、制御フローがウェブ入力によって崩壊せず、単一のセッションのみがあり、クライアントが良好に動作されるという理想的なモデルを有する。これらは、現実世界の状況のＭＯＳＳモデルをもはや保持しない。２つのモデルを接続するために、変換は、プログラム分割、フォーム形成、セッション管理、状態保持、偽造防止、および、入力認証を処理する。ＭＯＳＳにおけるクライアントがクッキーおよびフォームのリストから構成されるということを図８および図９から呼び戻す。本願明細書における変換において、クッキーがクライアントのＣＩＤを記憶するという不変条件が保持され、フォームは以下の形態からなる。
【数６１】
0005409620.tif 000062
【０１０３】
[0117]これは、基本的に、変換のキーであるＭＯＳＳのクライアントフォームにおけるＢＡＳＳのクライアントクロージャの符号化である。目的関数ｆおよび入力パラメータ
【数６２】
0005409620.tif 000063
の他に、本発明者らはまた、ローカル環境についての情報（不揮発性変数
【数６３】
0005409620.tif 000064
）を符号化する。さらに、いくつかの特殊変数が、セッション管理および偽造防止のために使用される。
【０１０４】
[0118]第１の特殊変数ｘｃｉｄは、規則（３８）においてサーバプログラムがクライアントのために割り当てたＣＩＤを格納する。変換されたプログラムにおいて、レスポンスをクライアントに対して送信する前に、ＣＩＤは、現在のクロージャのクッキーから取得され、変数ｘｃｉｄに入れられる。他方では、クライアントからのリクエストを処理した場合に、ｘｃｉｄは、クライアントクッキーに対して検査されて照合される。これは、以下のいくつかの単純な見解に基づいてリクエストが実際にクライアントから到来することを確実にする。すなわち、（１）封印された状態は、クライアントによって変更されることができない、（２）クライアントのクッキーは、他によって更新されることができない、（３）クライアントが自身のクッキーを変更することがあるにもかかわらず、それ自体は、ＣＩＤが偽造できないことから、他のクライアントのＣＩＤの値に変化させることができない。これらは、規則（３６）にしたがって被害者の履歴に挿入された攻撃者の巧妙に作り上げられたフォームがサーバによって受理されることをともに防止する。
【０１０５】
[0119]ｘｓｉｄ変数は、ＳＩＤを格納するために専用とされる。ｘｔｏｋ変数は、「履歴管理」のためにサーバ生成されたトークンを格納する。サーバプログラムがリクエストを処理する場合に、このトークンの正当性が照合される。単一使用フォームについて、トークンは、最初の使用後に失効とされ、したがって、将来の再送信が受理されることを防止する。さらにまた、トークンは、プログラマが（ＢＡＳＳ消去操作の動作にしたがって）全ての既存のフォームを許可しないように選択した場合に、サーバプログラムによって失効されうる。上述したように、より高度な履歴管理は、容易に考えられるが、単純な消去が実証のために使用される。本発明者らはまた、ｘｓｉｄおよびｘｔｏｋの値のみが固有であることを必要とする旨を指摘する。それらは、封印された状態に格納され、したがって偽造されることができないことから、単独で偽造不可能である必要はない。同じトークン構成は、ＣＩＤ、ＳＩＤ、ＭＯＳＳにおける履歴管理のために再利用されるが、これは本発明についての要求ではない。
【０１０６】
[0120]３つのトークンの他に、目的関数名を格納する特殊変数ｘｆｕｎがある。これは、クライアントがフォームの目的関数を変更する所定のリクエストフォージェリを防止することである。リクエストにより、ｘｆｕｎが検査され、それが実際の目的関数と一致した場合にのみリクエストが処理される。
【０１０７】
[0121]一実施形態において、正確な変換が図１３において与えられる。一実施形態において、全てのＢＡＳＳ表現／値がＭＯＳＳ表現／値であることから、表現変換は自明である。変換規則において、ＢＡＳＳ表現Ｅから対応するＭＯＳＳ表現Ｅへの自明な変換を示すようにＥをＥに更新するようにフォントが調整される。
【０１０８】
[0122]コマンド変換は、フォーム
【数６４】
0005409620.tif 000065
を有する。ここで、ＢＡＳＳコマンドＣは、ＭＯＳＳコマンドＣに変換される。変換は、ＢＡＳＳグローバル環境Σ、ＭＯＳＳグローバル環境
【数６５】
0005409620.tif 000066
、および、関数名ｆの入力として取る。Σは、変化なしで変換全体にわたって伝播され、それは、入力認証のためのコードを生成する場合に入力変数の型を取得するために使用される。
【数６６】
0005409620.tif 000067
は、プログラム分割中に導入された新たなコードブロックが累積されることができるように
【数６７】
0005409620.tif 000068
に更新される環境である。ｆは、現在のコマンドに対する継続として提供される。
【０１０９】
[0123]規則（５１）は、スキップを変換する規範事例を記述する。変換は、同じ環境
【数６８】
0005409620.tif 000069
および継続ｆに対する呼び出しを生成する。他の全ての規則は、複合コマンドを変換する。
【０１１０】
[0124]規則（５２）、（５３）、および、（５４）は、スキップまたは割り当てによって開始する複合コマンドを変換する。これらのコマンドは、ＭＯＳＳにおけるそれらの対照に変換される。ここで留意すべきは、環境
【数６９】
0005409620.tif 000070
が後のコマンドＣを変換する場合に
【数７０】
0005409620.tif 000071
に更新されることがあるということである。
【０１１１】
[0125]規則（５５）は、条件節によって開始する複合コマンドを変換する。第１に、後のコマンドＣがＣに変換され、環境
【数７１】
0005409620.tif 000072
を生成する。次に、新たなラベルｆ’が生成され、Ｃを参照するために
【数７２】
0005409620.tif 000073
に追加される。そして、更新された環境
【数７３】
0005409620.tif 000074
が、双方にとって継続としての新たなラベルｆ’によって２つの分岐Ｃ１およびＣ２を変換するために使用される（コマンド変換が１つの規範事例のみを必要とするようにスキップが挿入される−規則（５１））。最後に、変換結果が最新の環境
【数７４】
0005409620.tif 000075
および対応するＭＯＳＳ条件節を使用して生成される。この規則において、新たなラベルｆ’は、条件分岐のいずれかがウェブ入力を含む場合に制御フローを再構成するために生成される。Ｃ１が、フォームａ：＝１；ｆｏｒｍＳ（．．．）；ａ：＝２からなると仮定する。規則（５５）は、分割目的コードを生成する−Ｃ１は、ａ←１；；ｉｎｐｕｔ（φ）のみであり、φに埋め込まれたリンクは、コードａ←２；；ｆ’（）を有する関数を指し示す。いずれの分岐もウェブ入力を含まない場合には、最適化されたバージョンが、より単純な目的コードを生成するために使用されることができ、それは容易であって省略される。
【０１１２】
[0126]規則（５６）は、ｗｈｉｌｅループを変換する。新たなラベルｆ’がループの開始点として生成される。ｆ’についてのいくつかのダミーコードが
【数７５】
0005409620.tif 000076
に挿入され、
【数７６】
0005409620.tif 000077
を生む。そして、
【数７７】
0005409620.tif 000078
は、継続としてｆ’によって（スキップによって付加された）Ｃを変換するために使用される。最後に、ｆ’のコードが最後の環境
【数７８】
0005409620.tif 000079
における条件節によって更新される。表現Ｅが真と評価された場合には、Ｃが実行され、Ｃが継続としてｆ’を使用することからループが形成される。Ｅが偽と評価された場合には、（Ｃ１から変換された）Ｃ１が実行され、したがって、ループを終了する。また、Ｃがウェブ入力を含まない場合には、最適化されたバージョンが使用されることができる。
【０１１３】
[0127]ウェブ入力の変換は、このセクションの冒頭に記載された直観およびフォーム符号化にしたがう。規則（５７）は、コマンドＣが後に続く単一使用フォーム
【数７９】
0005409620.tif 000080
を変換する。プログラムは、ここでは２つの部分に分割される。第１の部分Ｃ１は、変換結果において明確であるのに対して、第２の部分Ｃ２は、新たなラベルｆ’のもとで、結果としての環境
【数８０】
0005409620.tif 000081
に格納される。Ｃ１において、本発明者らは、クッキー値（ＣＩＤ）をｘｃｉｄに入れ、関数名ｓをｘｆｕｎに入れ（ｔｏＳｔｒｉｎｇ（ｆ’）は、関数名を固有文字列に変換する）、新たなトークンをｘｔｏｋに入れ、正当なトークンの集合に新たなトークンを含むように揮発性変数ａｓｔｏｋを更新し、ターゲットとしてのｆ’、初期環境Σから取得されたいくつかのデフォルト値
【数８１】
0005409620.tif 000082
（この決定は任意であり、他のデフォルト値が使用されることができる）、および、ｐａｃｋ（）を使用して生成された封印された状態を有するフォームを送信する。フォームが送信された場合に実行されるＣ２において、入力パラメータが型によって認証され、封印された状態が解凍され、リクエストの正当性がＥを使用して照合される。Ｅにおいて、ｘｃｉｄにおけるＣＩＤは、フォームが投入された攻撃者を検出するためにクッキーに対して比較され、単一使用フォームが２回送信されることを防止するためにトークンｘｔｏｋの正当性が照合され、偽造されたリンクを防止するためにターゲット名ｘｆｕｎが照合される。これらの全ての照合が成功したとすると、使用されたトークンｘｔｏｋは、正当なトークンａｓｔｏｋのリストから除去され、プログラムは、コマンドＣから変換されたＣによって開始する。さもなければ、プログラムは、エラーによって終了される。
【０１１４】
[0128]規則（５８）は、コマンドＣが後に続く複数使用フォーム
【数８２】
0005409620.tif 000083
を変換する。着想は、ａｍｔｏｋに格納された同じトークンが全ての複数使用フォームのために再利用されることを除いて規則（５７）と同様である（ａｍｔｏｋは他で初期化される）。コマンドＣ２において、認証および解凍後に、トークンｘｔｏｋがａｍｔｏｋとなおも一致するかどうかに関して照合が行われる（ａｍｔｏｋは、サーバプログラムが消去を使用する全てのクライアントフォームを無効にするように選択した場合に新たな値を与えられる）。
【０１１５】
[0129]最後のコマンド変換の場合が規則（５９）に記載される。消去により、揮発性変数ａｓｔｏｋおよびａｍｔｏｋがリセットされる。これは、規則（５７）および（５８）におけるフォーム変換が、埋め込まれたトークンのａｓｔｏｋおよびａｍｔｏｋに対する正当性を照合することから、クライアント上の全ての既存のフォームを有効に無効にする。
【０１１６】
[0130]変換が定義されたコマンドについて、完全ＢＡＳＳ世界の変換は、規則（６０）において提示される。ここで、実行されないプログラムに対応するもののみが変換され、クライアント履歴は空である。変換は、プログラムの開始点としてのｆｓｔａｒｔおよび終了点としてのｆｅｘｉｔという２つの特別なラベルを参照する。（スキップによって付加された）プログラム本体Ｃは、継続としてｆｅｘｉｔによって変換され、ｆｓｔａｒｔについてのエントリは、最後の環境
【数８３】
0005409620.tif 000084
において生成される。ｆｓｔａｒｔの本体は、ＢＡＳＳ環境
【数８４】
0005409620.tif 000085
および
【数８５】
0005409620.tif 000086
に基づくセッション環境およびローカルの環境を初期化し、ａｓｔｏｋおよびａｍｔｏｋに初期値を割り当てる。
【０１１７】
正当性およびプロトタイピング
[0131]これは、形式的変換を完了し、ＢＡＳＳの高水準意味論は、ＭＯＳＳにおけるトークンおよび封印された状態の注意深い操作を使用して強制実行される。ここで留意すべきは、ＢＡＳＳプログラムがＭＯＳＳにおける単一セッションに対応するということである。一度限りのウェブインタラクションおよびセキュリティにおける共通操作を処理する変換（コンパイラ）について、プログラムは、ウェブプログラミングの単純且つ簡潔な宣言型視点にしたがってＢＡＳＳにおいて作成されることができる。変換の正当性は、本セクションの全体にわたって略式に説明される。基本的なＢＡＳＳおよびＭＯＳＳは、双方とも、厳密な意味論を有することから、原則として、形式的に変換の正当性を証明することは可能である。
【０１１８】
[0132]他の正当性引数は、本願明細書に説明された全ての特性の保存にある。これは、先に提示されたフォーム符号化を検査することによって容易に確立されることができる。封印された状態が保護されることから、クライアント変更を受けるフォーム要素のみが入力パラメータである。関数名はまた、封印された状態に格納されることから、目的関数名における変更は成功しない。結果として、クライアントが目的リンクを偽造することができない−それらはサーバプログラムにアクセスするためにサーバ提供されたフォームにしたがうことができるのみであることから、ＢＡＳＳプログラムの制御フローは強制実行される。さらに、攻撃者は、他のクライアントになりすますことができない−攻撃者がクッキーを変更することがあるにもかかわらず、それ自身は他のクライアントの偽造不可能なＣＩＤにクッキーを設定することができない。より興味深いことに、攻撃者がクライアント内にフォームを投入することが必要である（規則（３６））ＣＳＲＦ、一次ＸＳＳ、および、セッションの固定化は、投入されたフォームがクライアントのクッキーに格納されるよりも異なるＣＩＤを有することから防止される。最後に、入力認証、セッション状態の回復、および、履歴管理は、全て適切に実行される。
【０１１９】
コンピュータシステムの例
[0133]図１４は、本願明細書に記載される１つ以上の動作を実行することがある、例示的なコンピュータシステムのブロック図である。図１４を参照すると、コンピュータシステム１４００は、典型的なクライアントまたはサーバコンピュータシステムを備えてもよい。コンピュータシステム１４００は、情報を通信するための通信機構またはバス１４１１と、情報を処理するためのバス１４１１と結合されたプロセッサ１４１２とを備える。プロセッサ１４１２は、限定されるわけではないが、Ｐｅｎｔｉｕｍ（商標）、ＰｏｗｅｒＰＣ（商標）、Ａｌｐｈａ（商標）等のマイクロプロセッサを含む。
【０１２０】
[0134]システム１４００は、さらに、プロセッサ１４１２によって実行される情報および命令を記憶するためにバス１４１１に連結されたランダムアクセスメモリ（ＲＡＭ）または（主記憶装置と称される）他の動的記憶装置１４０４を備える。主メモリ１４０４はまた、プロセッサ１４１２による命令の実行中に、一時的に変数または他の中間情報を記憶するために使用されてもよい。
【０１２１】
[0135]コンピュータシステム１４００はまた、プロセッサ１４１２のための静止情報および命令を記憶するためにバス１４１１に連結された読み出し専用メモリ（ＲＯＭ）および／または他の静的記憶装置１４０６と、磁気ディスクまたは光ディスクおよびその対応するディスク駆動装置等のデータ記憶装置１４０７とを備える。データ記憶装置１４０７は、情報および命令を記憶するためにバス１４１１に連結されている。
【０１２２】
[0136]コンピュータシステム１４００は、さらに、コンピュータユーザに情報を表示するためにバス１４１１に連結された陰極線管（ＣＲＴ）または液晶ディスプレイ（ＬＣＤ）等の表示装置１４２１に連結されてもよい。英数字および他のキーを含む英数字入力装置１４２２はまた、プロセッサ１４１２に情報およびコマンド選択を通信するためのバス１４１１に連結されてもよい。さらなるユーザ入力装置は、プロセッサ１４１２に方向情報およびコマンド選択を通信するために且つ表示装置１４２１上のカーソル移動を制御するためにバス１４１１に連結されたマウス、トラックボール、トラックパッド、タッチペン、または、カーソル方向キー等のカーソル制御装置１４２３である。
【０１２３】
[0137]バス１４１１に連結されてもよい他の装置は、紙やフィルム等の媒体、または、同様のタイプの媒体上の情報をマーキングするために使用されることがあるハードコピー装置１４２４である。バス１４１１に連結されてもよい他の装置は、電話またはハンドヘルドパーム装置と通信するための外部ネットワークインターフェース１４２０である。
【０１２４】
[0138]ここで留意すべきは、システム１４００の任意または全ての要素および関連するハードウェアが本発明において使用されてもよいということである。しかしながら、コンピュータシステムの他の構成が一部のまたは全ての装置を含んでもよいことはいうまでもない。
【０１２５】
[0139]本発明の多くの代替例および変更例が上述の記載を読んだ後に当業者にとって間違いなく明らかになるのに対して、当然のことながら、例示として示されて記載されたいかなる特定の実施形態も、決して限定して参酌されるように意図されるものではない。したがって、様々な実施形態の詳細の参照は、それら自体が本発明に欠くことのできないと考えられるそれらの特徴のみを列挙する特許請求の範囲を限定するように意図されるものではない。
【図１Ａ】
0005409620.tif 000087
【図１Ｂ】
0005409620.tif 000088
【図２】
0005409620.tif 000089
【図３】
0005409620.tif 000090
【図４】
0005409620.tif 000091
【図５】
0005409620.tif 000092
【図６】
0005409620.tif 000093
【図７】
0005409620.tif 000094
【図８】
0005409620.tif 000095
【図９】
0005409620.tif 000096
【図１０】
0005409620.tif 000097
【図１１】
0005409620.tif 000098
【図１２】
0005409620.tif 000099
【図１３】
0005409620.tif 000100
【図１４】
0005409620.tif 000101