(57)【要約】  アセンブリコードのための情報フロー実行を実施するための方法及び装置を開示する。一実施形態では、方法が、コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報を備えたタイミング注釈を有するアセンブリコードを受信するステップと、セキュリティポリシーに基づいて、前記アセンブリコードについて情報フローに関する検証を行うステップとを含む。【選択図】図４Ａ
2010503921.tif 000002
【特許請求の範囲】
【請求項１】
コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報を備えたタイミング注釈を有するアセンブリコードを受信するステップと、
セキュリティポリシーに基づいて、前記アセンブリコードに対して情報フローに関する検証を行うステップと
を含む方法。
【請求項２】
システムによって実行されると該システムに方法を実行させる命令を記憶している１つ又は複数の記録可能媒体を有する製品であって、
前記方法が、
コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報を備えたタイミング注釈を有するアセンブリコードを受信するステップと、
セキュリティポリシーに基づいて、前記アセンブリコードに対して情報フローに関する検証を行うステップと
を含む製品。
【請求項３】
注釈付きアセンブリコード、検証モジュール、コード修正モジュールを記憶するメモリであって、前記注釈付きアセンブリコードが、コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報を備えたタイミング注釈を有する、メモリと、
前記検証モジュールを実行して、セキュリティポリシーに基づいて前記注釈付きコードに対して情報フローに関する検証を行うプロセッサと
を備える装置。
【請求項４】
アセンブリコードに対してセキュリティ型維持翻訳を行うステップであって、コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報を備えたタイミング注釈を用いて前記コードに注釈付けを行うことを含む、ステップと、
前記アセンブリコードが実行された結果である情報フローのコンパイルを証明するステップと、
前記安全に型付けされたアセンブリコードがネットワークを介してダウンロードされることを可能にするステップと
を含む方法。
【発明の詳細な説明】
【優先権】
【０００１】
[1]本特許出願は、２００６年９月１４日に提出した、「Ｉｎｆｏｒｍａｔｉｏｎ  Ｆｌｏｗ  Ｅｎｆｏｒｃｅｍｅｎｔ  ｆｏｒ  ＲＩＳＣ−ｓｔｙｌｅ  Ａｓｓｅｍｂｌｙ  Ｃｏｄｅ  ｉｎ  ｔｈｅ  Ｐｒｅｓｅｎｃｅ  ｏｆ  Ｔｉｍｉｎｇ−Ｒｅｌａｔｅｄ  Ｃｏｖｅｒｔ  Ｃｈａｎｎｅｌｓ  ａｎｄ  Ｍｕｌｔｉ−Ｔｈｒｅａｄｉｎｇ」という名称の、対応する仮特許出願番号６０／８４４，９７４の優先権を主張し、参照のためにそれを組み込むものである。
【関連出願】
【０００２】
[2]本出願は、本発明の法人譲受人に譲渡された、２００５年１２月１９日に提出した「Ｉｎｆｏｒｍａｔｉｏｎ  Ｆｌｏｗ  Ｅｎｆｏｒｃｅｍｅｎｔ  ｆｏｒ  ＲＩＳＣ−Ｓｔｙｌｅ  Ａｓｓｅｍｂｌｙ  Ｃｏｄｅ」という名称の同時係属中の米国仮出願番号１１／３１６，６２１の出願に関連する。
【発明の分野】
【０００３】
[3]本発明は、プログラムの実行及びセキュリティの分野に関する。より詳細には、本発明は、アセンブリコードにおける情報フローの制約の実行に関する。
【発明の背景】
【０００４】
[4]情報フローの問題は、一般的に、異なるセキュリティレベル（例えば、高い低いなど）のデータ上で動作するプログラムに関するものである。本明細書では、実際には、低データとはすべてのユーザに開示してもよい公衆データであり、高データとはアクセスを制限する必要がある機密データである。不干渉などの情報フローポリシーは、一般的に、高入力データについての情報が低出力データを見ることによって推測できないことを要求する。実際には、セキュリティレベルは、一般化して格子にすることができる。
【０００５】
[5]言語ベースの技術は、このような情報フローの問題に対処するのに期待できるものとされてきた。それらの技術は、プログラムコードを直接調べることによって、情報フローのセキュリティを強力に保証するものである。それにもかかわらず、既存の言語ベースの情報フロー技術のほとんどは、高レベル言語に重点を置いている。アセンブリコードには高レベルの抽象概念（例えば、プログラム構造及びデータ構造）が欠如していることや、アセンブリコードがきわめてフレキシビリティが高いこと（例えば、メモリエイリアシングやファーストクラスコードポインタ）を主な理由として、それらの技術はアセンブリコードに適用されない。
【０００６】
[6]アプリケーションによってはアセンブリコードで配布されるもの（例えば、モバイルコンピュテーションのためのネイティブコード）や、直接アセンブリコードで書かれているもの（例えば、組み込みシステム）があるので、アセンブリコードについて情報フロー問題に対処することは有益である。このような状況で、型システムが提案されてきた。より具体的には、型システムとは、型注釈を使ってアセンブリコード中の欠けている抽象概念を復元し、また、型維持コンパイルを使って、ソースからターゲットへのセキュリティ証拠を維持するものである。ターゲットレベルにおいてセキュリティ型のチェックを直接行うことにより、コード消費者は、信頼できないコードの挙動がある特定の望ましい情報フローポリシーを満たすものであるという確信を得る。
【０００７】
[7]攻撃者が、プログラムのタイミング挙動など、秘密の情報フローチャネルを悪用することができる場合もあり得る。プログラムの実行時間（外部タイミング）を物理的に観察するか、又はスレッドの相互作用（内部タイミング）を悪用することによって、攻撃者は機密データについての情報を知ることができる。したがって、特に、抽象概念が欠如し極度なフレキシビリティを有するアセンブリコードについて、このようなタイミング関連の秘密チャネルが存在する場合の情報フローセキュリティを保護する解決策を得ることは有益である。
【０００８】
[8]秘密チャネル及びマルチスレッドについての従来の解決策に関しては、Ｖｏｌｐａｎｏ及びＳｍｉｔｈ著の「Ｅｌｉｍｉｎａｔｉｎｇ  Ｃｏｖｅｒｔ  Ｆｌｏｗｓ  ｗｉｔｈ  Ｍｉｎｉｍｕｍ  Ｔｙｐｉｎｇｓ」（１０ｔｈ  ＩＥＥＥ  Ｃｏｍｐｕｔｅｒ  Ｓｅｃｕｒｉｔｙ  Ｆｏｕｎｄａｔｉｏｎｓ  Ｗｏｒｋｓｈｏｐ、１５６−１６９ページ、ワシントンＤＣ、１９９７年６月）において、終了に敏感な不干渉が検討され、敏感なプログラムポイントではループの発生を許可しないことによって終端チャネルを閉じる型システムが提案されている。Ａｇａｔは、「Ｔｒａｎｓｆｏｒｍｉｎｇ  Ｏｕｔ  Ｔｉｍｉｎｇ  Ｌｅａｋｓ」（Ｐｒｏｃ．２７ｔｈ  ＡＣＭ  Ｓｙｍｐｏｓｉｕｍ  ｏｎ  Ｐｒｉｎｃｉｐｌｅｓ  ｏｆ  Ｐｒｏｇｒａｍｍｉｎｇ  Ｌａｎｇｕａｇｅｓ、４０−５３ページ、マサチューセッツ州ボストン、２０００年１月）の中で、プログラム変換を使用してタイミングの漏洩を防いだ。この場合、高分岐の実行時間は適切なダミー命令とのクロスパディングにより等化される。Ｓｍｉｔｈ及びＶｏｌｐａｎｏ著の「Ｓｅｃｕｒｅ  Ｉｎｆｏｒｍａｔｉｏｎ  Ｆｌｏｗ  ｉｎ  ａ  Ｍｕｌｔｉ−Ｔｈｒｅａｄｅｄ  Ｉｍｐｅｒａｔｉｖｅ  Ｌａｎｇｕａｇｅ」（Ｐｒｏｃ．２５ｔｈ  ＡＣＭ  Ｓｙｍｐｏｓｉｕｍ  ｏｎ  Ｐｒｉｎｃｉｐｌｅｓ  ｏｆ  Ｐｒｏｇｒａｍｍｉｎｇ  Ｌａｎｇｕａｇｅｓ、３５５−３６４ページ、カリフォルニア州サンディエゴ、１９９８年１月）は、ここでも敏感なプログラムポイントではループの発生を許可しないことによって、マルチスレッド言語のための可能的不干渉を確立した。Ｓａｂｅｌｆｅｌｄ及びＳａｎｄｓ著の「Ｐｒｏｂａｂｉｌｉｓｔｉｃ  Ｎｏｎｉｎｔｅｒｆｅｒｅｎｃｅ  ｆｏｒ  Ｍｕｌｔｉ−Ｔｈｒｅａｄ  Ｐｒｏｇｒａｍｓ」（Ｐｒｏｃ．１３ｔｈ  ＩＥＥＥ  Ｃｏｍｐｕｔｅｒ  Ｓｅｃｕｒｉｔｙ  Ｆｏｕｎｄａｔｉｏｎｓ  Ｗｏｒｋｓｈｏｐ、２００−２１４ページ、イギリスのケンブリッジ、２０００年７月）は、スケジューラ非依存のセキュリティ状態に関して、確率的不干渉結果を証明した。これらのシステムは、ソースレベルプログラムのための情報フローセキュリティに対処しており、アセンブリコードには当てはまらない。
【０００９】
[9]型付けされたアセンブリ言語の観点から、近年、ターゲットコードレベルにおいて情報フローセキュリティを直接実行することに向けた努力がなされている。しかし、そのような作業はどれも、秘密チャネル及び／又はマルチスレッドに取り組んではいない。そのため、それらの解決策を、秘密チャネルやスレッドの相互作用が容易に攻撃されうる現実のシナリオに適用する際に、困難が生じる。
【発明の概要】
【００１０】
[10]アセンブリコードのための情報フロー実行を実施するための方法及び装置を開示する。一実施形態では、方法が、コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報を備えたタイミング注釈を有するアセンブリコードを受信するステップと、セキュリティポリシーに基づいて、前記アセンブリコードについて、情報フローに関する検証を行うステップとを含む。
【００１１】
[11]本発明は、以下に記載の詳細な説明、及び添付の本発明の様々な実施形態の図面を見ることでさらに十分に理解されよう。しかし、それらは、本発明を具体的な実施形態に限定するものと解釈されるべきものではなく、説明及び理解を目的としたものにすぎない。
【発明の詳細な説明】
【００１２】
[12]タイミング関連の秘密チャネル及びマルチスレッドが存在する場合のアセンブリコード（例えば、ＲＩＳＣ型のアセンブリコード）のための情報フロー実行を開示する。本発明の実施形態は、ＲＩＳＣ型のアセンブリコードの情報フローセキュリティを保証する型システムの分野に関する。アセンブリコードは、型付け注釈で拡張される。型付け規則に導かれた型チェッカーは、拡張されたコードを調べて、そのコードがある特定の情報フローポリシーを満たすかどうかを判断する。
【００１３】
[13]本発明の実施形態は、シーケンシャルコード及びマルチスレッドコードの両方について情報フローセキュリティを保護し、攻撃者がタイミング関連の秘密チャネルにアクセスできるとしても適用可能である。本発明は、異なる実施形態において、終了、タイミング、可能的及び／又は確率的チャネルが存在する場合の情報フローセキュリティに対処する。
【００１４】
[14]アセンブリコードの情報フローセキュリティのための一連の型システムを開示する。これらのシステムは、タイミング注釈と関連する判断及び規則とを含む。異なるタイミング規則を使用することによって、これらのシステムを異なる実際の設定に適用することができる。特に、それらを使って、シーケンシャルプログラムにおける終端チャネル及びタイミングチャネル、並びにマルチスレッドプログラムにおける可能的チャネル及び確率的チャネルを通じた不正な情報フローを防ぐことができる。
【００１５】
[15]以下に、一般的な型システムＴＡＬＣ＋としてのこれらの型システムの正規の詳細を提示し、また、認証コンパイルにおけるその使用法を説明する。ＴＡＬＣ＋の異なる「パラメータ」を使って、終了に敏感な不干渉ポリシー、タイミングに敏感な不干渉ポリシー、可能的不干渉ポリシー、及び確率的不干渉ポリシーのそれぞれに対処する一連の型システム及び認証コンパイルスキームを得ることができる。さらに、それらの「パラメータ」の組合せを使って、上記ポリシーの組合せに対処するシステムを得ることができる。
【００１６】
[16]次の説明では、多数の詳細を明記して、本発明をより完全に説明する。しかし、当業者には、それらの具体的な詳細がなくても本発明を実施できることが明らかになろう。他の例では、本発明をわかりにくくすることを避けるために、よく知られている構造及びデバイスは詳細にではなくブロック図の形態で示す。
【００１７】
[17]以下の詳細な説明の一部は、コンピュータメモリ内のデータビット上のオペレーションのアルゴリズム及び記号表現に関するものである。それらのアルゴリズムの記載及び表現は、データ処理技術の当業者が、自分の作業の内容をその分野の他の当業者に最も効率的に伝達するために使用する手段である。本明細書では、また一般的にも、アルゴリズムとは、所望の結果につながる自己無撞着ステップシーケンスであると考えられている。それらのステップは、物理量の物理的操作を必要とするステップである。通常、必ずというわけではないが、これらの量は、保存、転送、結合、比較、及びそれ以外の操作を行うことが可能な、電気又は磁気信号の形態をとる。主として一般的な使用法であるという理由から、これらの信号を時にはビット、値、要素、記号、文字、用語、又は数などと呼ぶことが便利であることがわかっている。
【００１８】
[18]しかしながら、これら及び同様の用語はすべて、該当する物理量に関連付けるべきものであり、また、それらの量に貼られる便利なラベルにすぎないことを心に留めておくべきである。以下の議論から明らかなように、別途明確に記載していない限り、この説明を通して、「処理」、「コンピューティング」、「算出」、「決定」、「表示」などの用語を使った議論は、コンピュータシステムのレジスタやメモリ内の物理（電子）量として表されたデータを操作及び変換して、そのコンピュータシステムのレジスタやメモリ内、又はその他のそのような情報記憶装置、伝送装置又は表示装置内の同じく物理量として表された他のデータにする、コンピュータシステム、又は同様の電子コンピューティングデバイスのアクション及びプロセスについてのものであることを理解されたい。
【００１９】
[19]本発明はまた、本明細書におけるオペレーションを実施するための装置に関する。この装置は、要求される目的のために特別に組み立てられたものであってもよいし、或いは、内部に保存されたコンピュータプログラムによって選択的に起動又は再構成される汎用コンピュータから成るものであってもよい。そのようなコンピュータプログラムを、コンピュータ読み取り可能記憶媒体に記憶することができる。コンピュータ読み取り可能記憶媒体は、フロッピーディスク、光ディスク、ＣＤ−ＲＯＭ、光磁気ディスクを含む任意の種類のディスク、読み出し専用メモリ（ＲＯＭ）、ランダムアクセスメモリ（ＲＡＭ）、ＥＰＲＯＭ、ＥＥＰＲＯＭ、磁気又は光カード、或いは電子命令を記憶するのに適した任意の種類の媒体などで、それぞれがコンピュータシステムバスに連結されるものであるが、それらに限定されるものではない。
【００２０】
[20]本明細書で提示されるアルゴリズム及び表示は、本来的にいずれかの特定のコンピュータ又はその他の装置に関連するものではない。本明細書での教示に従って、様々な汎用システムをプログラムと共に使用することができる。或いは、必要な方法ステップを実施するためには、より特殊化された装置を組み立てるのが便利であることがわかる場合もあろう。様々なこれらのシステムに必要な構造が、以下の説明から明らかになろう。さらに、本発明は、いずれかの特定のプログラミング言語に関して記載したものではない。本明細書に記載されているように本発明の教示を実装するために様々なプログラミング言語を使用できることを理解されたい。
【００２１】
[21]マシン読み取り可能媒体には、マシン（例えば、コンピュータ）が読み取り可能な形態で情報を記憶又は伝送するための任意のメカニズムが含まれる。例えば、マシン読み取り可能媒体には、読み取り専用メモリ（「ＲＯＭ」）、ランダムアクセスメモリ（「ＲＡＭ」）、磁気ディスク記憶媒体、光記憶媒体、フラッシュメモリデバイス、電気、光、音響、又はその他の形態の伝達信号（例えば、搬送波、赤外線信号、デジタル信号など）などが含まれる。
【００２２】
概略
セキュリティ型システム
[22]以下に、型システムを使ってソース言語のための情報フローセキュリティに対処する方法を簡単に説明する。
【００２３】
[23]図１Ａに示す単純な言語について考察する。この言語では２つのセキュリティレベル、低と高が使用されている。環境（Φ）は、変数（Ｖ）のセキュリティレベル（ｔ）を指定する。便宜上、ｈ（及びｈ１、ｈ２、．．．）及びｌ（及びｌ１、ｌ２、．．．）を使って、それぞれ、高変数、低変数を表す。式（Ｅ）は定数（ｉ）、変数（Ｖ）、又は加算である。コマンド（Ｃ）はすべて共通である。高変数から低変数への情報の流れがあってはならないというポリシーが望ましい。より具体的には、以下のような、何種類かの不正な情報フローが妨げられる。
１．ｌ：＝ｈなど、割当てによる明示的フロー。
２．ｉｆ  ｈ  ｔｈｅｎ  ｌ：＝１  ｅｌｓｅ  ｌ：＝０など、プログラム構造（条件文やｗｈｉｌｅループ）による暗示的フロー。
３．ファーストクラスオブジェクト及び／又は関数で拡張した場合は、データ及び／又はコードポインタを通じたさらなる暗示的フローが生じる。
【００２４】
[24]上記の単純な言語については、セキュリティ型システムは一般的に以下を含む。
１．式の型におけるセキュリティレベルを追跡すること。これは、明示的フローを通じた情報漏洩を防ぐのに役立つ−割当てにおけるセキュリティレベルの不整合を許可しない。
２．プログラムカウンタ（ＰＣ）にセキュリティレベルを付けること。条件式が高いレベルで保護されている場合、その分岐については、高ＰＣのもとで型チェックが行われる。これは、本質的には、低変数への更新が許可されない「敏感な領域」に分類されるものとして、分岐に印を付けることである。この考え方は、ｗｈｉｌｅループなどの他のプログラム構造にも当てはまる。
３．ポインタを有する言語では、ポインタに２種類のセキュリティレベルが与えられる−１つはポインタのセキュリティレベルであり、もう１つは、参照されるデータ又はコードのセキュリティレベルである。ポインタを通じた不正フローは、ポインタがアクセスされたときにその２つのセキュリティレベルについて適切なチェックを行うことで防ぐことができる。
【００２５】
[25]図１Ｂは、これらの考え方のうち最初の２つを反映した単純なセキュリティ型システムを示す。そこでの規則については、当業者であれば十分に理解されよう。規則［Ｃ４］（小前提）が、高い計算を低いセキュリティコンテキストに含めることを認めるのに役立つことに注意されたい−敏感なコンテキストにおいてあるコードを実行することが安全であるならば、敏感ではないコンテキストにおいてその同じコードを実行することも安全であるはずである。
【００２６】
ＴＡＬＣ
[26]ＴＡＬＣは、２００５年１２月１９日に出願され、本発明の法人譲受人に譲渡された「Ｉｎｆｏｒｍａｔｉｏｎ  Ｆｌｏｗ  Ｅｎｆｏｒｃｅｍｅｎｔ  ｆｏｒ  ＲＩＳＣ−ｓｔｙｌｅ  Ａｓｓｅｍｂｌｙ  Ｃｏｄｅ」という名称のＵＳ２００５０００３１６６２１に記載されており、アセンブリコードについての情報フロー問題を扱っている。その中に記載されている主な課題の１つが、アセンブリコードはソースコードほど多くの抽象概念を提供してくれないということである。ソースコードのプログラム構造は様々なプログラムポイントのセキュリティレベルを決定するのに役立つのだが、そのような構造はアセンブリコードでは利用できない。例えば、両方の分岐がガード式のセキュリティレベルを考慮するように、ソースプログラム中の条件文をチェックすることができる。このようなチェックはアセンブリコードにおいては難しい。アセンブリコードでは、「扁平な」制御フローがプログラム構造を特定するのにほとんど役立たないからである。条件文は、一般的に、分岐命令及びいくつかのコードブロックに解釈され、そこでは分岐の終了ポイントが明白ではない。
【００２７】
[27]ＴＡＬＣは、型注釈を使って、欠如している構造を回復する。これらの注釈は、命令のセキュリティレベル並びにそのセキュリティレベルの終了ポイントについての明示的な情報を提供してくれる。一実施形態では、２つのセキュリティオペレーションを使って注釈を操作し、また、適切な型付け規則を使って、それらの注釈がコードの実際の構造を忠実に反映していることを確認する。
【００２８】
[28]ＴＡＬＣの簡略版の構文を図２に示す。元のＴＡＬＣと比べると、スタック及び多相性が省略されている。これは、スタック及び多相性が主にソースプログラム中の関数やプロシージャをサポートするためのものであり、それらの取り扱いは、本明細書で記載している拡張とは直交するためである。記号θを使ってセキュリティレベルを表す。セキュリティコンテキスト
【数１】
2010503921.tif 000003
は、プログラムポイントｌに到達するまではＰＣのセキュリティレベルがθ以上でなければならないことを表す。
【００２９】
[29]ｒａｉｓｅ  κオペレーションはセキュリティレベルを上げるために使用され、これは、高条件文によって始まる領域などの敏感な領域の開始に対応する。ｌｏｗｅｒ  ｌはセキュリティレベルを復元するために使用され、これは、敏感な領域の終了を表すものである。ソースプログラムの構造及び型付けに基づいた認証コンパイルプロセスによって、これらの２種類のセキュリティオペレーションをターゲットコード中に入れることができる。
【００３０】
[30]これらにより、すべてのプログラムポイントのセキュリティレベルが、注釈（コンテキスト）を通して明らかになる。高コンテキストにおいて高分岐が生じ、高コンテキストにおける低データへの割当てが許可されない。さらに、あらゆる参照セルには２種類のセキュリティレベルが与えられる−１つはポインタのセキュリティレベルであり、もう１つは、参照されるデータ又はコードのセキュリティレベルである。
【００３１】
[31]図３は、ＴＡＬＣプログラムの例を示す。これは、セキュリティ型付けされたソースプログラムから解釈されたものである。ソースプログラムには、低変数ａと、２つの高変数ｂ及びｃが含まれている。対応するＴＡＬＣプログラムでは、ｌａ、ｌｂ、ｌｃとラベル付けされたヒープセルを使って、それらの変数を表している。ＴＡＬＣプログラムは、低セキュリティコンテキスト・中のラベルｌ０とラベル付けされたコードから始まっている。初期設定の後、ＴＡＬＣプログラムはそのセキュリティコンテキストを
【数２】
2010503921.tif 000004
に上げる。式中、Τは、セキュリティレベルが高であることを表す。次いで、制御はｌ１とラベル付けされたコードに移される。このコードは、高変数ｂに対するテストを含み、２つの別個の分岐への実行を指示している。この条件文の分岐のどちらにおいても、高変数ｃが更新され、セキュリティコンテキストはｌｏｗｅｒ  ｌ３で復元される。次いで、ｌ３のコードは、低変数ａを再び更新することができる。
【００３２】
[32]関数及びポインタに対するサポート、正確な意味論及び正確な照明、並びにＴＡＬＣをターゲットとした認証コンパイルスキームを含むさらなる詳細については、Ｙｕ及びＩｓｌａｍ著の「Ａ  Ｔｙｐｅｄ  Ａｓｓｅｍｂｌｙ  Ｌａｎｇｕａｇｅ  ｆｏｒ  Ｃｏｎｆｉｄｅｎｔｉａｌｉｔｙ」（技術レポートＤＣＬ−ＴＲ−２００５−０００２、ＤｏＣｏＭｏ  Ｃｏｍｍｕｎｉｃａｔｉｏｎｓ  Ｌａｂｏｒａｔｏｒｉｅｓ  ＵＳＡカリフォルニア州サンホセ、２００５年３月、ｈｔｔｐ：／／ｗｗｗ．ｄｏｃｏｍｏｌａｂｓｒｅｓｅａｒｃｈｅｒｓ−ｕｓａ．ｃｏｍ／−ｄｙｕ／ｔａｌｃ−ｔｒ．ｐｄｆ）を参照されたい。
【００３３】
[33]以下に、様々なセキュリティ上の前提のもとで適用可能な、ＴＡＬＣに対する一連の拡張について説明する。これは、不干渉のための低レベルの型システムと実際の用途との間のギャップを埋めるものである。特に、これらの拡張は、以下に説明し、本明細書でＴＡＬＣ＋と呼ぶ一般的なフレームワークに完全に適合するものである。このように、一般的な型付けされたアセンブリ言語が「カスタマイズされた」不干渉（終了に敏感な、タイミングに敏感な、可能的、確率的、そして単純な）のために利用可能になる。
【００３４】
タイミング関連のチャネル
[34]本明細書では、いくつかの実際的な設定における、アセンブリコードのための情報フローセキュリティに対処するために使用することができる実施形態について説明する。シーケンシャルプログラムについては、終端チャネル及びタイミングチャネルを含み、いくつかの秘密チャネルを閉じるための型システムを説明する。マルチスレッドプログラムについては、可能的且つ確率的不干渉を保証する型システムを説明する。一実施形態では、プログラム実行のタイミングを記録するための追加注釈を含むように、前記の型システムＴＡＬＣを拡張する。これらのタイミング注釈を使って、高セキュリティコンテキストにおいてはループがないことなどの、様々なソースレベルの制約を表現する。
【００３５】
[35]異なるタイミング注釈を使って、異なる情報フローチャネルに対処する。しかし、それでも、基本的な型システムには多くの類似点がある。異なる「タイミング規則」が与えられると、異なる情報フローチャネルに対処する一般的な型システムＴＡＬＣ＋が公式化される。本発明の実施形態の詳細を、この一般的な型システムの観点から説明する。この一般的な型システムに異なる「パラメータ」を与えることにより、様々な状況に対応した特殊化した型システムが得られる。
【００３６】
[36]図４Ａは、情報フロー実行のためのプロセスの一実施形態の流れ図である。このプロセスは、ハードウェア（例えば、電気回路、専用ロジックなど）、ソフトウェア（汎用コンピュータシステム又は専用マシンにおいて実行されるようなもの）、又はその両方の組合せを含むことができる処理ロジックにより実行される。
【００３７】
[37]図４Ａを見ると、そのプロセスは、処理ロジック受信アセンブリ又はその他の安全に型付けされたネイティブコードにより開始する（処理ブロック４０１）。一実施形態では、処理ロジックはそのコードをネットワークロケーションからダウンロード又は検索することにより受信する。
【００３８】
[38]一実施形態では、安全に型付けされたネイティブコードは、セキュリティ型維持翻訳がなされたアセンブリコードを含む。セキュリティ型維持翻訳には、コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報及びタイミング注釈でアセンブリコードに注釈付けを行うことが含まれる。一実施形態では、並列チャネルはマルチスレッドに関連付けられる。一実施形態では、タイミング関連秘密チャネルは、１つ又は複数の終端チャネル、タイミングチャネル、可能的チャネル、及び確率的チャネルを含む。
【００３９】
[39]一実施形態では、タイミング注釈はソースレベルの制約を表現する。一実施形態では、タイミング注釈には、コマンドが実行されるのに必要な時間の量を表す時間値を特定する第１の注釈と、コマンドに関連付けられたタイミングが指定期間の後に変更可能であることを特定する第２の注釈と、特定のセキュリティレベルのもとでコマンドが実行されるための許容できるタイミングを特定する第３の注釈と、コマンドに関連付けられたタイミングが特定のセキュリティレベルの下での時間の経過に一致することを特定する第４の注釈とから成るグループが１つ又は複数含まれる。一実施形態では、タイミング注釈が、アセンブリコードの一部の実行に関連付けられたタイミング情報の観察を可能にするための観察可能なアクションシーケンスに関連付けられた実行時間を表す。一実施形態では、タイミング注釈が、分岐命令の分岐の両方が同じタイミング挙動を示すことを明らかにするためのチェックを可能にする。一実施形態では、分岐命令の両方の分岐が、特定のセキュリティレベルで識別されたコードの終了においてそれらの分岐が同じ時間で合流した場合に、同じタイミング挙動を示す。一実施形態では、タイミング注釈が、第１のセキュリティレベルよりも高い第２のセキュリティレベルを有するコードの領域において第１のセキュリティレベルの変数の出力又は更新が行われないことを確認するためのチェックを可能にする。一実施形態では、注釈が、所定の情報に基づく２つの実行パスが出会うコードの領域の開始と終了を表すためのオペレーションも含む。
【００４０】
[40]コードを受け取った後、処理ロジックは、安全に型付けされたネイティブコードの情報フローに関して、セキュリティポリシーに基づき検証を行う（処理ブロック４０２）。検証は、装置（例えば、携帯電話などの携帯装置）において、その装置がそのコードを実行する前に行われる。一実施形態では、処理ロジックは、コードの挙動を統計的にチェックして、そのコードがセキュリティポリシーに違反していないかどうかを判断することにより検証を行う。一実施形態では、コードが実行されたときに、識別された型情報がそのコードを実行したデバイスから流出しなかった場合に、そのコードはセキュリティ（安全）ポリシーに違反していないということになる。言い換えれば、アセンブリコードが実行されたときに、そのアセンブリコードの制御下において生じる情報フローを検証する。
【００４１】
[41]検証によりコードがセキュリティポリシーに違反していないと判断された場合には、処理ロジックはそのコードからあらゆる注釈を除去して（処理ブロック４０３）、そのコードを実行する（処理ロジック４０４）。
【００４２】
[42]図４Ｂは、図４Ａの情報フロー実行を実装することができる環境を説明する図である。図４Ｂを見ると、プログラム４５０に対して、セキュリティポリシー４５２に基づくセキュリティ型推測４５１がなされる。その結果が、セキュリティ型付けプログラム４５３である。認証コンパイラ５４５は、プログラム４５３をコンパイルし、その結果、安全に型付けされたターゲットコード４５５を生成する。
【００４３】
[43]安全に型付けされたターゲットコード４５５を家庭用装置によってダウンロードすることができる。家庭用装置は、携帯電話、又は以下のようなその他のモバイルデバイスであってよい。家庭用装置は、コード４５５を実行する前に、安全に型付けされたターゲットコード４５５上で検証モジュール４６０を実行する。検証モジュール４６０は、型チェッカーとして動作しながら、セキュリティポリシー４５２に基づいて検証を行う。
【００４４】
[44]家庭用装置はまた、コード４５５を実行する前に、安全に型付けされたターゲットコード４５５上で削除モジュール４７０を実行して、認証コンパイラ４５４によってコードに追加された注釈を削除する。
【００４５】
[45]検証モジュール４６０がコードが安全であると判断した場合、又は、セキュリティポリシー４５２に基づいてその他の方法でコードが許容できると検証した場合には、検証モジュール４６０は、家庭用装置（例えば、家庭用装置上のプロセッサ）が安全に型付けされたターゲットコード４５５を実行してもよいという信号を、家庭用装置に送る。
【００４６】
[46]本発明の様々な実施形態の詳細を、抽象言語ＴＡＬＣ＋を使って以下に記載する。
【００４７】
終端チャネル
[47]本明細書に記載の技術を使って、情報フローセキュリティに関連するいくつかの異なる問題に取り組む。理解し易いように、以下では、シーケンシャルプログラムにおける終端チャネルについてより詳細に述べる。
【００４８】
[48]ＴＡＬＣは、プログラムの挙動を観察する手段として、プログラムの変数（又はアセンブリコードのヒープファイル及びレジスタファイル）の内容を検査することを前提とする。実際には、変数を超えるいくつかの秘密チャネルが存在する。代表的な例の１つが終端チャネルである。より具体的には、攻撃者は、プログラムが終了するかどうかを観察することもでき得る。
【００４９】
[49]終端チャネルを悪用することによって、攻撃者は不正な情報フローを組み立てることができる。以下の２つの例では、いかなる低変数も更新されない。にもかかわらず、プログラムが終了するかどうかを観察することによって、高変数ｈの値を知ることができる。
１．非終了高ループ：ｗｈｉｌｅ  ｈ  ｄｏ  ｓｋｉｐ；
２．高条件文中の非終了ループ：ｉｆ  ｈ  ｔｈｅｎ｛ｗｈｉｌｅ  ｔｒｕｅ  ｄｏ  ｓｋｉｐ｝ｅｌｓｅ  ｓｋｉｐ．
【００５０】
[50]一実施形態では、すべてのｗｈｉｌｅループが最小限の型付けであるｌｏｗを有するように制約されている。これは保守的なアプローチであることに注意されたい。なぜならば、終了ループでさえも潜在的に非終了であるとみなされているからである。これは、型システムにおいて、低プログラムカウンタ（ＰＣ）のもとでのみｗｈｉｌｅループを許可するという形で反映されている。より具体的には、ＰＣがループについてｌｏｗでなければならないためには、図１Ｂの型システムにおいてたった１つの型付け規則、すなわち［Ｃ６］を変更しさえすればよい。
【数３】
2010503921.tif 000005
【００５１】
[51]この変更は、ソースレベルプログラムにおける終端チャネルを閉じる。前に述べた第１の例では、高ループが許可されなくなる。なぜなら、そのループの高レベルの保護は、低ＰＣのもとでは型付けすることができないからである。第２の例では、高条件文におけるループも許可されなくなる。なぜならば、高条件文の本体は高ＰＣであるが、ループは低ＰＣのもとでのみ許可されるからである。本質的には、ループ構造はこのような分析の鍵となる。なぜならば、ループ構造は高分岐が終了すべきであることを強制するからである。上記の解決策は、ソースプログラムには適用できるが、アセンブリコード対しては機能しない。
【００５２】
[52]型付けされたアセンブリ言語では、ループを容易に識別することができない。なぜならば、ループと条件式はともに、分岐命令を使って実装されるからである。一実施形態では、高分岐の終了は特別に設計された注釈で実行される。ＴＡＬＣのセキュリティ注釈は高分岐を識別するのに便利である−分岐は、高コンテキストを有するとき且つそのときに限り、高である。一実施形態では、この先頭において、低領域に戻る前に実行ステップの上界に印を付けるいくつかの追加タイミング注釈が、高分岐に付けられる。ＴＡＬＣの解決策は、高分岐の終了が結局は、低領域において、一致する低変数と合流することを保証する。追加タイミング注釈は、高分岐が必ず終了することを保証するものである。
【００５３】
[53]より具体的には、一実施形態では、タイミングタグｔがこの目的で使用されている。この場合、ｔは、自然数（せいぜいこの数のステップ内では実行によっても現在の高領域のままであることを表す）か∞（「未知」又は「潜在的に無限」を表す）である。高コンテキストのもとでは、型システムは、両方の分岐が有限のタイミングタグを有する場合にのみ分岐命令を許可する。言い換えれば、高分岐においては、プログラムの２回の実行が分かれる場合があるが、低領域において有限数のステップで合流する。これは、将来、潜在的に非終了の「後方へのジャンプ」を防ぐ。分岐命令の２つの分岐が異なるタイミングタグを有する場合があることに注意されたい。分岐命令自体にタイミングタグを与えた場合には（入れ子分岐の場合に必要）、長い方の分岐を考慮する。なぜならば、タイミングタグは、本質的に、現在の高領域を出る前の実行ステップの上界だからである。
【００５４】
[54]これらのタイミング注釈は、セキュリティ型付けされたソースコードのコンパイルから得られる。一実施形態では、条件文は、両方の分岐が有限のタイミングをもたらすとき且つそのときに限り有限のタイミングでコンパイルされ、ループは、無限のタイミングで保守的にコンパイルされる。これは、図５及び図６（ｂとｃの両方が高変数）で説明している。図５及び図６では、本発明をわかりにくくすることを避けるため、タイミング注釈及びその他の注釈のみ省略してある。
【００５５】
[55]ループは∞でのみ型付けできることに注意されたい。図６の場合を調べてみると、いかなる有限タイミングもコードブロックｌ２中のｊｍｐ  ｌ１の後方へのジャンプに対して機能しない。同様の推理に基づき、前に挙げた２つのソースレベルの反例についても、有限タイミングで型付けすることはできない。高領域において有限タイミングの注釈のみを許容することによって、型システムはそれらのループを拒否する。
【００５６】
[56]このようなタイミング注釈はまた、非再帰のループフリー関数もサポートすることができる。なぜならば、そのような関数の本体には有限のタイミング注釈を与えることができるからである。コードの再使用をサポートするためには、以下の例のように、多相性の単純な形態を導入することが役立つ。
ｆ：∀ｍ．＜ｍ＋３＞｛ｒ０：（ｍ）｝
コストが２かかる何かを行う
（ｍ＋１）ｊｍｐ  ｒ０
【００５７】
[57]この「タイミング後の」多相性は、本質的に、異なる型付けコンテキストについて同じ関数の複数のコピーを宣言するものである。一実施形態では、どのコピーを使用すべきかに関する決定が、型のインスタンス化を使って、使用サイト（ｕｓｅ  ｓｉｔｅ）で行われる。
【００５８】
[58]要約すると、高コンテキストにおいて潜在的に非終了の構造（例えば、ループや再帰関数）を許可しないことによって、終端チャネルが閉じられる。アセンブリコードにおける、部分的なオペレーションによって生じる補足されない例外などの異常終了についてのサポートは、高領域において部分的なオペレーションを許可しないことによって簡単に行える。
【００５９】
ＴＡＬＣ＋
[59]上記の考え方を実装する型付けされたアセンブリ言語ＴＡＬＣ＋について、以下に説明する。特に、ＴＡＬＣ＋はＴＡＬＣ（図２の版を使用しており、そこで説明したように、タイミング挙動に直交する機能は省略してある）の拡張である。
【００６０】
[60]ＴＡＬＣによると、セキュリティラベルは格子Ｌを形成する。変数θを使って、Ｌの要素を網羅する。記号⊥及びΤを格子の下部と上部として使用し、∪及び∩をｌａｔｔｉｃｅ  ｊｏｉｎオペレーション及びｌａｔｔｉｃｅ  ｍｅｅｔオペレーションとして使用し、⊆をｌａｔｔｉｃｅ  ｏｒｄｅｒｉｎｇとして使用する。
【００６１】
[61]構文拡張の一実施形態を図７に示す。タイミング注釈ｔは、自然数ｎ又は特別な∞のいずれかである。それらは、コード型及びコード値において、セキュリティコンテキストκに付随するものである。
【００６２】
[62]図８では、タイミング注釈用に型付け判断が拡張されている。命令シーケンス及びプログラムが、ｔに関してさらにチェックされる。一実施形態では、タイミング注釈の４つの判断形態が使用されている。これらの４つの判断形態の異なる定義を使うことによって、様々な情報チャネルを閉じるための型システムが得られる。終端チャネルについては図９に定義を示す。その他のチャネルについての定義はさらに以下に説明する。
【００６３】
[63]［ｃｏｍｍ］＝ｎという判断は、プログラム実行の間の時間経過を追跡するために設計されている。終了に関しては、任意のアセンブリコマンド（又はセキュリティオペレーション）を一単位の時間を消費するものとして考えれば十分である。時間の経過
【数４】
2010503921.tif 000006
は、低セキュリティコンテキスト⊥には無関係である。その他のセキュリティコンテキストでは、ｔがｔ´とｔ´´の合計以上であることが要求される。ここで、∞を用いても機能するように、加算＋を簡単に拡張する。低セキュリティコンテキスト⊥の下では、いかなるタイミングも容認され得る。対照的に、高セキュリティコンテキストの下では、タイミングが有限であり且つ有限である場合に限って、容認され得る。最後に、マッチングタイミングθ├ｔ〜ｔ´は終端チャネルのための役割を果たさないため、自明に有効であるように定義される。それは、後のセクションにおける拡張のための代替物である。
【００６４】
[64]拡張された型付け規則の一実施形態を図１０及び図１１に例示する。一実施形態では、ＴＡＬＣ＋において、非命令のための規則についてＴＡＬＣにわずかな変更だけが施される。明らかに、プログラムをチェックするための規則においては余分の不変部分がある。すなわち、コンテキストκのセキュリティレベルに関して、タイミングｔはＯＫでなければならない。この場合、ＳＬ（κ）を使ってκのセキュリティラベルコンポーネントを表し、ＳＬ（・）は⊥と定義される。
【００６５】
[65]一実施形態では、図１１に示すａｄｄ、ｌｄ、ｍｏｖ、ｓｔのための規則が、すべて同じ方法で拡張される。図１１を参照すると、時間経過に対する余分のチェックを行って、タイミング注釈が実際の命令に一致することを確認する。命令ｂｎｚは、２つの潜在的な継承条件を有する。したがって、時間経過に関して、両方の分岐に対しチェックが行われる。このマッチング判断は、差し当たって自明に有効である。
【００６６】
[66]一実施形態では、ｒａｉｓｅにより印が付けられた新しいセキュリティコンテキストに入る際に、新しいタイミングｔ´がチェックされて、新しいセキュリティレベルθ´のもとでＯＫであるかどうかが判断される。さらに、時間経過もチェックされる。これは、現在のセキュリティレベルθが⊥ではないかもしれないマルチレベルセキュリティ格子においては役に立つ。この点で、新しいコンテキストκ´の終了ポイントω´のタイミングｔ１を直接チェックする必要はない。一実施形態では、ｌｏｗｅｒについて、θのもとでＯＫである時間経過がチェックされる。最も低いセキュリティレベルに行く場合には、これは自明に有効である。
【００６７】
[67]一実施形態では、ｊｍｐについて、時間経過がチェックされる。一実施形態では、ｈａｌｔについては特に何も必要とされない。ＴＡＬＣは、空のセキュリティコンテキストにおいてはｈａｌｔを許可する。このようなコンテキストでは、すべてのタイミング注釈がＯＫである。
【００６８】
認証コンパイル
[68]一実施形態では、最小限のソース言語からセキュリティ型を維持する翻訳が使用される。より具体的には、このソース言語は、図１Ｂの型システムが規則［Ｃ６´］で改造された場合の図１Ａのソース言語である。これによって簡潔な提示が可能になり、それは、簡潔ではあるが、アセンブリコードにおいて終端チャネルを閉じるためのタイミング注釈の使用、という主要な提案を明示するのに十分である。
【００６９】
[69]図１Ａの高低セキュリティ階層は、２つの要素⊥及びΤから成る単純な格子を定義している。｜ｔ｜という表記は、ＴＡＬＣ＋のソース型の翻訳を表す。｜ｌｏｗ｜≡ｉｎｔ⊥及び｜ｈｉｇｈ｜≡ｉｎｔΤである。
【００７０】
[70]プログラムの翻訳は、├Ｈ０：Ψ０を満たしソースプログラムのすべての変数に対するエントリを含むヒープＨ０及びヒープ型Ψ０で開始する。Φ（ｖ）＝ｔである任意のソース変数ｖについては、Ψ（ｌｖ）＝＜｜ｔ｜＞⊥であるようなヒープ中のロケーションｌｖが存在する。この対応を、本明細書ではΦ〜Ψで表す。
【００７１】
[71]フォーム
【数５】
2010503921.tif 000007
の式翻訳を図１２に定義する。命令ベクトル
【数６】
2010503921.tif 000008
はＥの値を計算し、その結果がレジスタτに入力される。
【数７】
2010503921.tif 000009
を完了するのに必要な時間はｔである。
【００７２】
[72]図１３において、コマンド翻訳の定義は、ソースプログラムの型付け導出の構造に基づいている。どの翻訳規則を適用するかは、ソースコマンドのチェックに最後に使用した型付け規則によって決定される。型付け導出（場合によっては複数のこともある）はＴＤを使って表す。特に、一実施形態では、コマンド翻訳は以下の形式である。
【数８】
2010503921.tif 000010
【００７３】
[73]６つの引数は、コードヒープ型Ψ、コードヒープＨ、Ｃを計算するための開始ラベルｌｓｔａｒｔ及び終了ラベルｌｅｎｄ、終了ラベルｌｅｎｄにおけるコードのタイミング注釈ｔ、及びセキュリティコンテキストκである。それは、拡張されたコードヒープ型Ψ´及びコードヒープＨ´を生成し、開始ラベルｌｓｔａｒｔのタイミング注釈を生じさせる。
【００７４】
[74]コマンド翻訳の定義は、認証コンパイラの正式なモデルを提供するため、複雑に見える場合もある。しかし、それでも、いくつかの不変部分が翻訳によって維持されるので、定義に従うことは難しくはない。
・Ｈは、Ψのもとで十分に型付けされ、ソースのすべての変数及びプロシージャに対するエントリを含む。
・Ψ及びＨは、ｌｅｎｄとラベル付けされた継続コードをすでに含んでいる。
・ｌｅｎｄにおけるコードは、ｔによって反映されたタイミング挙動を有する。
・ｌｓｔａｒｔとラベル付けされた新たなコードがΨ´及びＨ´に入力される。
・生成された注釈ｔ´は、ｌｓｔａｒｔで開始するコードのタイミング挙動を反映する。
・セキュリティコンテキストκはｐｃと一致しなければならない。
【００７５】
タイミング注釈の操作
[75]∞を用いても機能するように、加算＋を予期された方法で拡張する。規則［ＴＲＣ１］では、開始ラベルのタイミング注釈ｔ´を計算する際に、ソースコマンドを計算するためのアセンブリ命令のコストを終了ラベルのタイミング注釈ｔの先頭に追加する。規則［ＴＲＣ２］では、セキュリティレベルが低のため、特別な注釈∞を使用する。規則［ＴＲＣ３］は、条件式については、「長い方の」分岐のタイミングを考慮しなければならないと指示している。規則［ＴＲＣ４］は、本質的に、何らかのラッパーコードを、したがってそのタイミングの計算を導入している。シーケンシャルコマンドについては、規則［ＴＲＣ５］が、２つのサブコマンドの翻訳をつなぎ合わせている。最後に、ｗｈｉｌｅループについては、規則［ＴＲＣ６］が、単に特別な注釈∞を使っている。
【００７６】
[76]その他の翻訳規則についてのさらなる情報については、Ｄ．Ｙｕ及びＮ．Ｉｓｌａｍ著の「Ａ  Ｔｙｐｅｄ  Ａｓｓｅｍｂｌｙ  Ｌａｎｇｕａｇｅ  ｆｏｒ  Ｃｏｎｆｉｄｅｎｔｉａｌｉｔｙ」（技術レポートＤＣＬ−ＴＲ−２００５−０００２、ＤｏＣｏＭｏ  Ｃｏｍｍｕｎｉｃａｔｉｏｎｓ  Ｌａｂｏｒａｔｏｒｉｅｓ  ＵＳＡカリフォルニア州サンホセ、２００５年３月、ｈｔｔｐ：／／ｗｗｗ．ｄｏｃｏｍｏｌａｂｓｒｅｓｅａｒｃｈｅｒｓ−ｕｓａ．ｃｏｍ／−ｄｙｕ／ｔａｌｃ−ｔｒ．ｐｄｆ．）を参照されたい。翻訳の正しさは、２つの補題として公式化されている。それらは、翻訳の導出についての構造帰納法によって簡単に証明され得る。
補題１（式の翻訳）
【数９】
2010503921.tif 000011
補題２（コマンドの翻訳）
【数１０】
2010503921.tif 000012
【００７７】
タイミングチャネル、可能的不干渉、及び確率的不干渉
[77]本発明の一実施形態は、終端チャネルが存在する場合の情報フローセキュリティに関するものである。以下に、タイミングチャネル、可能的不干渉、及び確率的不干渉に関する３つの他の実施形態を説明する。
【００７８】
タイミングチャネル
[78]タイミングチャネルを考えると、我々はマシンモデルを拡張して、実行時間ｔ及び出力アクションのｏｕｔｐｕｔ  ｎを明示的に指定し、プログラム実行のより正確なタイミング情報を観察できるようにする。
【００７９】
[79]
【数１１】
2010503921.tif 000013
の形式の、ＴＡＬＣの小ステップの状態遷移の先頭で、プログラム実行とともに生成されるアクションシーケンスが
【数１２】
2010503921.tif 000014
の形式で指定される。これは、Ｐが、観察可能なアクションシーケンスａｓを生成するＰ’に進むことを意味する。この場合、ａｓは、実行時間ｔによって分離された出力回数ｎを表す。
（アクションシーケンス）ａｓ：：＝ε｜ｔ  ａｓ  ｜ｎ  ａｓ
【００８０】
[80]操作意味論では、ａｓの値は現在の命令によって決定される。以下のサンプルケースについて考える。
【数１３】
2010503921.tif 000015
これは、即値オペランドωに対してｍｏｖ命令を実行する操作意味論上のケースである。通常のマシン状態の更新の他に、上記は、この命令を完了するために必要な時間ｔｍｏｖｉも指定する。本発明をわかりにくくすることを避けるため、この操作意味論の簡単な定義は省略し、命令ｃｏｍｍの実行時間を表すのにｔｃｏｍｍを使用している。原始的操作（すなわちアセンブリ命令）は、引数として与えられた値にかかわらず、一定の時間で実行すべきであることとする。これが、ｍｏｖ  γｄ，ω（すぐに移動）及びｍｏｖ  γｄ，γｓ（レジスタを移動）が異なる時間になることを妨げるものではないことに注意されたい。したがって、このステップ推移の反射的推移的閉鎖が拡張される。
【００８１】
[81]この拡張されたマシンモデルは、タイミングチャネルを通じて情報を漏洩させる。以下のソースレベルプログラムを例として挙げる。
Ｉｆ  ｈ  ｔｈｅｎ｛時間のかかるオペレーション｝ｅｌｓｅ  ｓｋｉｐ；
ｏｕｔｐｕｔ  ｎ
【００８２】
[82]ｈ≠０ならば、プログラムは観察可能なアクションシーケンスｔｌｏｎｇｎを生成する。この場合、ｔｌｏｎｇは「時間のかかるオペレーション」の実行時間である。ｈ＝０ならば、プログラムはｔｓｋｉｐｎを生成する。この場合、ｔｓｋｉｐはｓｋｉｐコマンドの実行時間である。これは、たとえそのプログラムにおいていかなる低データも更新されないとしても、情報の漏洩を引き起こす。
【００８３】
[83]前に説明したＴＡＬＣ＋のアプローチを使って、タイミングチャネルを通じたこのような情報の漏洩を説明することができる。高領域の終了まで実行ステップの上界を記録する代わりに、タイミング注釈を使って正確な観察可能アクションシーケンスａｓを記録することができる。高領域において低更新を許可しないのと同じ論法に基づいて、高領域では出力アクションが許可されない。本質的には、拡張されたタイミング注釈は実行時間を反映する。このような拡張されたシステムにおいては、分岐のための型付け規則は、２つの分岐のタイミング注釈が一致することをチェックすべきものである。
【００８４】
[84]図１４に、ＴＡＬＣ＋への正確な適用を示す。タイミング判定に異なる定義を与えることにより、タイミングチャネルを閉じるための型システムが得られ、図１０及び図１１の型付け規則は同じままである。図１４のタイミング規則は、正確なタイミングが追跡されるという考え方を反映している。非低コンテキストにおける時間経過
【数１４】
2010503921.tif 000016
については、ｔがｔ´とｔ´´の合計を正確に反映するようになっている。∞は、依然として、低コンテキストにおいてのみ許可される。最後に、タイミングθ├ｔ〜ｔ´のマッチングは、ｔ＝ｔ´として定義される。分岐が同じタイミング挙動を示すことを確認するために分岐命令の型チェックを行うときに、これが使用されたことを思い出されたい。図１５に例示のプログラム及び関連するタイミング注釈を示す。
【００８５】
[85]本明細書に記載の認証コンパイルスキームを、安全なソースプログラムをサポートするように改造することができる。安全なソースプログラムとは、例えば、「Ｔｒａｎｓｆｏｒｍｉｎｇ  Ｏｕｔ  Ｔｉｍｉｎｇ  Ｌｅａｋｓ」（Ｐｒｏｃ．２７ｔｈ  ＡＣＭ  Ｓｙｍｐｏｓｉｕｍ  ｏｎ  Ｐｒｉｎｃｉｐｌｅｓ  ｏｆ  Ｐｒｏｇｒａｍｍｉｎｇ  Ｌａｎｇｕａｇｅｓ、４０−５３ページ、マサチューセッツ州ボストン、２０００年１月）でＪ．Ａｇａｔによって提案されているクロスコピー変換によって生成されたものである。プログラムＰがクロスコピー変換によって受け付けられ、Ｐ´に変換されたならば、改造された認証コンパイルスキームが、Ｐ´を十分に型付けされたアセンブリコードに翻訳する。
【００８６】
[86]この改造については、たった１つの変更が規則［ＴＲＣ３］にある。その場合、「平衡分岐」がコンパイル後も平衡であることが保証される。１つの方法を規則［ＴＲＣ３´］として図１６に示す。変換されたソースプログラムでは、条件文の２つの分岐が平衡であることに注意されたい。したがって、規則［ＴＲＣ３´］は、ｔ１＝ｔ２であるコードを生成する。前の規則［ＴＲＣ３］では、ターゲットコードは平衡ではなく、「ｍａｘ」を使用して上界をとっている。さて、規則［ＴＲＣ３´］は、分岐がターゲットコードにおいても平衡であるように、ｌ´１とラベル付けされた余分のコードブロックを挿入する。
【００８７】
可能的不干渉
[87]一実施形態では、マルチスレッド設定における情報フローの問題を考察するのに、不干渉の表記を拡張してスレッドの非決定性実行を説明している。一実施形態では、プログラムの観察可能な挙動を一組の可能な実行結果とみなす簡単な一般化を使用している。
【００８８】
[88]スレッド間の相互作用を情報フローのチャネルとして悪用することができる。攻撃者がプログラムの外部タイミング挙動を観察することができないとしても、例えば、相互作用しているスレッドの実行順序に影響を与えることなどによって、いくつかの内部タイミング挙動が不正な情報フローにつながる可能性は依然としてある。
【００８９】
[89]図１７は、３スレッドの例示的プログラムを示す。ｆの値が初めは０であると仮定する。ｈが真（ｔｒｕｅ）である場合を考える。スレッド１は初めは「ロックされない」状態になる。スレッド２は、スレッド１の最後のステートメントの後で「ロックされない」状態になる。したがって、ｌの最終的な値は真（ｔｒｕｅ）になる。同様に、ｈが偽（ｆａｌｓｅ）であるならば、ｌの最終的な値は偽（ｆａｌｓｅ）になる。実質的に、上記のマルチスレッドプログラムは、ｈの内容をｌにコピーする。個々のスレッドの各々は、ｈ及びｆが高変数でありｌが低変数であるという前提のもとに、一般的なシーケンシャル情報フロー型システム（例えば、図１Ｂのもの）の下でうまく型付けされている。にもかかわらず、スレッドが一緒になると、高情報を漏洩する。
【００９０】
[90]一実施形態では、非決定性スレッドスケージューリングが存在する場合に可能的不干渉を保証するために、シーケンシャル設定において不干渉のために実行される要件に加えて、２つの要件を満たすよう、あらゆるスレッドがこの型システムにおいて別々にチェックされる。
１．ｗｈｉｌｅループの保護の型は低（ｌｏｗ）でなければならない。
２．ｗｈｉｌｅループ自体の型も低（ｌｏｗ）でなければならない。
【００９１】
[91]これらの２つの条件は、ソースレベルプログラムにおいて終端チャネルを閉じるための条件と同じである。本質的に、ループは低ＰＣにおいてのみ発生する（上記の規則［Ｃ６´］参照）。これは、上記のアセンブリコードのための技術を再使用できるため便利である。特に、高領域において後方へのジャンプが存在しないことが、単調減少するタイミング注釈で実行される。型チェックが各スレッドについて別々に行われるため、マルチスレッドの導入が上記の対処法に悪影響を及ぼすことはない。
【００９２】
確率的不干渉
[92]上記の不干渉の一般化は、一組の可能性ある実行結果を考慮している。これは、時折、実際にはある特定の悪用を防ぐのに十分なほど強力ではないことがある。例えば、可能性ある結果の確率分布が情報フローのチャネルとしての役割を果たす場合がある。
【００９３】
[93]図１８は、例示的プログラムを示す。ｈが高であり、ｌが低であり、Ｃｌｏｎｇが中間に多くの潜在的なコンテキストスイッチを有する長いステートメントシーケンスであるとする。このプログラムは、上記の可能的不干渉の分析では安全であるとみなされるであろう。しかし、多くのスケジューラの下では、おそらくｌの結果はｈと同じになるであろう。なぜならば、長い方の分岐を実行するスレッドは、おそらくもう一方のスレッドよりも遅く終わるからである。たとえｌの一組の可能性ある結果がｈの値にかかわらず同じであったとしても、可能性ある結果の確率分布は異なってくる。
【００９４】
[94]このような可能的攻撃は、プログラムの内部タイミング挙動を悪用する。したがって、一実施形態では、タイミングチャネルを閉じる技術を、外部タイミングに対処するものから内部タイミングに対処するものへと改造している。より具体的には、プログラム命令の外部実行時間を反映する代わりに、タイミング注釈は、潜在的なコンテキストスイッチの数−スレッドによって観察可能な「内部時間」を反映する。この内部時間は、潜在的なコンテキストスイッチがある度に１単位だけ進む。したがって、一実施形態では、タイミングに敏感な不干渉の分析がこれに応じて改造され、以下を実行している。
１．高領域における低割当てを許可しない。
２．高領域におけるｗｈｉｌｅループを許可しない。
３．２つの分岐が一致する内部タイミング注釈を有する場合にのみ高条件式を許可する。
【００９５】
[95]アトミックコマンド、スキップ命令、ダミーフォークを正しく実装するよう注意する限り、ＴＡＬＣ＋が安全なソースプログラムの認証コンパイルをサポートするのは当然である（例えば、Ｓａｂｅｌｆｅｌｄ及びＳａｎｄｓ著の「Ｐｒｏｂａｂｉｌｉｓｔｉｃ  Ｎｏｎｉｎｔｅｒｆｅｒｅｎｃｅ  ｆｏｒ  Ｍｕｌｔｉ−Ｔｈｒｅａｄ  Ｐｒｏｇｒａｍｓ」、Ｐｒｏｃ．１３ｔｈ  ＩＥＥＥ  Ｃｏｍｐｕｔｅｒ  Ｓｅｃｕｒｉｔｙ  Ｆｏｕｎｄａｔｉｏｎｓ  Ｗｏｒｋｓｈｏｐ、２００−２１４ページ、イギリスのケンブリッジ、２０００年７月）。
【００９６】
正当性
[96]セキュリティレベルθに関する２つのプログラムの同等性を定義する。直感的に言えば、２つのプログラム（ヒープファイル及びレジスタファイル）は、それらが低セキュリティの内容について一致する場合に且つその場合にのみ同等である。
定義１（ヒープの同等性）
【数１５】
2010503921.tif 000017
定義２（レジスタファイルの同等性）
【数１６】
2010503921.tif 000018
定義３（プログラムの同等性）
【数１７】
2010503921.tif 000019
【００９７】
[97]上記の関係は、反射的、対照的、且つ推移的である。不干渉の定理は、ともに（重要なキュリティレベルに対して）低セキュリティコンテキストで開始する２つの同等のプログラムの実行に関する。ＴＡＬＣでは、両方の実行が終了したならば、結果のプログラムは同等である。余分のタイミング注釈は、最も低いセキュリティレベルのコンテキストでのみ非終了が生じることを保証する。
【００９８】
[98]この証明の考え方は直感的である。重要なセキュリティレベルが与えられると、実行は「低ステップ」及び「高ステップ」に段階的に行われる。低ステップのもとで２つの実行を関連させることは容易である。なぜならば、それらは同じ命令を含むからである。高ステップのもとでは、２つの実行はもはやロックステップにはない。ｒａｉｓｅ及びｌｏｗｅｒが、安全に守られた領域の開始及び終了に印を付けることを思い出されたい。高ステップ下で２つの実行を直接関連付けることを避けながら、ｒａｉｓｅの前及びｌｏｗｅｒの後のプログラムの状態が関連付けられる。さらに、その安全に守られた領域では、非終了はまったく生じない。
【００９９】
[99]正式な詳細を、３つの補題及び不干渉の定理に記載する。補題３は、高ステップにおけるセキュリティコンテキストがｒａｉｓｅ又はｌｏｗｅｒを用いてのみ変更可能であることを示している。補題４は、高コンテキストにおけるプログラムが結局はｌｏｗｅｒで現在のセキュリティコンテキストを排出するステップに降格されることを述べている。補題５は、低ステップにおける２つの同等のプログラムの間のロックステップ関係をはっきり述べている。したがって、２つの同等のプログラムが与えられた場合、一方が終了すると、もう一方は最初のものと同等の状態で終了する、という不干渉の定理ｌが成立する。必然的に、一方が終了しないと、もう一方も終了しないと言える。
【０１００】
[100]以下において、
【数１８】
2010503921.tif 000020
は、操作意味論の単一ステップの関係
【数１９】
2010503921.tif 000021
の反射的且つ推移的な閉鎖を表す。
【数２０】
2010503921.tif 000022
は、Γ´（γ）＝τθ´及びθ´⊆θであるようなあらゆるγについて、Γ（γ）＝Γ´（γ）であることを意味する。２つの実行を比較する際のプログラムを表すために、Ｐに加えてＱという記号を使用する。
補題３（高ステップ）
【数２１】
2010503921.tif 000023
ならば、以下のいずれかである。
１．
【数２２】
2010503921.tif 000024
であるようなΓ１、ｔ１且つＰ１＝（Ｈ１，Ｒ１，Ｉ１）κが存在する、又は
２．Ｉは形態（ｒａｉｓｅ  κ´；Ｉ´）又は（ｌｏｗｅｒω）である。
証明の概略：Ｉの最初の命令についてのケース分析による。Ｉはｈａｌｔではない。なぜならば、ｈａｌｔの型付け規則は、コンテキストが・であることを要求するからである。操作意味論及び型付け規則の反転により、Ｉがｈａｌｔ、ｒａｉｓｅ又はｌｏｗｅｒでないならば、次のステップのためのΓ１、ｔ１及びＰ１を得ることができる。型付け規則中の時間経過判断により、ｔ１＜ｔが維持される。型付け規則はまた、低ヒープセル中への書き込みを禁じるので、低ヒープセルはそのステップの後も同じままである。レジスタが更新されると、Γ１は、それに対して、セキュリティラベルがＳＬ（κ）を考慮している型を与えるので、そのレジスタはΓ１に高い型を有する。その結果、
【数２３】
2010503921.tif 000025
である。
補題４（コンテキストの排出）
【数２４】
2010503921.tif 000026
ならば、
【数２５】
2010503921.tif 000027
であるような
【数２６】
2010503921.tif 000028
が存在する。
証明の概略：ｔに対する一般化された帰納法による。
【０１０１】
[101]ｔ＝０という基本ケースが容易に排出される。なぜならば、θ≠⊥であるＰの十分な型付けの反転によって、ｔ＞０を暗に意味する時間経過判断が得られるからである。
【０１０２】
[102]帰納的なケースの場合、任意のｔ＜ｔ０についてその命題が有効であると仮定する。補題３に従い、考えるべき２つのケースがある
【０１０３】
[103]Ｉの最初の命令がｒａｉｓｅでもｌｏｗｅｒでもない場合、補題３により、
【数２７】
2010503921.tif 000029
であるようなΓ１、ｔ１及びＰ１が存在し、Ｐ１のセキュリティコンテキストはＰのセキュリティコンテキストと同じである。ｔ１及びＰ１についての帰納法の仮定によって、
【数２８】
2010503921.tif 000030
であるようなΓ´、ｔ´及びＰ´が存在する。上記を合わせると、
【数２９】
2010503921.tif 000031
になる。なぜならば、
【数３０】
2010503921.tif 000032
は定義により推移的であり、ｔ´≦ｔであり、且つ定義及び
【数３１】
2010503921.tif 000033
という事実によりΨ；Ｉ´├Ｐ≒θ´Ｐ´だからである。
【０１０４】
[104]
【数３２】
2010503921.tif 000034
というケース。操作意味論の定義により、
【数３３】
2010503921.tif 000035
。この場合
【数３４】
2010503921.tif 000036
である。Ψ；Γ；ｔ├Ｐの反転、及びｒａｉｓｅの型付け規則によりθ⊆θ１であり、
【数３５】
2010503921.tif 000037
であるようなｔ１＜ｔが存在する。十分に型付けされたプログラムの定義により、Ψ；Γ；ｔ１├Ｐ１である。ｔ１及びＰ１についての帰納法の仮定により、
【数３６】
2010503921.tif 000038
であるようなΓ２、ｔ２、及び
【数３７】
2010503921.tif 000039
が存在する。したがって、Ψ；Γ２├Ｐ≒θ´Ｐ２が成立する。なぜならば、Ｐ及びＰ１におけるヒープレジスタ及びレジスタファイルは同じだからである。
【０１０５】
[105]Ｈ（ω１）＝ｃｏｄｅ［］（κ；ｔ３）Γ３．Ｉ３と仮定する。ｌｏｗｅｒ（Ｐ２の現在の命令）の型付け規則の反転により、ｔ３＜ｔ２である。操作意味論により、
【数３８】
2010503921.tif 000040
。この場合Ｐ３＝（Ｈ２，Ｒ２，Ｉ３）κ。Ｉの十分な型付けの反転により（すなわち、
【数３９】
2010503921.tif 000041
）、
【数４０】
2010503921.tif 000042
である。ｔ３及びＰ３についての帰納法の仮定により、
【数４１】
2010503921.tif 000043
であるような、Γ´、ｔ´及び
【数４２】
2010503921.tif 000044
が存在する。上記を合わせると、
【数４３】
2010503921.tif 000045
のケースについて、元の命題が有効である。
【０１０６】
[106]Ｉ＝ｌｏｗｅｒ  ω１のケース。ｌｏｗｅｒの型付け規則の反転により、ω＝ω１が得られる。Γ´＝Γ´、ｔ´＝ｔ及びＰ´＝Ｐを選択することにより、この命題が自明に有効である。
補題５（低ステップ）
Ｐ＝（Ｈ，Ｒ，Ｉ）κ、ＳＬ（κ）⊆θ、Ψ；Γ；ｔ├Ｐ、Ψ；Γ；ｔ├Ｑ、Ψ；Γ├Ｐ≒θＱ、
【数４４】
2010503921.tif 000046
ならば、Ψ；Γ１；ｔ１├Ｐ１、Ψ；Γ１；ｔ１├Ｑ１、且つΨ；Γ１├Ｐ１≒θＱ１であるようなΓ１及びｔ１が存在する。
証明の概略：Ｉの最初の命令についてのケース分析。ＳＬ（κ）⊆θ、及び≒θの定義により、Ｐ及びＱは同じ命令シーケンスを含む。ｒａｉｓｅのケースは状態を変えないので、自明に同等性を維持する。その他のケースはすべて、セキュリティコンテキストがθよりも低であることを維持する。型付け規則の検査は、ヒープ中の低ロケーションには低い値しか割当てられないことを示している。いったんレジスタに高い値が与えられるとΓ１中のその型は高に変わる。分岐を行う場合、ガードは低でなければならず、したがってＰ及びＱの両方が同じコードに分岐する。したがって、２つのプログラムは１ステップ後も同等のままである。
定理１（不干渉）
Ｐ＝（Ｈ，Ｒ，Ｉ）κ、ＳＬ（κ）⊆θ、Ψ；Γ；ｔ├Ｐ、Ψ；Γ；ｔ├Ｑ、Ψ；Γ├Ｐ≒θＱ、且つ
【数４５】
2010503921.tif 000047
ならば、
【数４６】
2010503921.tif 000048
且つΨ；Γ´├（Ｈｐ，Ｒｐ，ｈａｌｔ｜σＰ｜）・≒θ（Ｈｑ，Ｒｑ，ｈａｌｔ｜σＱ｜）・であるようなＨｑ、Ｒｑ、σｑ及びΓ´が存在する。
証明の概略：導出
【数４７】
2010503921.tif 000049
のステップ数の一般化された帰納法による。ゼロステップの基本ケースは自明である。帰納的なケースは、Ｉの第１の命令のケース分析により証明される。
【０１０７】
[107]
【数４８】
2010503921.tif 000050
であるケースについて考える。操作意味論の定義及び型付け規則により、
【数４９】
2010503921.tif 000051
であるようなｔ１が存在する。この場合、
【数５０】
2010503921.tif 000052
である。補題４により、
【数５１】
2010503921.tif 000053
であるようなΓ２、ｔ２及び
【数５２】
2010503921.tif 000054
が存在する。したがって、Ψ├Ｈ≒θＨ２且つΓ２├Ｒ≒θＲ２である。
【０１０８】
[108]操作意味論のｌｏｗｅｒであるケースにより、
【数５３】
2010503921.tif 000055
である。この場合、Ｐ３＝（Ｈ２，Ｒ２，Ｉ３）κ３且つＨ（ω１）＝ｃｏｄｅ［］（κ３；ｔ３）Γ３．Ｉ３である。Ψ：Γ２；ｔ２├Ｐ２の導出の反転により、Γ３⊆Γ２、ｔ３＋１≦ｔ２、Ψ；Γ３；ｔ３├Ｐ３である。Γ３├Ｒ≒θＲ２が成立する。Ｐの命令シーケンスが
【数５４】
2010503921.tif 000056
である場合の、Ψ；Γ；ｔ├Ｐの導出の反転により、κ３＝κが得られる。
【０１０９】
[109]同様の推理により、
【数５５】
2010503921.tif 000057
。この場合、Ｑ３＝（Ｈ´２，Ｒ´２，Ｉ３）κ３、Ψ├Ｈ≒θＨ´２、Γ３├Ｒ≒θＲ´２、且つΨ；Γ３；ｔ３├Ｑ３。同等関係の推移性により、Ψ├Ｈ２≒θＨ´２、且つΓ３├Ｒ２≒θＲ´２。したがって、Ψ；Γ├Ｐ３≒θＱ３。よって、このケースが帰納法の仮定により成立する。
【０１１０】
[110]１ステップの後、その他のケースはすべて低のままである。補題５により、次のステップにおける２つのプログラムは同等であり十分に型付けされている。したがって、これらのケースの証明は、帰納法の仮定により成立する。
【０１１１】
コンピュータシステムの例
[111]図１９は、本明細書に記載のオペレーションの１つ又は複数を実行することができる例示的コンピュータシステムのブロック図である。図１９を参照すると、コンピュータシステム１９００は例示的なクライアント又はサーバコンピュータシステムを含む。コンピュータシステム１９００は、情報を伝達するための通信メカニズム又はバス１９１１と、及び情報を処理するための、バス１９１１と接続されたプロセッサ１９１２とを備える。プロセッサ１９１２はマイクロプロセッサを含むが、例えば、Ｐｅｎｔｉｕｍ（商標）、ＰｏｗｅｒＰＣ（商標）、Ａｌｐｈａ（商標）などのマイクロプロセッサに限定されるものではない。
【０１１２】
[112]システム１９００は、ランダムアクセスメモリ（ＲＡＭ）、又は、バス１９１１に接続された、情報及びプロセッサ１９１２が実行するための命令を記憶するためのその他のダイナミック記憶デバイス１９０４（メインメモリと呼ぶ）をさらに備える。また、メインメモリ１９０４は、プロセッサ１９１２が命令を実行している間に、一時的変数やその他の中間情報を記憶するために使用することもできる。
【０１１３】
[113]また、コンピュータシステム１９００は、読み取り専用メモリ（ＲＯＭ）、及び／又は、バス１９１１に接続された、プロセッサ１９１２のための静的情報及び命令を記憶するためのその他の静的記憶デバイス１９０６と、磁気ディスクや光ディスク及びそれに対応するディスクドライブなどのデータ記憶デバイス１９０７とを備える。データ記憶デバイス１９０７は、情報及び命令を記憶するためにバス１９１１に接続されている。
【０１１４】
[114]システム１９００はさらに、コンピュータユーザに情報を表示するためにバス１９１１に接続された、陰極線管（ＣＲＴ）や液晶ディスプレイ（ＬＣＤ）などのディスプレイデバイス１９２１に接続することもできる。情報やコマンドの選択をプロセッサ１９１２に伝達するために、英数字及びその他のキーを含む英数字入力デバイス１９２２もバス１９１１に接続することができる。さらなるユーザ入力デバイスは、方向情報やコマンドの選択をプロセッサ１９１２に伝達したりディスプレイ１９２１上のカーソルの動きを制御するためにバス１９１１に接続された、マウス、トラックボール、トラックパッド、タッチペン、カーソル方向キーなどのカーソル制御装置１９２３である。
【０１１５】
[115]バス１９１１に接続することができる別のデバイスとして、紙やフィルムなどの媒体、又は同様の種類の媒体の上に情報をマーキングするために使用できるハードコピーデバイス１９２４がある。バス１９１１に接続することができる別のデバイスとして、電話やハンドヘルドパームデバイスへの通信を行うための有線／無線通信機能１９２５がある。
【０１１６】
[116]システム１９００の構成要素のいずれか又はすべてと関連ハードウェアとを本発明において使用できることに注意されたい。しかし、当然ながら、このコンピュータシステムの他の構成が、それらのデバイスのいくつか又はすべてを含むことができる。
【０１１７】
[117]当業者は、これまでの説明を読めば、本発明の多くの変更及び修正が疑いもなく明らかになろう。しかし、例示の目的で示し、説明した特定の実施形態のいずれも、限定するものとしてみなすことを意図したものでは決してないことを理解されたい。したがって、様々な実施形態の詳細を述べたことは、本発明に不可欠とみなされる特徴のみが記載されている特許請求の範囲を限定することを意図していない。
【図面の簡単な説明】
【０１１８】
【図１Ａ】命令型言語の例を説明する図である。
【図１Ｂ】単純なセキュリティ型システムを説明する図である。
【図２】ＴＡＬＣの簡略版の構文を説明する図である。
【図３】セキュリティ型付けされたソースプログラムから翻訳されたターゲットコードであるＴＡＬＣプログラムの例を説明する図である。
【図４Ａ】情報フロー実行のためのプロセスの流れ図である。
【図４Ｂ】図４Ａの情報フロー実行を実装することができる環境を説明する図である。
【図５】条件文のタイミング注釈の一実施形態を説明する図である。
【図６】ループのタイミング型注釈の一実施形態を説明する図である。
【図７】ＴＡＬＣ＋の構文拡張の一実施形態を説明する図である。
【図８】ＴＡＬＣ＋の型付け判断の一実施形態を説明する図である。
【図９】終端チャネルを閉じるためのタイミング規則の一実施形態を説明する図である。
【図１０】非命令のためのＴＡＬＣ＋の型付け規則の一実施形態を説明する図である。
【図１１】命令のためのＴＡＬＣ＋の型付け規則の一実施形態を説明する図である。
【図１２】式の解釈の一実施形態を説明する図である。
【図１３】コマンドの解釈の一実施形態を説明する図である。
【図１４】タイミングチャネルを閉じるためのタイミング規則の一実施形態を説明する図である。
【図１５】条件文の拡張されたタイミング注釈の一実施形態を説明する図である。
【図１６】タイミングチャネルが存在する場合の条件式の解釈を説明する図である。
【図１７】可能的不干渉の例を説明する図である。
【図１８】確率的不干渉の例を説明する図である。
【図１９】コンピュータシステムの一実施形態のブロック図である。
【図１Ａ】
2010503921.tif 000058
【図１Ｂ】
2010503921.tif 000059
【図２】
2010503921.tif 000060
【図３】
2010503921.tif 000061
【図４Ａ】
2010503921.tif 000062
【図４Ｂ】
2010503921.tif 000063
【図５】
2010503921.tif 000064
【図６】
2010503921.tif 000065
【図７】
2010503921.tif 000066
【図８】
2010503921.tif 000067
【図９】
2010503921.tif 000068
【図１０】
2010503921.tif 000069
【図１１】
2010503921.tif 000070
【図１２】
2010503921.tif 000071
【図１３】
2010503921.tif 000072
【図１４】
2010503921.tif 000073
【図１５】
2010503921.tif 000074
【図１６】
2010503921.tif 000075
【図１７】
2010503921.tif 000076
【図１８】
2010503921.tif 000077
【図１９】
2010503921.tif 000078
【手続補正書】
【提出日】平成21年3月18日(2009.3.18)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報を備えたタイミング注釈を有するアセンブリコードを受信するステップと、
セキュリティポリシーに基づいて、前記アセンブリコードについて情報フローに関する検証を行うステップと
を含む方法。
【請求項２】
並列チャネルがマルチスレッドに関連付けられている、請求項１に記載の方法。
【請求項３】
前記タイミング関連の秘密チャネルが、１つ又は複数の終端チャネル、タイミングチャネル、可能的チャネル、及び確率的チャネルを含む請求項１に記載の方法。
【請求項４】
前記タイミング注釈がソースレベルの制約を表現している、請求項１に記載の方法。
【請求項５】
前記タイミング注釈が、コマンドが実行されるのに必要な時間の量を表す時間値を特定する第１の注釈と、コマンドに関連付けられたタイミングが指定期間の後に変更可能であることを特定する第２の注釈と、特定のセキュリティレベルの下でコマンドが実行されるための許容できるタイミングを特定する第３の注釈と、コマンドに関連付けられた前記タイミングが特定のセキュリティレベルの下で時間の経過に一致することを特定する第４の注釈とから成るグループを１つ又は複数含む、請求項１に記載の方法。
【請求項６】
前記タイミング注釈が、前記アセンブリコードの一部の実行に関連付けられたタイミング情報の観察を可能にするために、観察可能アクションシーケンスに関連付けられた実行時間を表す、請求項１に記載の方法。
【請求項７】
前記タイミング注釈が、分岐命令の両分岐が同じタイミング挙動を示すことを明らかにするためのチェックを行うことを可能にする、請求項１に記載の方法。
【請求項８】
前記分岐命令の両分岐が、特定のセキュリティレベルで識別された前記コードの終了において同じ時間量で合流したときに同じタイミング挙動を示す、請求項７に記載の方法。
【請求項９】
前記タイミング注釈が、第１のセキュリティレベルよりも高い第２のセキュリティレベルを有する前記コードの領域においては、前記第１のセキュリティレベルの変数については出力も更新も一切発生しないことを保証するためのチェックを可能にする、請求項１に記載の方法。
【請求項１０】
前記コードから前記注釈を除去するステップと、
前記検証を行うステップにおいて前記コードが前記セキュリティポリシーに違反していないと判断された場合に前記コードを実行するステップと、
を含む請求項１に記載の方法。
【請求項１１】
デバイスが前記コードを実行する前に、前記検証を行なうステップが該デバイスにおいて実行される、請求項１に記載の方法。
【請求項１２】
前記検証を行うステップが、前記コードが前記セキュリティポリシーに違反していないかどうかを判断するために該コードの挙動を静的にチェックするステップを含む、請求項１に記載の方法。
【請求項１３】
前記コードが、実行されたときに、識別された型の情報を該コードを実行しているデバイスから流出させなかったならば、該コードは前記セキュリティポリシーに違反していない、請求項１２に記載の方法。
【請求項１４】
前記検証を行うステップにおいて前記コードが前記セキュリティポリシーに違反していないと判断された場合に前記コードを実行するステップをさらに含む請求項１に記載の方法。
【請求項１５】
前記コードを受信するステップが前記コードをダウンロードするステップを含む、請求項１に記載の方法。
【請求項１６】
安全に型付けされたネイティブコードを受信するステップが、前記アセンブリコードを型情報で注釈付けすることを含むセキュリティ型維持翻訳を施されたアセンブリコードを受信するステップを含み、さらに、前記検証を行うステップが、安全ポリシーに関して、実行されたときの前記アセンブリコードの制御の下で生じる情報フローを静的にチェックすることによって前記型情報を検証するステップを含む、請求項１に記載の方法。
【請求項１７】
システムによって実行されると前記システムに方法を実行させる命令を記憶している１つ又は複数の記録可能媒体を有する製品であって、
前記方法が、
コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報を備えたタイミング注釈を有するアセンブリコードを受信するステップと、
セキュリティポリシーに基づいて、前記アセンブリコードについて情報フローに関する検証を行うステップと
を含む製品。
【請求項１８】
前記タイミング注釈がソースレベルの制約を表現している、請求項１７に記載の製品。
【請求項１９】
前記タイミング注釈が、コマンドが実行されるのに必要な時間の量を表す時間値を特定する第１の注釈と、コマンドに関連付けられたタイミングが指定期間の後に変更可能であることを特定する第２の注釈と、特定のセキュリティレベルの下でコマンドが実行されるための許容できるタイミングを特定する第３の注釈と、コマンドに関連付けられた前記タイミングが特定のセキュリティレベルの下で時間の経過に一致することを指定する第４の注釈とから成るグループを１つ又は複数含む、請求項１７に記載の製品。
【請求項２０】
前記タイミング注釈が、前記アセンブリコードの一部の実行に関連付けられたタイミング情報の観察を可能にするために、観察可能アクションシーケンスに関連付けられた実行時間を表す、請求項１７に記載の製品。
【請求項２１】
前記タイミング注釈が、分岐命令の両分岐が同じタイミング挙動を示すことを明らかにするためのチェックを行うことを可能にする、請求項１７に記載の製品。
【請求項２２】
前記分岐命令の両分岐が、特定のセキュリティレベルで識別された前記コードの終了において同じ時間量で合流したときに同じタイミング挙動を示す、請求項２１に記載の製品。
【請求項２３】
前記タイミング注釈が、第１のセキュリティレベルよりも高い第２のセキュリティレベルを有する前記コードの領域においては、前記第１のセキュリティレベルの変数については出力も更新も一切発生しないことを保証するためのチェックを可能にする、請求項１７に記載の製品。
【請求項２４】
注釈付きアセンブリコード、検証モジュール、コード修正モジュールを記憶するメモリであって、前記注釈付きアセンブリコードが、コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報を備えたタイミング注釈を有する、メモリと、
前記検証モジュールを実行して、セキュリティポリシーに基づいて前記注釈付きコードの情報フローに関する検証を行うプロセッサと
を備える装置。
【請求項２５】
前記タイミング注釈が、コマンドが実行されるのに必要な時間の量を表す時間値を特定する第１の注釈と、コマンドに関連付けられたタイミングが指定期間の後に変更可能であることを特定する第２の注釈と、特定のセキュリティレベルのもとでコマンドが実行されるための許容できるタイミングを特定する第３の注釈と、コマンドに関連付けられた前記タイミングが特定のセキュリティレベルのもとで時間の経過に一致することを特定する第４の注釈とから成るグループを１つ又は複数含む、請求項２４に記載の装置。
【請求項２６】
前記タイミング注釈が、前記アセンブリコードの一部の実行に関連付けられたタイミング情報の観察を可能にするために、観察可能アクションシーケンスに関連付けられた実行時間を表す請求項２４に記載の装置。
【請求項２７】
前記タイミング注釈が、分岐命令の両分岐が同じタイミング挙動を示すことを明らかにするためのチェックを行うことを可能にする、請求項２４に記載の装置。
【請求項２８】
前記分岐命令の両分岐が、特定のセキュリティレベルで識別された前記コードの終了において同じ時間量で合流したときに同じタイミング挙動を示す、請求項２７に記載の装置。
【請求項２９】
前記タイミング注釈が、第１のセキュリティレベルよりも高い第２のセキュリティレベルを有する前記コードの領域においては、前記第１のセキュリティレベルの変数については出力も更新も一切発生しないことを保証するためのチェックを可能にする、請求項２４に記載の装置。
【請求項３０】
前記プロセッサが、前記コードが、識別された型の情報を前記コードを実行しているデバイスから流出させることによって前記セキュリティポリシーに違反していないかどうかを判断するために、前記コードの挙動を静的にチェックすることによって検証を行う、請求項２４に記載の装置。
【請求項３１】
無線通信の送受信を行うための無線通信ハードウェア及び無線通信ソフトウェアをさらに備える請求項２４に記載の装置。
【請求項３２】
アセンブリコードに対してセキュリティ型維持翻訳を行うステップであって、コードがセキュリティポリシーに違反しているかどうかについて静的にチェックがなされる際に、１つ又は複数のタイミング関連の秘密チャネル及び並列チャネルに関して情報フローを実行する型情報を備えたタイミング注釈を用いて前記コードに注釈付けを行うことを含む、ステップと、
前記アセンブリコードが実行された結果である情報フローのコンパイルを証明するステップと、
前記安全に型付けされたアセンブリコードがネットワークを介してダウンロードされることを可能にするステップと
を含む方法。
【国際調査報告】
2010503921.tif 000079
2010503921.tif 000080
2010503921.tif 000081