(57)【要約】  情報フローの強制を実行する方法、製造品、及び装置が開示される。一実施形態において、方法は、セキュアに型付けされたネイティブコードを受け取り、セキュアに型付けされたネイティブコードに対して、セキュリティポリシーに基づいて情報フローに関する検証を実行することを含む。【選択図】  図１Ａ
2008524726.tif 000002
【特許請求の範囲】
【請求項１】
セキュアに型付けされたネイティブコードを受け取る受け取りステップと、
セキュリティポリシーに基づいて、前記セキュアに型付けされたネイティブコードに対して情報フローに関する検証を実行するステップと、
を備える、方法。
【請求項２】
システムによって実行されるときに前記システムに方法を実行させる命令を記憶した１つ以上の記録可能な媒体を有する製造品であって、
前記方法が、
セキュアに型付けされたネイティブコードを受け取る受け取りステップと、
セキュリティポリシーに基づいて、前記セキュアに型付けされたネイティブコードに対して情報フローに関する検証を実行する検証ステップと、
を備える、製造品。
【請求項３】
注釈されたアセンブリコード、検証モジュール及びコード修正モジュールを記憶するメモリと、
前記検証モジュールを実行し、セキュリティポリシーに基づいて、前記注釈されたコードに対して情報フローに関する検証を実行するプロセッサと、
を備える装置。
【請求項４】
アセンブリコード上でセキュリティ型保存変換を実行するステップであって、
メモリ、スタック、及びレジスタの内容にセキュリティレベルによって注釈する工程と、
機密情報に基づく２つの実行経路が出会う前記アセンブリコードのセキュリティ領域の始まり及び終わりをマークする演算を前記アセンブリコードに付加することによって、注釈を有する前記アセンブリコードのソースレベル構造を再構築する工程と、
を含むステップと、
実行されたときの前記アセンブリコードから生じる情報フローについてコンパイルを認証するステップと、
前記セキュアに型付けされたアセンブリコードをネットワークへ送るステップと、
を備える方法。
【発明の詳細な説明】
【優先権】
【０００１】
[0001]本願は、対応する仮特許出願第６０／６３８，２９８号、即ち、２００４年１２月２１日に出願され、発明の名称が「Ｉｎｆｏｒｍａｔｉｏｎ  Ｆｌｏｗ  Ｅｎｆｏｒｃｅｍｅｎｔ  ｆｏｒ  ＲＩＳＣ−Ｓｔｙｌｅ  Ａｓｓｅｍｂｌｙ  Ｃｏｄｅ」である出願の優先権を主張し、参照することによりそれを組み込んだ。
【０００２】
[0002]本発明は、プログラム実行及びセキュリティの分野に関する。より詳細には、本発明はアセンブリコード上で情報フローの制約を強制することに関する。
【０００３】
[0003]従来のセキュリティメカニズムは、情報フローのポリシーを強制することにおいて不十分であることが周知である。近年、プログラミング言語の理論及び実装に基づく手法を使用して、機密扱いデータの機密を保護することに多くの努力が重ねられて来た。これらの手法は、目標システムの内部の情報フローを解析し、多くの従来のセキュリティメカニズムの欠点を克服する潜在力を有する。残念ながら、情報フローに関する大量の言語ベース研究は、依然としてアセンブリコード又は機械実行可能コードの問題を直接取り上げていない。そこでの困難な問題は、高レベルの抽象化（例えば、プログラム構造及びデータ構造）の欠乏に取り組むこと、及びアセンブリコードによって提供される極端な柔軟性（例えば、メモリ再命名及び第１級コード・ポインタ）を管理することに大きく存在する。
【０００４】
[0004]しかしながら、低レベルで不干渉を直接強制することが望ましい。一方では、高レベル・プログラムが実計算機で実行可能になる前に、それらのプログラムは低レベルコードへコンパイルされなければならない。コンパイル又は最適化のバグは、ソースプログラムについて確立されたセキュリティの保証を無効にするかも知れず、可能性として悪意の第三者によって利用されるかも知れない。他方では、幾つかのアプリケーションがアセンブリコードで配布され（例えば、移動計算のバイトコード又はネイティブコード）、直接に書かれる（例えば、組み込みシステム、核心的システム・ライブラリ）。したがって、或る場合には、低レベルでの強制を行わなければならない。
【０００５】
[0005]ネットワーク情報システムへの依存性が大きくなるにつれて、機密データの保護が益々重要になっている。機密扱いデータを取り扱うと共に公開情報通信路へのアクセスを必要とする計算システムにおいて、問題は特に複雑である。機密扱いデータ又は公開通信路（又は、これらの組み合わせ）へのアクセスを制限する簡単なポリシーは、多くの場合、あまりに制限的であることを証明する。より望ましいポリシーは、機密扱いデータに関する情報が公開通信路の観察からは推論できないことである。計算システムが双方へのアクセスを許可されるとしてもそうである。情報フローのそのような規制は、多くの場合、情報フローと呼ばれ、機密扱いデータが公開データに影響を与えないポリシーは、多くの場合、非干渉と呼ばれる。
【０００６】
[0006]機密扱いデータを直接公表する単純な違反を検出及び防止するのは比較的容易であるが、複雑にコード化された情報をアプリケーションが送り出すことを防止するのは、はるかに困難である。従来のセキュリティメカニズム、例えば、アクセス制御、ファイヤウォール、暗号化、及びアンチ・ウィルスは、非干渉ポリシーを強制することにおいて完全でない。一方では、非干渉は、従来のメカニズムには一見して矛盾する要件を掲示する。即ち、それは機密扱い情報の使用を許すが、そのフローを制限する。他方では、非干渉の違反は、プログラムの単一の実行を監視することから観察できないが、そのような実行監視は多くの従来のメカニズムの基礎として役立つ。
【０００７】
[0007]情報フローの問題は、異なるセキュリティレベル、例えば、低及び高レベルのデータに作用するプログラムとして抽象化可能である。セキュリティレベルが「低」のデータ（低いセキュリティを表す、以下、低データとも記載する）は公開データであり、このことは全ての原理によって観察可能である。セキュリティレベルが「高」のデータ（高いセキュリティを表す、以下、高データとも記載する）は、制限されたアクセスを有する機密データである。情報フローのポリシーは、高（機密）入力に関する情報が、低（公開）出力を観察することから推論不可能であることを要求する。一般的に、セキュリティレベルは格子へ一般化可能である。
【０００８】
[0008]そのような情報フローのポリシーは、目標システムの内部における情報フローの追跡に関わっている。明瞭なフローを検出することは容易であるが（例えば、ｌ＝ｈにより機密ｈから公開ｌへの代入を介して）、暗黙的フローの様々な形式を検出することは、はるかに困難である。例えば、命令文ｌ＝０；ｉｆ  ｈ  ｔｈｅｎ  ｌ＝１は、ｈからｌへの情報の暗黙的フローを含む。実行時には、ｔｈｅｎ分岐が取られなければ、実行の監視に基づく従来のセキュリティメカニズムは違反を検出しないであろう。しかし、ｈに関する情報は、実にｌの結果から推論可能である。なぜなら、ｌが０のままである事実は、ｈの値も０でなければならないことを示すからである。
【０００９】
[0009]単一の実行を観察する代わりに、言語ベースの手法は、プログラムコードを検討し、また可能性として編成することによって、プログラムの振る舞いに関する保証を引き出す。上記の例において、情報は、本質的に、プログラム・カウンタ（本明細書では、ｐｃと呼ばれる）を介して漏洩する。即ち、分岐が取られる事実は、条件文の保護に関する情報を反映する。これに応答して、セキュリティ型システムは、典型的には、セキュリティラベルでプログラム・カウンタをタグ付けする。条件文の保護が高データに関わっているならば、分岐は、高いセキュリティラベルを有するプログラム・カウンタのもとで検証される。更に、高いプログラム・カウンタのもとでは、低い変数への代入は許されず、これは上記の形式の暗黙的フローを防止する。
【００１０】
（従来のメカニズム）
[0010]多くの従来のセキュリティメカニズムは、実行監視（ＥＭ）に基づいている。幾つかの代表的な例は、セキュリティカーネル、参照モニタ、アクセス制御、及びファイヤウォールを含む。これらのメカニズムは、目標システムの実行を監視し、セキュリティポリシーへの潜在的違反を探索することによってセキュリティを強制する。残念ながら、そのようなＥＭは、「安全特性」を強制できるだけである。情報フローのポリシーは「特性」ではなく（実行がポリシーを満足させるかどうかは、他の可能な実行に依存する）、したがってＥＭによって強制され得ない。
【００１１】
[0011]暗号プロトコルは、証明されない複雑性理論の仮定に依存する。これらの仮定の幾つかは誤っていることが示された（例えば、ＤＥＳ、ＳＨＡ０、ＭＤ５）。強力な暗号の商業的使用も、政治的及び法律的複雑性の中で混乱させられる。おそらく、更に重要なこととして、暗号は通信路のセキュリティを確保するだけで、コードが或るソースから来ることだけを確立する。それは単独でアプリケーションの安全性を確立することはできない。
【００１２】
[0012]アンチ・ウィルスは、他の広く適用されるアプローチである。その限界は周知である。即ち、それは常にウィルスよりも一歩遅れていることである。なぜなら、それはウィルスコードの中の或るパターンの検出に基づいているからである。
【００１３】
（強制的アクセス制御）
[0013]強制的アクセス制御は、Ｆｅｎｔｏｎ、Ｂｅｌｌ、及びＬａＰａｄｕｌａによって開発された実行時強制メカニズムであって、安全システムについて米国国防省の「オレンジ・ブック」によって規定されている。このアプローチにおいて、簡単なセキュリティポリシーがセキュリティラベルを使用してコード化される。データ項目及びプログラム実行は、これらのラベルでタグ付けされる。情報フローは、これらのラベルに基づいて管理され、これらのラベルは実行時に操作及び計算される。
【００１４】
[0014]強制的アクセス制御の明らかな弱点は、セキュリティラベルを計算及び記憶するため計算及び記憶装置のオーバーヘッドを生じることである。おそらく、より重要なことは、強制がプログラム実行時における実行を観察することに基づいていることである。前述したように、そのような実行時の強制は、プログラムの全ての可能な実行経路に関わる暗黙的フローを効果的に検出することができない。
【００１５】
[0015]暗黙的フローの存在で機密性を取得するため、機密扱いラベルを使用するプロセスが導入される。プログラムの実行が、機密データに基づいて異なる経路へ分かれるならば、プロセス機密扱いラベルが増加される。ラベルを単調に増加するこの効果は、ラベル・クリープとして公知である。それは、強制的アクセス制御の一般的な使用を非常に制限的なものにする。なぜなら、ラベル計算の結果は、データの意図された使用のためには、あまりに機密扱いになる傾向があるからである。
【００１６】
（言語ベースのアプローチ）
[0016]情報フローへ言語ベースの手法を適用するため多くの努力が行われたが、それらの大部分は高レベル言語に焦点を当てた。関数、例外、オブジェクト、及び並行性を含む多くの高レベル抽象化が公式的に研究され、実用的な実装が実行された。しかし、高レベルだけで情報フローを強制することは、コンパイラを信頼性計算ベース（ＴＣＢ）の中へ置く。更に、低レベルコードで配布又は書かれたソフトウェアの検証を見過ごすことはできない。
【００１７】
[0017]Ｂａｒｔｈｅらは、Ｓｅｃｕｒｉｔｙ  ｔｙｐｅｓ  ｐｒｅｓｅｒｖｉｎｇ  ｃｏｍｐｉｌａｔｉｏｎ，  Ｐｒｏｃ．  ５ｔｈ  Ｉｎｔｅｒｎａｔｉｏｎａｌ  Ｃｏｎｆｅｒｅｎｃｅ  ｏｎ  Ｖｅｒｉｆｉｃａｔｉｏｎ，  Ｍｏｄｅｌ  Ｃｈｅｃｋｉｎｇ  ａｎｄ  Ａｂｓｔｒａｃｔ  Ｉｎｔｅｒｐｒｅｔａｔｉｏｎ，  ｖｏｌｕｍｅ  ２９３７  ｏｆ  ＬＮＣＳ，  ｐａｇｅｓ  ２−１５．  Ｓｐｒｉｎｇｅｒ−Ｖｅｒｌａｇ，  Ｊａｎ．  ２００４  において、バイトコード言語及び変換用のセキュリティ型システムを呈示するが、このシステムはセキュリティ型を保存する。この参照文献はスタック・ベースの言語を開示する。更に重要なことに、Ｂａｒｔｈｅらの検証は、条件文について依存領域及びポストドミネータ（postdominator）を計算する信頼性構成要素を導入することによって、主要な困難、即ち、低レベルでのプログラム構造の欠如を回避する。この構成要素はＴＣＢの中にあり、信頼されなければならない。
【００１８】
[0018]Ａｖｖｅｎｕｔｉらは、Ｊａｖａ  ｂｙｔｅｃｏｄｅ  ｖｅｒｉｆｉｃａｔｉｏｎ  ｆｏｒ  ｓｅｃｕｒｅ  ｉｎｆｏｒｍａｔｉｏｎ  ｆｌｏｗ，  ＡＣＭ  ＳＩＧＰＬＡＮ  Ｎｏｔｉｃｅｓ，  ３８（１２）：２０−２７，  Ｄｅｃ．  ２００３  において、抽象解釈を適用してスタックベースのバイトコード言語に情報フローを強制した。機械モデルにおける相違のほかに、Ａｖｖｅｎｕｔｉらの努力は、更に、制御フロー・グラフ及びポストドミネータの計算に依存した。
【００１９】
[0019]Ｚｄａｎｃｅｗｉｃ及びＭｙｅｒｓは、Ｓｅｃｕｒｅ  ｉｎｆｏｒｍａｔｉｏｎ  ｆｌｏｗ  ｖｉａ  ｌｉｎｅａｒ  ｃｏｎｔｉｎｕａｔｉｏｎｓ，  Ｈｉｇｈｅｒ−Ｏｒｄｅｒ  ａｎｄ  Ｓｙｍｂｏｌｉｃ  Ｃｏｍｐｕｔａｔｉｏｎ，  １５（２−３）：２０９−２３４，  Ｓｅｐｔ．  ２００２  において、線形連続を使用して低レベルで非干渉を強制する。Ｚｄａｎｃｅｗｉｃ及びＭｙｅｒｓの言語は変数に基づいており、依然としてアセンブリ言語とは大きく異なっている。具体的には、線形連続は、情報フローの解析を助けるスタック原理を強制するには有用であるが、従来のアセンブリコードには不在である。したがって、ネイティブコードへの更なる（信頼性）コンパイルが必要である。
【００２０】
[0020]従来、コンパイルの認証は、大部分が標準型安全特性（例えば、ＴＡＬ、ＰＣＣ、ＥＣＣ）について実行された。コンパイルの認証は、セキュリティポリシーへ適用された。しかし、そのようなシステムは、セキュリティオートマトンに基づいており、したがって非干渉を強制することはできない。前述したＢａｒｔｈｅらによるセキュリティ型保存コンパイルに関する努力のほかに、セキュリティ型を有するπ計算法の関連問題も研究された。ＲＩＳＣ形式アセンブリコードを目標にして提案された関連する解法は残されていない。
【発明の概要】
【００２１】
[0021]情報フローの強制を実行する方法、製造品、及び装置が開示される。一実施形態において、方法は、セキュアに型付けされたネイティブコードを受け取り、セキュリティポリシーに基づいて、セキュアに型付けされたネイティブコードに対して情報フローに関する検証を実行することを含む。
【００２２】
[0022]本発明は、下記で与えられる詳細な説明及び本発明の様々な実施形態の添付の図面から一層完全に理解されるであろう。しかし、これらは本発明を特定の実施形態へ限定すると解釈されてはならず、説明及び理解のためのものにすぎない。
【本発明の詳細な説明】
【００２３】
[0046]低レベル情報フロー解析の型付けシステムが開示される。一実施形態において、システムは、型付きアセンブリ言語と互換性があり、メモリ・タプル及び第１級コード・ポインタを含むＲＩＳＣコードの重要な特徴をモデル化する。非干渉定理は、良好に型付けされたプログラムが機密性を守ることを明瞭に示す。システムを目標にするセキュリティ型保存変換も、その健全性定理と同じく呈示される。これは、非干渉へのコンパイル認証の応用を示す。これらの言語ベースの手法は、機密扱いデータの機密性を保護するために有望である。ＲＩＳＣ形式アセンブリコードについては、そのような低レベルの検証が望ましい。なぜなら、それは小さな信頼性計算ベースを生じるからである。更に、多くのアプリケーションは、ネイティブコードで直接配布される。
【００２４】
[0047]本発明の実施形態は、ＲＩＳＣ形式のアセンブリコードに焦点を当てる。一実施形態において、型付け注釈が使用されて高レベル・プログラム構造に関する情報を回復し、ポストドミネータを計算する追加の信頼性構成要素を必要としない。更に、本明細書で記述された手法は、追加の構造、例えば、線形連続又は連続スタックに依存しない。消去意味論（erasuresemantics）は、言語のプログラムを通常のアセンブリコードへ縮小する。
【００２５】
[0048]下記されるように、言語ベースのアプローチが使用され、強制はプログラムコードの静的解析に基づく。それは実行時にセキュリティラベルの計算及び記憶を必要としない。更に、プログラムコード及び注釈（annotations）の精査は、ラベル・クリープへ落ち入ることなく、暗黙的フローの検出を可能にする。
【００２６】
[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]高レベル言語で情報を転送する１つの方法は、代入を使用することである。前述したように、高レベル言語における変数は、セキュリティラベル、例えば、低及び高で「タグ付け」することができる。セキュリティ型システムは、代入についてラベルのミスマッチを防止する。アセンブリ・レベルにおいて、メモリ・セルは同じようにタグ付け可能である。メモリ・セルの中へ記憶するとき、型付け規則は、ソースのセキュリティラベルが目標とマッチすることを確保する。
【００５６】
[0079]レジスタによる情報フローの規制は異なる。なぜなら、レジスタは、異なるセキュリティラベルを有する異なる変数について再使用可能だからである。変数及び活性情報はアセンブリ・レベルでは利用できず、それを強制の基礎とすることは、容易にできることではない。
【００５７】
[0080]実際、通常型の安全についても類似の問題が生じる。型付きアセンブリ言語（ＴＡＬ）の中のレジスタは、異なるプログラム点で異なる型を有することができる。これらの型は、本質的に、計算自体から推論される。例えば、加法命令ａｄｄ  ｒｄ，ｒｓ，ｒｔにおいて、レジスタｒｄは型ｉｎｔを与えられる。なぜなら、ｉｎｔのみが、ここでは有効であり得るからである。同様に、メモリ・セルからロードしているとき、目標レジスタはソース・メモリ・セルの型を与えられる。発明者らは、そのような推論をセキュリティラベルに適合化する。加法ａｄｄ  ｒｄ，ｒｓ，ｒｔにおいて、ｒｄのラベルはｒｓ及びｒｔのラベルを結合することによって取得される。なぜなら、ｒｄの中の結果はｒｓ及びｒｔからの情報を反映するからである。移動及びメモリ読み取り命令は、同様に取り扱われる。
【００５８】
（プログラム構造）
[0081]高レベル・プログラムの条件文は、双方の部分コマンドが保護式のセキュリティレベルを守るように検証可能である。そのような検証はアセンブリコードでは困難になる。アセンブリコードにおいて、「平坦化された（flattened）」制御フローは、プログラム構造を識別するとき、ほとんど援助を提供しない。条件文は、典型的には、分岐命令（ｂｎｚ  ｒ，ｌ）及び幾つかのコード・ブロックへ変換される。その場合、２つの分岐のポストドミネータは、もはや明らかでない。
【００５９】
[0082]一実施形態において、注釈が使用され、ポストドミネータが必要であるとき、常に、ポストドミネータを指し示すことによって、プログラム構造を回復する。注意すべきは、高レベル・プログラムがポストドミネータを判定するための十分な情報を提供し、これらのポストドミネータが、常に、静的に判定可能であることである。例えば、条件付きコマンドの終わりは、２つの分岐のポストドミネータである。したがって、コンパイラは、セキュアに型付けされたソースプログラムに基づいて、注釈を自動的に生成することができる。本発明のシステムの一実施形態において、ポストドミネータ注釈は、セキュリティラベルとペアにされた静的コード・ラベルである。
【００６０】
[0083]分岐命令（ｂｎｚ  ｒ，ｌ）は、異なる実行経路を直接に生じる唯一の命令であるから、分岐命令をポストドミネータで強化すべきであるように思われる。したがって、型付け規則は、保護式を考慮に入れる適切なセキュリティコンテキストのもとで双方の分岐を検査する。そのようなセキュリティコンテキストは、ポストドミネータへ到達したときに終了する。
【００６１】
[0084]もっともらしいが、このアプローチは未熟である。図３は、３つのシナリオを示す。条件文シナリオのほかに、分岐命令はｗｈｉｌｅループを実現するためにも使用される。その場合、ポストドミネータは正確に分岐の１つの始まりである。この場合、他の分岐のみが、新しいセキュリティコンテキストのもとで検査されるべきである。分岐命令が直接に注釈されるならば、対応する型付け規則は「オーバーロード」されるであろう。更に重要なことに、アセンブリ・プログラムは、分岐命令が存在しない「暗黙の分岐」を含んでもよい。第３のシナリオは、オペランド・レジスタの値に基づいて、間接ジャンプがプログラムを異なる経路へ導くことを示す。具体的な例は、この後で明らかになるであろう。
【００６２】
[0085]より良好な解決法のインスピレーションは、図２の簡単なシステムに存在する。注意すべきは、小前提規則［Ｃ４］が特定のコマンドに結びつけられないことである。それは、本質的に、セキュリティレベルが低から高へ上げられる計算領域をマークする。領域の終わりは、まさにポストドミネータである。これに続いて、一実施形態では、本明細書で記述されるアプローチが、２つの低レベル演算ｒａｉｓｅ及びｌｏｗｅｒで、高レベルの小前提規則を模倣する。これらの演算は、セキュリティコンテキストを明白に操作し、セキュリティ領域の始まり及び終わりをマークする。
【００６３】
（メモリの再命名）
[0086]メモリ・セルの再命名は、情報転送の他の道筋を与える。図４において、低ポインタｐ＿ｌ及び高ポインタｐ＿ｈは、同じセルの別名である（それらは、同じ値を指す２つのポインタである）。同じ図面の中のコードは、ｐ＿ｈに他のセルを指させることによって、或る高の変数ｈに基づいて再命名関係を変更してよい。ｐ＿ｈによる更なる修正は、元のセルに記憶された値を変更しても変更しなくてもよい。結果として、低ポインタｐ＿ｌによる観察は、高の変数ｈに関する情報を公表する。
【００６４】
[0087]問題は、高ポインタｐ＿ｈによる代入に存在する。なぜなら、それは再命名関係に関する情報を顕示するからである。一実施形態において、ポインタは２つのセキュリティラベルでタグ付けされる。１つは、ポインタ自体のためであり、他の１つは参照されているデータのためである。一実施形態において、高ポインタによる低データへの代入は許されない。これは保守的なアプローチである。即ち、全てのポインタが潜在的別名として考えられる。
【００６５】
（コード・ポインタ）
[0088]コード・ポインタは、情報フローを更に複雑にする。図５は、高の変数ｈに基づいてｆが異なる関数を表す関数コードの断片を示す。異なるコード・ラベルは、アセンブリ・レベルでのリフレクションで、ｈの値に基づいてｆへ代入されるであろう。当然のことながら、ｆは機密扱い情報を含み、高に型付けされるべきである。しかしながら、実際の関数ｆ０及びｆ１は低コンテキストのもとでのみ実行可能である。なぜなら、それらは低の変数ｌを修正するからである。この場合、ｆへの呼び出しは禁止されるべきである。
【００６６】
[0089]本発明のシステムの一実施形態において、データ・ポインタと同じく、コード・ポインタも２つのセキュリティラベルを与えられる。型付け規則は、高コード・ポインタを介して低関数が呼び出されないことを確保する。
【００６７】
（セキュリティコンテキスト強制力）
[0090]図６は、変動性コード・ポインタがフロー解析を複雑にするコードの断片を示す。関数ｆ０及びｆ１のみが高データを修正する。参照セルｆは、高条件文の中で、異なるコード・ポインタを代入される。後に、参照セルｆは、参照を解かれ、低コンテキストの中で呼び出される。
【００６８】
[0091]このコードは情報フローに関して安全である。高レベルにおいて、図２の規則［Ｃ４］のような小前提規則は、低コンテキストで高関数！ｆ（）の呼び出しを可能にする。しかし、そのアセンブリ対応部分において、ｆへの呼び出し及びｆからの戻りは、間接ジャンプとして実現される。呼び出しシーケンスは、低コンテキストから高コンテキストへ制御を移転するが、戻りシーケンスは反対のことを行う。関数呼び出しは、アセンブリ・レベルでは、もはやアトミックではないので、小前提規則を直接考案することはできない。更に、ｆが参照を解かれて呼び出されるとき（図３の第３のシナリオ）、明示の分岐命令は存在しない。
【００６９】
[0092]本発明のシステムの一実施形態において、ｒａｉｓｅ及びｌｏｗｅｒ演算は、小前提規則の境界を明示的にマークする。コンパイル認証の間、ソースレベルの型付け及びプログラム構造は、目標レベル注釈を生成するための十分な情報を提供する。小前提規則がソースコードの中で適用されるとき、対応する目標コードがｒａｉｓｅ及びｌｏｗｅｒ演算のペアの中で生成される。
【００７０】
（情報フローポリシーの強制）
[0093]前述したように、本発明の実施形態は、アセンブリコードに対して情報フローポリシーを直接強制する。このアプローチの利点は、図７Ａ及び図７Ｂで例示される。図７Ａで示されるように、既存の言語ベースのアプローチは、高レベル言語（例えば、Ｊａｖａ）のためにセキュリティ型システムを使用して情報フローを強制する。検証は、ソースレベルでのみ達成される。しかし、高レベルプログラムは、実計算機で実行する前にコンパイルされなければならない。コンパイラは、ネイティブコードの生成を含む変換の大部分を達成する。変換又は最適化のバグは、ソースプログラムについて確立されたセキュリティの保証を無効にするかも知れない。結果として、そのようなソースレベル検証は、巨大な信頼性計算基盤に依存する。
【００７１】
[0094]対照的に、本明細書において、アセンブリコードを直接検証するセキュリティ型システムが記述される。図７Ｂで示されるように、検証は、セキュアに型付けされたネイティブコードの上で達成される。これは、信頼性計算基盤からコンパイラの多くを除去し、それによって信頼に値する環境を達成する。更に、これは、プログラムのセキュリティの検証が、ネイティブコードの中に直接分散されることを可能にする。
【００７２】
[0095]本発明のセキュリティ型システムの実施形態は、セキュリティコンテキストに依存して、プログラム構造から生じる暗黙のフローを防止する。セキュリティコンテキストは、２つの演算、即ち、ｒａｉｓｅ及びｌｏｗｅｒによって明示的に操作される。図８は例示的経路を示す。プログラムが、機密扱いデータに基づいて、異なる実行経路へ分岐する地点で、セキュリティコンテキストは、データの機密扱い性を捕捉するため十分に高く上げられる。図８において、これはＰｓｔａｒｔからＰｅｎｄへ実行するプログラムの中で地点８０１及び８０２で起こる。異なる実行経路が合流する場所（即ち、ポストドミネータ）において、セキュリティコンテキストは元のレベルへ下げられる。図８において、これはＰｓｔａｒｔからＰｅｎｄへ実行するプログラムの地点８０３及び８０４で起こる。こうして、プログラムコードは、異なるセキュリティ領域へ組織化されていると静的に見ることができる。セキュリティ領域の始まり及び終わりは、ｒａｉｓｅ及びｌｏｗｅｒによって明示的にマークされる。
【００７３】
[0096]懸案のセキュリティレベルθが与えられると、データ項目は、そのセキュリティレベルとθとの比較に基づいて、公開又は機密として見られる。所望の非干渉の結果は、公開出力データが機密の入力データに関する情報を反映しないことである。一実施形態において、非干渉の結果は、同値関係
【数１】
2008524726.tif 000003
（以下、本明細書では、上記の数学記号を≒θと記載）に基づいて確立される。直感的には、２つの機械状態は、同じ公開データを含むならば、セキュリティレベルθに関して同値である。図９は、異なるが同値の入力に基づいて、同じプログラムの２つの実行経路を示す。低いセキュリティコンテキストのもとで、２つの実行は横並び様式で相互にマッチする。高セキュリティコンテキストのもとでは、２つの実行は異なるコードを含むかも知れない。しかし、本発明のシステムの実施形態は、高セキュリティコンテキストのもとで低データが更新されないことを確実にする。こうして、同値関係の推移に続いて、２つの実行は、同値状態を有するポストドミネータで合流する。
【００７４】
[0097]本発明のシステムの一実施形態は、機密情報を型注釈の中にコード化する。検証プロセスは、幾つかの型付け規則によって導かれる。図１０は、プログラムをその型注釈に対して検証するプロセスの一実施形態の流れ図である。このプロセスは、タスクを３つの構成要素、即ち、ヒープの検証、レジスタ・ファイルの検証、及び命令シーケンスの検証へ委任する。プログラムは、３つの構成要素の全てが成功を戻すときにのみ、セキュリティポリシーに関して安全である。プロセスは、ハードウェア（回路、専用論理など）、ソフトウェア（例えば、汎用コンピュータ又は専用機械で実行される）、又はこれらの組み合わせを含む処理論理によって達成される。
【００７５】
[0098]命令シーケンスの検証は、最も複雑な部分である。しかし、それは完全に構文的であり、それによって直接的で機械的な実現を可能にする。現在の命令の構文に基づいて、検証は異なる型付け規則に対して実行される。検証は、型付け規則が満足されないとき常に失敗し、機密違反を報告する。型付け規則が現在の命令で満足されるならば、検証は残りの命令シーケンスで再帰的に進行する。最後に、命令シーケンスの終わりに到達すると（即ち、ｊｍｐ又はｈａｌｔ）、処理論理は、対応する規則を検査した後に検証を終了する。
【００７６】
[0099]一実施形態において、図１４、図１５、及び図１６に記述される形式規則が使用され、下記で説明される。
【００７７】
[00100]図１０を参照すると、ＨがΨに対して検証可能かどうかを処理論理がテストする（処理ブロック１００２）ことによって、プロセスが開始する。それが失敗すれば、処理論理は、プログラムが受け入れられないことを示す（処理ブロック１０１０）。受け入れられるならば、処理論理は、Ｒが（Ψ，Γ）に対して検証可能かどうかをテストする（処理ブロック１００３）。検証可能でなければ、処理論理は、プログラムが受け入れられないことを示す（処理ブロック１０１０）。検証可能であれば、処理論理は、Ｓが（Ψ，Γ，κ）に対して検証可能かどうかをテストする（処理ブロック１００４）。検証可能であれば、処理論理は、プログラムが受け入れられることを示す（処理ブロック１０１１）。
【００７８】
[00101]図１１は、命令シーケンスの検証について例示的流れ図を示す。
【００７９】
（抽象機械）
[00102]一実施形態において、言語ＴＡＬＣは、通常の型安全性の既存の結果と統合が容易であるため、ＴＡＬ及びＳＴＡＬと類似する。幾つかの追加の構造は機密について使用され、提案されたセキュリティ演算と直交する幾つかのＴＡＬ及びＳＴＡＬ特徴は除去される。セキュリティラベルは格子£を形成すると想定される。記号θは、£の要素の上で範囲を定めるために使用される。記号⊥及びＴは、格子の底部及び頂部として使用され、∪及び∩は格子の合併及び交わり演算として使用され、⊆は格子の順序づけとして使用される。下記はＴＡＬＣの構文的構造を説明する。
【００８０】
[00103]図１２の上部は型構造を呈示する。セキュリティコンテキストはκで示される。空のセキュリティコンテキスト（・）は、最低セキュリティラベルを有するプログラム・カウンタを表す。具体的コンテキスト
【数２】
2008524726.tif 000004
（以下、本明細書では、上記の数学記号を▽と記載）は、セキュリティラベルθ（現在のセキュリティレベル）及びポストドミネータｗから構成される。ポストドミネータｗはワード値の構文を有するが、その使用は最終的にインスタンス化コード・ラベル、即ち、現在のセキュリティレベルの終了点である意味論によって制限される。ポストドミネータｗは、更に、変数αであってよい。これはコンパイル手続きで有用である。コンパイル手続きは、異なるポストドミネータを有する異なるコンテキストの中で呼び出し可能である。
【００８１】
[00104]事前型τは、整数型、タプル型、及びコード型を含めてＴＡＬの中で見られるような通常の型を反映する。ＴＡＬと比較すると、一実施形態において、本明細書で説明されるコード型は、インタフェースの一部分として特別のセキュリティコンテキスト（κ）を必要とする。型（σ）は、セキュリティラベルでタグ付けされた事前型であるか、非初期化スタック・スロットのナンセンス型（ｎｓ）である。スタック型（Σ）は、変数（ρ）、又は型の（可能性として空の）シーケンスである。変数コンテキスト（Δ）は、多相性コードを型付けするために使用される。それはスタック型変数（ρ）及びポストドミネータ変数（α）を文書化する。スタック型及びポストドミネータも、一般的に、本明細書では型引数ψと呼ばれる。最後に、ヒープ型（Ψ）又はレジスタ・ファイル型（Γ）は、ヒープ・ラベル又はレジスタから型へのマッピングである。レジスタ・ファイルの中のｓｐはスタックを表す。
【００８２】
[00105]図１２の中間部分は、値の構造を示す。ワード値ｗは、変数、ヒープ・ラベルｌ、即値整数ｉ、非初期化スタック・スロットのナンセンス値、又は型引数でインスタンス化された他のワード値のいずれかである。小さな値ｖは、幾つかの命令のオペランドとして役立つ。それらは、レジスタｒ、ワード値ｗ、又はインスタンス化された小さな値である。ヒープ値ｈは、タプル又は型付けされたコード・シーケンスである。それらはヒープＨのビルディング・ブロックである。注意すべきは、値はセキュリティラベルを保持しないことである。これは値が固有に機密扱いであるわけではないこと、即ち、それは機密扱いロケーションから来るときにのみ機密扱いであるという考え方と首尾一貫する。機密扱いロケーションは、対応する型（Ψ及びΓ）の中で文書化される。最後に、レジスタ・ファイルＲは、全てのレジスタ及びスタックの内容を記憶する。ここで、スタックとは、ワード値の（可能性として空の）シーケンスである。
【００８３】
[00106]コード構造は、図１２の下部に与えられる。ＴＡＬ及びＳＴＡＬからの最小命令セットが保持され、２つの新しい命令（ｒａｉｓｅ  κ及びｌｏｗｅｒ  ｌ）が、前述したようにセキュリティコンテキストを取り扱うために導入される。一実施形態において、プログラムは、セキュリティコンテキストでタグ付けされた通常のトリプルである。セキュリティコンテキストは、形式的な健全性証明を容易にするが、計算に影響を与えない。
【００８４】
[00107]操作的意味論（図１３）において、セキュリティコンテキストを修正する２つのケースがあるだけである。即ち、ｒａｉｓｅ  κ’はセキュリティコンテキストをκ’へ更新し、ｌｏｗｅｒ  ｗは、目標コードｗのインタフェースから新しいセキュリティコンテキストを選択する。全ての他のケースにおいて、セキュリティコンテキストは同じままであり、意味論は標準である。操作的意味論は実計算機の振る舞いを模倣する。従来の機械は、セキュリティコンテキスト及びｒａｉｓｅ  κ命令を除去し、ｌｏｗｅｒ  ｗをｊｍｐ  ｗで置換することによって取得可能である。
【００８５】
（型付け規則）
[00108]静的意味論は、図１４で要約された判断形式から構成される。セキュリティコンテキストは、有効な命令シーケンスの判断の中に現れる。ヒープ及びレジスタ・ファイルの型は、非干渉定理を容易にするため有効なプログラムの判断の中で明示的にされる。全ての他の判断形式は、ＴＡＬ及びＳＴＡＬと酷似する。
【００８６】
[00109]型付け規則は、図１５及び図１６で与えられる。全ての自由型変数が型環境で文書化されるならば、型構造は有効である（図１４の上部の６つの判断形式）。ヒープ値及び整数は、任意のセキュリティラベルを有してもよい。ヒープ・ラベル及びレジスタの型は、それぞれヒープ型及びレジスタ・ファイル型で説明されるとおりである。非命令の全ての他の規則は直接的である。
【００８７】
[00110]一実施形態において、κのセキュリティラベル構成要素を参照するため、マクロＳＬ（κ）が使用される。ＳＬ（・）は⊥として定義される。ａｄｄ、ｌｄ、及びｍｏｖ命令の型付け規則は、行き先レジスタのセキュリティラベルを推論する。即ち、それらはソース及び目標オペランド及び現在のセキュリティコンテキストのセキュリティラベルを考慮に入れる。
【００８８】
[00111]ｂｎｚの規則は、保護レジスタｒが整数であり、目標値ｖがコード・ラベルであるかを最初に検査する。次に、それは、現在のセキュリティコンテキストが保護（プログラム構造を介してフローを防止する）及び目標コード（コード・ポインタを介してフローを防止する）のセキュリティレベルをカバーするのに十分高いかを検査する。最後に、レジスタ・ファイル及び残りの命令シーケンスの検査は、双方の分岐が実行するのに安全であることを確実にする。
【００８９】
[00112]ｓｔの規則は、４つのセキュリティラベルに関わっている。この規則は、目標セルのラベルが、コンテキスト、包含タプル、及びソース値よりも高いか等しいことを確実にする。
【００９０】
[00113]スタック命令の規則は、類似のアイデアに従っている。要約すると、スタックは、無限数のレジスタと見ることができる。命令ｓａｌｌｏｃ又はｓｆｒｅｅは、スロットへ新しいスロットを付加するか、スロットから既存のスロットを除去し、それによって規則は、更新されたスタック型のもとで残りの命令シーケンスを検査する。命令ｓｌｄ又はｓｓｔの規則は、ｍｏｖ命令に続いて理解可能である。
【００９１】
[00114]ｒａｉｓｅの規則は、新しいセキュリティコンテキストが現在のコンテキストよりも高いかを検査する。更に、それは新しいコンテキストのポストドミネータｗ’に注目し、ｗ’でのセキュリティコンテキストが現在のコンテキストとマッチすることを確実にする。残りの命令シーケンスは、新しいコンテキストのもとで検査される。
【００９２】
[00115]ｒａｉｓｅの規則が安全領域の終了ラベルの有効性を既に検査したので、領域を終了するタスクは比較的簡単である。ｌｏｗｅｒの規則は、そのオペランド・ラベルが、セキュリティコンテキストによって指示されたものとマッチするかを検査する。これは、安全領域がｒａｉｓｅ及びｌｏｗｅｒのペアで囲まれることを保証する。規則は、更に、ｗでのコードが実行するのに安全であることを確実にする。これは、セキュリティラベル及びレジスタ・ファイル型を検査することを含む。
【００９３】
[00116]ｊｍｐの規則は、目標コードが実行するのに安全であるかを検査する。類似の検査はｂｎｚの規則にも現れた。これらの２つの規則において、目標コードのセキュリティコンテキストは現在のコンテキストと同じである。これは、システムの一実施形態において、コンテキストの変更が、従来の命令から分離されるからである。例えば、高目標コードを低コンテキストで呼び出す前に、それをｒａｉｓｅ及びｌｏｗｅｒの中に囲んでよい。
【００９４】
[00117]最後に、セキュリティコンテキストが空であり、ｒ１の中の値が、期待された型σを有するときにのみ、ｈａｌｔが有効である。
【００９５】
[00118]ＴＡＬＣ言語は、従来の型の安全性（メモリ及び制御フローの安全性）を享受する。この安全性は、進行及び保存補助定理に従って確立可能である。これらの補助定理の証明はＴＡＬ及びＳＴＡＬと類似しており、本発明を不明瞭にすることを避けるため省略された。
補助定理１（進行）：Ψ；Γ├Ｐであれば、次のいずれかである。
１．
【数３】
2008524726.tif 000005
（以下、本明細書では、上記の数学記号を├→と記載）となるようなＰ’が存在するか、又は
２．Ｐは、（Ｈ，Ｒ｛ｒ１├→ｗ｝，ｈａｌｔ［σ］）の形式である。ここで、├Ｈ：Ψ及びΨ；°├ｗ：σである。
補助定理２（保存）：Ψ；Γ├Ｐ及びＰ├→Ｐ’であれば、Ψ；Γ’├Ｐ’となるようなΓ’が存在する。
【００９６】
[00119] ＴＡＬＣの非干渉定理を呈示する前に、２つのプログラムの同値が、所与のセキュリティレベルθに関して定義される。
定義１（ヒープの同値）：Ψ├Ｈ１≒θＨ２⇔全てのl∈ｄｏｍ（Ψ）について、
Ψ（ｌ）＝τθ’及びθ’⊆θは、Ｈ１（ｌ）＝Ｈ２（ｌ）を暗黙に意味する。
定義２（スタックの同値）：Σ├Ｓ１≒θＳ２⇔全てのスタック・スロットｉ∈ｄｏｍ（Σ）について、
Σ（ｉ）＝τθ’及びθ’⊆θは、Ｓ１（ｉ）＝Ｓ２（ｉ）を暗黙に意味する。
定義３（レジスタ・ファイルの同値）：Γ├Ｒ１≒θＲ２⇔双方
１．Γ（ｓｐ）├Ｒ１（ｓｐ）≒θＲ２（ｓｐ）、及び
２．全てのｒ∈ｄｏｍ（Γ）について、Γ（ｒ）＝τθ’及びθ’⊆θは、Ｒ１（ｒ）＝Ｒ２（ｒ）を暗黙に意味する。
定義４（プログラムの同値）：Ψ；Γ├Ｐ１≒θＰ２⇔Ｐ１＝（Ｈ１，Ｒ１，Ｉ１）κ１、Ｐ２＝（Ｈ２，Ｒ２，Ｉ２）κ２、Ψ├Ｈ１≒θＨ２、Ψ；Γ├Ｒ１≒θＲ２、及び次のいずれか、
１．κ１＝κ２、ＳＬ（κ１）⊆θ、及びＩ１＝Ｉ２、又は
２．
【数４】
2008524726.tif 000006
【００９７】
[00120]上記の３つの関係は、全て反射的、対称的、及び推移的である。非干渉定理は、（懸案のセキュリティレベルに対して）低いセキュリティコンテキストで開始する２つの同値プログラムの実行に関係する。双方の実行が終了すれば、結果のプログラムも同値でなければならない。
【００９８】
[00121]証明の基本的アイデアは直感的である。プログラムのセキュリティコンテキスト及び懸案のセキュリティレベルに基づいて、実行は「低ステップ」及び「高ステップ」の段階へ分けることができる。低ステップでの２つの実行は関係づけることができる。なぜなら、それらは同じ命令を実行しているからである。高ステップでの論法は異なる。即ち、２つの実行は、もはや横並びではない。しかし、ｒａｉｓｅ及びｌｏｗｅｒが安全領域の始まり及び終わりをマークし、したがってプログラム状態はｒａｉｓｅの前及びｌｏｗｅｒの後で関係づけられ、こうして高ステップで２つの実行を直接関係づけることを回避する。３つの補助定理及び非干渉定理を有する追加の公式詳細が提供される。補助定理３は、高ステップにおけるセキュリティコンテキストがｒａｉｓｅ又はｌｏｗｅｒでのみ変更可能であることを示す。補助定理４は、終了プログラムが、ｌｏｗｅｒで現在のセキュリティコンテキストを解放するステップへ縮小されることを記述する。補助定理５は、低ステップにおける２つの同値プログラム間の横並び関係を明瞭に示す。したがって、定理１は、これらの補助定理から続く。
【００９９】
[00122]下記において、├→＊は├→の反射的及び推移的終結を表し、
【数５】
2008524726.tif 000007
（以下、本明細書では、上記の数学記号を≧θと記載）は、全てのｉについてΣ（ｉ）＝Σ’（ｉ）であり、Σ’（ｉ）＝τθ及びθ’⊆θとなることを意味する。Γ≧θΓ’は、Γ（ｓｐ）≧θΓ’（ｓｐ）及び全てのｒについてΓ（ｒ）＝Γ’（ｒ）であり、Γ’（ｒ）＝τθ’及びθ’⊆θとなることを意味する。記号ＱはＰに追加して使用され、２つの実行を比較するときのプログラムを表す。
補助定理３（高ステップ）：  Ｐ＝（Ｈ，Ｒ，Ｉ）κ、
【数６】
2008524726.tif 000008
，Ψ；Γ├Ｐであれば、次のいずれかである。
１．Ｐ├→Ｐ１、Ψ；Γ１├Ｐ１、Γ≧θΓ１、及びΨ；Γ１├Ｐ≒θＰ１となるようなΓ１及びＰ１＝（Ｈ１，Ｒ１，Ｉ１）κが存在するか、又は
２．Ｉは形式（ｒａｉｓｅ  κ’；Ｉ’）又は（ｌｏｗｅｒ  ｗ）である。
証明の概要：  Ｉの最初の命令のケース解析による。Ｉはｈａｌｔではあり得ない。なぜなら、ｈａｌｔの型付け規則は、コンテキストが空であることを要求するからである。Ｉがｈａｌｔ、ｒａｉｓｅ、又はｌｏｗｅｒでなければ、型付け規則の操作的意味論及び反転によって、次のステップのためにΓ１及びＰ１を発見することができる。型付け規則は低ヒープ・セルへの書き込みを禁止し、したがって低ヒープ・セルはステップの後も同じままである。レジスタが更新されるとき、Γ１は、ＳＬ（κ）を考慮に入れたセキュリティラベルを有する更新型をレジスタに与え、したがってそのレジスタ又はスタック・スロットはΓ１の中に高の型を有する。結果として、Γ≧θΓ及びΨ；Γ１├Ｐ≒θＰ１である。
補助定理４（コンテキストの解放）：  Ｐ＝（Ｈ，Ｒ，Ｉ）θ▽ｗ、
【数７】
2008524726.tif 000009
、Ψ；Г├Ｐ、Ｐ├→＊（Ｈ０，Ｒ０，ｈａｌｔ［σ］）．であれば、Ψ；Γ’├Ｐ’、Ｐ├→＊Ｐ’、Γ≧θ’Γ’、及びΨ；Γ’├Ｐ≒θＰ’となるようなГ’及びＰ’＝（Ｈ’，Ｒ’，ｌｏｗｅｒ  ｗ）θ▽ｗが存在する。
証明の概要：  誘導Ｐ├→＊（Ｈ０，Ｒ０，ｈａｌｔ［σ］）のステップ数の上の一般化された帰納法による。
【０１００】
[00123]ゼロ・ステップの基本的ステップは可能でない。なぜなら、セキュリティコンテキストはマッチしないからである。帰納的ケースにおいて、実行がｎ個のステップから成ると仮定すれば、ｎよりも小さい任意のステップ数について命題が成り立つ。補助定理３に続いて、考慮すべき２つのケースが存在する。
【０１０１】
[00124]Ｉの最初の命令がｒａｉｓｅ又はｌｏｗｅｒでないケースでは、補助定理３によって、Ｐ├→Ｐ１、Ψ；Γ１├Ｐ１、Γ≧θ’Γ１、Ψ；Γ１├Ｐ≒θ’Ｐ１となるようなΓ１及びＰ１が存在し、Ｐ１のセキュリティコンテキストはＰと同じである。注意すべきこととして、Ｐ１はＰと最終プログラム（Ｈ０，Ｒ０，ｈａｌｔ［σ］）との間のステップである。なぜなら、操作的意味論は決定論的だからである。こうして、Ｐ１の帰納法の仮定によって、Ψ；Γ’├Ｐ’、Ｐ１├→＊Ｐ’、Γ１≧θ’Γ’、及びΨ；Γ’├Ｐ１≒θ’Ｐ’となるようなΓ’及びＰ’が存在する。上記を一緒にすると、Ｐ├→＊Ｐ’、Γ≧θ’Γ’となる。なぜなら、≧θ’は定義によって推移的であり、定義及びΓ１≧θ’Γ’という事実によってΨ；Γ’├Ｐ≒θ’Ｐ’だからである。
【０１０２】
[00125]ケースＩ＝ｒａｉｓｅθ１▽ｗ１；Ｉ１である。操作的意味論の定義によって、Ｐ├→Ｐ１である。ここで、Ｐ１＝（Ｈ，Ｒ，Ｉ１）θ１▽ｗ１である。Ψ；Γ├Ｐの反転及びｒａｉｓｅの型付け規則によって、θ⊆θ１及びΨ；Γ；θ１▽ｗ１├Ｉ１である。良好に型付けされたプログラムの定義によって、Ψ；Γ├Ｐ１である。Ｐ１の帰納法の仮定によって、Ψ；Γ２├Ｐ２、Ｐ１├→＊Ｐ２、Γ≧θ’Γ２、及びΨ；Γ２├Ｐ１≒θ’Ｐ２となるようなΓ２及びＰ２＝（Ｈ２，Ｒ２，ｌｏｗｅｒ  Ｗ１）θ１▽Ｗ１が存在する。次に、Ψ；Γ２├Ｐ≒θ’Ｐ２が続く。なぜなら、ヒープ及びレジスタ・ファイルは、Ｐ及びＰ１の中で同じだからである。
【０１０３】
[00126]更に、操作的意味論によって、Ｐ２├→Ｐ３である。ここでＰ３＝（Ｈ２，Ｒ２，Ｉ３）κであり、Ｉ３はκのセキュリティコンテキストを有するｗ１のインスタンス化されたコードである。Ｉの良好な型付け（即ち、ｒａｉｓｅ  θ１▽ｗ１；Ｉ１）の反転によって、κ＝θ▽ｗである。Ｐ３の帰納法の仮定によって、Ψ；Γ’├Ｐ’、Ｐ３├→＊Ｐ’、Γ２≧θ’Γ’、及びΨ；Γ’├Ｐ３≒θ’Ｐ’となるようなΓ’及びＰ’＝（Ｈ’，Ｒ’，ｌｏｗｅｒ  ｗ）θ▽ｗが存在する。上記を一緒にすると、元の命題は、ケースＩ＝ｒａｉｓｅ  θ１▽ｗ１；Ｉ１について成り立つ。
【０１０４】
[00127]ケースＳ＝ｌｏｗｅｒ  ｗ１。ｌｏｗｅｒの型付け規則の反転によって、ｗ＝ｗ１である。Ｐ’＝Ｐとすれば、命題は成り立つ。
補助定理５（低ステップ）：  Ｐ＝（Ｈ，Ｒ，Ｉ）κ、ＳＬ（κ）⊆θ、Ψ；Γ├Ｐ、Ψ；Γ├Ｑ、Ψ；Γ├Ｐ≒θＱ、Ｐ├→Ｐ１、Ｑ├→Ｑ１であれば、Ψ；Γ├Ｐ１、Ψ；Γ├Ｑ１、及びΨ；Γ１├Ｐ１≒θＱ１となるようなΓ１が存在する。
証明の概要：  Ｉの最初の命令のケース解析による。ＳＬ（κ）⊆θであるから、≒θの定義によってＰ及びＱは同じ命令シーケンスを含む。より高いコンテキストへ上げるケースは状態を変更せず、それによって自明に同値を維持する。全ての他のケースは、セキュリティコンテキストがθよりも低いことを維持する。型付け誘導の精査は、ヒープ内の低位置のみへ低値を代入できることを示す。一度レジスタが高値を与えられると、Γ１の中のその型は高へ変化するであろう。分岐のケースでは、保護は低でなければならず、したがってＰ及びＱの双方は同じコードへ分岐する。こうして、２つのプログラムは１つのステップの後で同値のままである。
定理１（非干渉）：  Ｐ＝（Ｈ，Ｒ，Ｉ）κ、ＳＬ（κ）⊆θ’、Ψ；Γ├Ｐ、Ψ；Γ├Ｑ、Ψ；Γ├Ｐ≒θＱ、Ｐ├→＊（Ｈｐ，Ｒｐ，ｈａｌｔ［σｐ］）．、及びＱ├→＊（Ｈｑ，Ｒｑ，ｈａｌｔ［σｑ］）．であれば、Ψ；Γ’├（Ｈｐ，Ｒｐ，ｈａｌｔ［σｐ］）．≒θ（Ｈｑ，Ｒｑ，ｈａｌｔ［σｑ］）．となるようなΓ’が存在する。
証明の概要：  誘導Ｐ├→＊（Ｈｐ，Ｒｐ，ｈａｌｔ［σｐ］）．のステップ数の一般化された帰納法による。ゼロ・ステップの基本的ケースは自明である。帰納法的ケースは、Ｉの最初の命令のケース解析によって行われる。
Ｉがｒａｉｓｅ  θ１▽ｗ１；Ｉ１の形式であるケースを考える。ここで、
【数８】
2008524726.tif 000010
である。操作的意味論及び型付け規則の定義によって、Ｐ├→Ｐ１である。ここで、Ｐ１＝（Ｈ，Ｒ，Ｉ１）θ１▽ｗ１、及びΨ；Γ├Ｐ１である。補助定理４によって、Ψ；Γ２├Ｐ２、Ｐ１├→＊Ｐ２、Γ≧θΓ２、及びΨ；Γ２├Ｐ１≒θＰ２となるようなΓ２及びＰ２＝（Ｈ２，Ｒ２，ｌｏｗｅｒ  ｗ１）θ１▽ｗ１が存在する。こうして、Ψ；├Ｈ≒θＨ２及びΨ；Γ２├Ｒ≒θＲ２である。
【０１０５】
[00128]操作的意味論によって、Ｐ２├→Ｐ３である。ここで、
【数９】
2008524726.tif 000011
及びＨ（ｌ１）＝ｃｏｄｅ［Δ］〈κ３〉Γ３．Ｉ３である。Ψ；Γ２├Ｐ２、Γ３⊆Γ２、及びΨ；Γ３├Ｐ３．の型付け誘導の反転によって、Ψ；Γ３├Ｒ≒θＲ２となる。Ｐの最初の命令がｒａｉｓｅ  θ１▽ｗ１；Ｉ１であるとき、Ψ；Γ├Ｐの型付け誘導の反転によって、κ３＝κとなる。
【０１０６】
[00129]同様の論法によって、Ｑ├→＊Ｑ３である。ここで、Ｑ３＝（Ｈ’２，Ｒ’２，Ｉ３）κ３、Ψ├Ｈ≒θＨ’２、Ψ；Γ３├Ｒ≒θＲ’２、及びΨ；Γ３├Ｑ３である。同値関係の推移によって、Ψ├Ｈ２≒θＨ’２、及びΨ；Γ３├Ｒ２≒θＲ’２である。こうして、Ψ；Γ├Ｐ３≒θＱ３となる。こうして、ケースは帰納法の仮定に従う。
【０１０７】
[00130]全ての他のケースは、ステップの後で低いままである。補助定理５によって、次のステップの２つの実行は同値であり、良好に型付けされる。こうして、これらのケースの証明は帰納法の仮定に従う。
【０１０８】
（機密性のためのコンパイル認証）
[00131]上記の非干渉定理は、メモリの再命名及び第１級コード・ポインタが存在するときでも、良好に型付けされたＴＡＬＣプログラムが情報フローポリシーを満足させることを保証する。下記は、ＴＡＬＣがコンパイル認証の目標としてどのように役立つかを説明する（図１７Ａ、図１７Ｂ、及び図１７Ｃ）。
【０１０９】
[00132]現実の言語のコンパイル認証は、典型的には、ＣＰＳ及び終結変換、ヒープ割り振り、及びコード生成を含む変換の複雑なシーケンスを含む。図２の簡単なセキュリティ型システムが原始言語として選ばれる。これは簡明な呈示を可能にするが、それでも従来の命令及びメカニズム（例えば、手続き呼び出しのスタック規約）からセキュリティコンテキスト演算ｒａｉｓｅ及びｌｏｗｅｒの分離を例証するのに十分である。
【０１１０】
[00133]図２の低・高セキュリティ階層は、２つの要素、即ち⊥及びＴから成る簡単な格子を定義する。下記において、ＴＡＬＣにおけるソース型ｔの変換、即ち、｜ｌｏｗ｜≡ｉｎｔ⊥及び｜ｈｉｇｈ｜≡ｉｎｔＴを表すため、｜ｔ｜が使用される。手続き型も、次のように原始言語からＴＡＬＣへ変換される。
｜〈ｐｃ〉（ｔ１，．．．，ｔｎ）→ｖｏｉｄ｜＝（∀［Δ］．〈κ〉｛ｓｐ：Σ｝）⊥
ここで、
【数１０】
2008524726.tif 000012
及びΣ＝（∀｜Δ｜．〈κ〉｛ｓｐ：ρ｝）⊥：：〈｜ｔ１｜〉⊥：：．．．：：〈｜ｔｎ｜〉⊥：：ρ
【０１１１】
[00134]この手続き型変換は、呼び出し側が、戻りポインタ及び引数の位置（原始言語の参照による呼び出し意味論を実現する）をスタックへプッシュし、被呼び出し側が、戻りのときに現在のスタック・フレームの割り振りを解く呼び出し規約を想定する。スタック型Σは変数ρを参照する。なぜなら、現在のスタック・フレームが期待される限り、異なるスタックのもとで手続きが呼び出されるかも知れないからである。ｐｃが低であれば、セキュリティコンテキストκは空であり、ｐｃが高であれば、Ｔ▽αである。ポストドミネータ変数αが使用される理由は、異なるポストドミネータを有するセキュリティコンテキストの中で手続きが呼び出されるかも知れないからである。型環境Δは、単に全ての必要な型変数を収集する。
【０１１２】
[00135]プログラム変換は、├Ｈ０：Ψ０を満足させてソースプログラムの全ての変数及び手続きについてエントリを含むヒープＨ０及びヒープ型Ψ０でスタートする。Φ（ｖ）＝ｔである任意のソース変数ｖについて、Ψ０（ｌｖ）＝〈｜ｔ｜〉⊥となるような位置ｌｖがヒープの中に存在する。Φ（ｆ）＝＜ｐｃ＞（ｔ１，．．．，ｔｎ）→ｖｏｉｄである任意のソース手続きｆについて、Ψ０（ｌｆ）＝｜＜ｐｃ＞（ｔ１，．．．，ｔｎ）→ｖｏｉｄ｜となるような位置ｌｆがヒープの中に存在する。Φ〜Ψ０は、この対応を示すために使用される。
【０１１３】
[00136]一実施形態において、上記のヒープΨ０は、手続きについてダミー・スロットで構成可能である。即ち、その中のコードは、単純にそれ自身へジャンプする。これは初期ヒープを型付けして型保存証明を容易にするのに十分である。それは全てのソース手続きについて位置を作り出し、実際のコードの変換がそれらを参照することを可能にする。
【０１１４】
[00137]変換の詳細は、ソースプログラムの型付け誘導の構造に基づいて図１７Ａ、図１７Ｂ、及び図１７Ｃで与えられる。どの変換規則が適用されるかは、ソース構造（プログラム、手続き、又はコマンド）を検査するために使用された最後の型付け規則によって判定される。発明者らは、ＴＤを使用して、（可能性として複数の）型付け誘導を表す。
【０１１５】
[00138]形式
【数１１】
2008524726.tif 000013
の式変換は、図１７Ａで定義される。命令ベクトル
【数１２】
2008524726.tif 000014
はＥの値を計算し、結果はレジスタｒの中に置かれる。グローバル変数については、値は、その対応するヒープ・ラベルを使用してヒープからロードされる。手続き引数については、実際のエンティティの位置がスタックからロードされ、次に値がヒープからロードされる。
【０１１６】
[00139]図１７Ｂにおいて、プログラムを変換するとき（規則［ＴＲＰ１］）、全ての手続き宣言が変換され、プログラムの終了点として停止コードを付加し、主コマンドを変換するように進行する。結果のトリプルは、更新されたヒープ型、ヒープ、及びプログラムの開始点へ導く開始ラベルｌを含む。手続き変換（規則［ＴＲＦ１］）は、呼び出し規約部分に注意を払う。それは戻りポインタをロードするエピローグコードを付加し、現在のスタック・フレームの割り振りを解き、制御を戻りポインタへ移転する。次に、それはコマンド変換を用いて手続き本体を変換し、手続き本体の終了点としてラベルをエピローグコードへ提供する。
【０１１７】
[00140]図１７Ｃは、次の形式、
【数１３】
2008524726.tif 000015
のコマンド変換を定義する。
【０１１８】
[00141]このコマンド変換は７つの引数を取る。即ち、コード・ヒープ型（Ψ）、コード・ヒープ（Ｈ）、Ｃを計算するための開始及び終了ラベル（ｌｓｔａｒｔ及びｌｅｎｄ）、型環境（Δ）、セキュリティコンテキスト（κ）、及びスタック型（Σ）である。それは拡張コード・ヒープ型（Ψ’）及びコード・ヒープ（Ｈ’）を生成する。驚くことではないが、この変換は複雑に見える。なぜなら、それは認証コンパイラの形式モデルを提供するからである。しかし、変換によって維持される幾つかの不変量が記憶されるならば、たどるのに容易である。即ち、
・  ＨはΨのもとで良好に型付けされ、全てのソース変数及び手続きについてエントリを含む。
・  Ψ及びＨは、ｌｅｎｄのラベルを有する継続コードを既に含む。
・  ｌｓｔａｒｔとラベルを付けられた新しいコードは、Ψ’及びＨ’の中に置かれる。
・  セキュリティコンテキストκはｐｃとマッチしなければならない。
・  コンパイルされているコマンドが手続き本体の中にあれば、スタック型Σは全ての手続き引数についてエントリを含む。
・  環境Δはκ及びΣの中に全ての自由型変数を含む。
【０１１９】
[00142]コマンド変換規則の大部分は、生成されたコード型のために単純にΔ、κ、及びΣを定位置に置き、更にそれらを部分構成要素の変換へ伝搬する。セキュリティコンテキストを非自明に取り扱う唯一の規則は規則［ＴＲＣ４］である。即ち、ソース・コマンドを型付けするため小前提規則が使用されるとき、変換はｒａｉｓｅとｌｏｗｅｒのペアに囲まれたコードを生成する。部分構成要素の変換は、新しい終了ラベルｌｌを有する更新ヒープの中で実行される。ｌｌにおけるコードはセキュリティコンテキストを回復し、制御を所与の終了ラベルｌ’へ移転する。部分構成要素の変換の後、コードが開始ラベルｌへ付加され、セキュリティコンテキストを期待レベルへ上げる。
【０１２０】
[00143]手続き呼び出し変換は、規則［ＴＲＣ７］として与えられる。それはスタック・フレームを割り振る「プロローグ」コードを作り出し、戻りポインタ及び引数をスタックへプッシュし、手続きラベルへジャンプする。注意すべきは、対応するエピローグコードが規則［ＴＲＦ１］で手続き宣言変換によって生成されることである。
【０１２１】
[00144]ｗｈｉｌｅループの変換も興味深い（規則［ＴＲＣ６］）。ループ本体を変換するとき、継続ブロックを準備する必要がある。これは偶然にもループ・テストのコードである。ｌのラベルを有するダミー・ブロックは、本体Ｃを変換するときの継続ブロックとして役立つように使用される。このブロックは、上記の不変量を維持するために導入される。それは変換の型保存証明を容易にする。ループ本体の変換の後、規則［ＴＲＣ６］の右側下方に示されるように、このダミー・ブロックは、ループ・テストを実現する実際のコードと置換される。
補助定理６（式変換）Φ〜Ψ、Φ├Ｅ：ｔ、
【数１４】
2008524726.tif 000016
及びΨ；Δ；｛ｒ：｜ｔ｜，ｓｐ：Σ｝；κ├Ｉであれば、
【数１５】
2008524726.tif 000017
である。
補助定理７（コマンド変換）Φ〜Ψ、Φ；［ｐｃ］├Ｃ、
【数１６】
2008524726.tif 000018
、Ψ（ｌｅｎｄ）＝（∀［Δ］．〈κ〉｛ｓｐ：Σ｝）⊥、ＳＬ（κ）＝｜ｐｃ｜、├Ｈ：Ψであれば、Φ〜Ψ、├Ｈ’：Ψ’、及びΨ’；Δ├ｌｓｔａｒｔ：（∀［Δ］．〈κ〉｛ｓｐ：Σ｝）⊥である。
【０１２２】
[00145]上記の２つの補助定理の証明は、変換の誘導における構造帰納法によって直接的である。手続き変換の型保存は、規則［ＴＲＦ１］に基づいて補助定理７から誘導可能である。次に、プログラム変換の型保存が規則［ＴＲＰ１］に基づいて続く。
補助定理８（手続き変換）Φ〜Ψ、Φ├Ｆ、├Ｈ：Ψ、
【数１７】
2008524726.tif 000019
であれば、Φ〜Ψ’及び├Ｈ’：Ψ’である。
定理２（プログラム変換）Φ〜Ψ０、Φ├Ｐ、├Ｈ０：Ψ０、
【数１８】
2008524726.tif 000020
であれば、Φ〜Ψ’及びΨ；｛ｓｐ：ｎｉｌ｝├（Ｈ，｛ｓｐ：ｎｉｌ｝，ｊｍｐ  ｌ）．である。
【０１２３】
（拡張及び代替）
[00146]直交的特徴：  上記の説明において、ＴＡＬＣは言語特徴の最小セットに焦点を当てている。代替の実施形態において、ＴＡＬで見られる多相性の存在する型は直交的であり、ほとんど困難なしに導入可能である。更に、ＴＡＬＣはＴＡＬと互換性を有するから、ＴＡＬ族の他の特徴に順応することもできる。例えば、別名型は、より正確な別名解析を提供し、全てのポインタを潜在的別名と考える現在の保守的アプローチを改善する。下記において、更に、単集合型の使用を説明する。
【０１２４】
[00147]セキュリティ多相性：  ＴＡＬＣはセキュリティコンテキストθ▽ｗに依存して現在のセキュリティレベルθ及びその終了点ｗを識別する。それはセキュリティに関して単相性である。なぜなら、コード・ブロックのセキュリティコンテキストは固定されているからである。実際には、セキュリティ多相性コードも有用であり得る。
【０１２５】
[00148]図１８は、１つの例を与える。関数ｄｏｕｂｌｅは、低又は高の入力で呼び出し可能である。入力のセキュリティレベルがコンテキストとマッチするだけで、コンテキストでｄｏｕｂｌｅを呼び出すことは安全である。多相性ＴＡＬＣのような型システムにおいて、型（∀［θ，α］．〈θ▽α〉｛ｒ１：ｉｎｔθ，ｒ０：（∀[]．〈θ▽α〉｛ｒ１：ｉｎｔθ｝）⊥｝）⊥をｄｏｕｂｌｅに与えることができる。この場合、ｒ１は引数レジスタであり、ｒ０は戻りポインタを記憶し、メタ変数θは変数として再使用される。
【０１２６】
[00149]この種の多相性をサポートすることは直接的である。実際、必要な構造の大部分は、ＴＡＬＣに既に存在する。発明者らは、そのような多相性が追加の洞察力を与えることなく呈示を複雑にするという単純な理由によって、それを省略した。しかし、そのような多相性の表現力は、依然として制限される。ラベルαはインスタンス化されるまで未知であるから、ｄｏｕｂｌｅのコードはαについて知識を有しない。こうして、セキュリティコンテキストθ▽α
は、ｄｏｕｂｌｅ本体の中で解放され得ない。
【０１２７】
[00150]多相性関数の中で、どうしてセキュリティコンテキストの解放が望まれるのかは明らかでない。実際、呼び出し側からの対称的なｒａｉｓｅ及びｌｏｗｅｒ演算によって、安全領域の内部に関数呼び出しを包むことは常に可能である。しかし、セキュリティコンテキストの非対称的解放は、ときには、最適化認証のために望ましいかも知れない。例えば、図１８において、ｄｏｕｂｌｅは高条件文の本体の最後の命令文として呼び出される。この場合、ｄｏｕｂｌｅが戻るときセキュリティコンテキストを直接解放することは、呼び出し側から余分なｌｏｗｅｒ演算を除去するであろう。そのような解放は、ｌｏｗｅｒが小さな値（特に、レジスタ）に作用することを必要とする。なぜなら、戻りラベルは静的でなく、レジスタを介して渡されるからである。
【０１２８】
[00151]そのような強力なｌｏｗｅｒ演算をサポートするには、単集合型及び交差型を必要とするかも知れない。例えば、セキュリティコンテキストを自動的に解放するｄｏｕｂｌｅ関数は、
【数１９】
2008524726.tif 000021
の型を有することができる。
【０１２９】
[00152]関数の終わりにおいて、命令ｌｏｗｅｒ  ｒ０はセキュリティコンテキストを解放し、制御を戻りコードへ移転する。型検査について、単集合整数型ｓｉｎｔ（α）は、セキュリティコンテキストの中でラベルを有するレジスタｒ０とマッチし、コード型は、戻りコードへの制御フローが安全であることを確保する。
【０１３０】
[00153]完全消去：  上記で説明した強力な型構造と共に、ｌｏｗｅｒ演算について完全消去を達成することができる。ｌｏｗｅｒを命令として取り扱う代わりに、それを小さな値への変換として取り扱うことができる。これは、精神において、ＴＡＬの存在型のｐａｃｋ演算と同じである。そのようなｌｏｗｅｒ変換は、現在のセキュリティコンテキストと目標ラベルのセキュリティレベルとの間のギャップを橋渡しする。こうして、実際の制御フローの移転は、従来のジャンプ命令（例えば、ｊｍｐ（ｌｏｗｅｒ  ｒ０））で完了される。更に、依存型を有しないｌｏｗｅｒについても完全消去を達成することができる。アイデアは、ジャンプ命令を直接ジャンプと間接ジャンプに分離することである。これも実計算機のアーキテクチャと首尾一貫する。ｌｏｗｅｒ演算は、ｐａｃｋと同じように、ワード値（終局的には直接ラベル）を変換する。下げられたラベルは、パックされた値と同じく、直接ジャンプのオペランドとして役立つ。他方、間接ジャンプは通常の小さな値を取る。これは、コンパイル認証について十分に表現的であるが、前述した最適化認証には十分でないかも知れない。
【０１３１】
（例示的形態電話）
[00154]図１９は、携帯電話の一実施形態のブロック図である。図１９を参照すると、携帯電話１９１０は、アンテナ１９１１、無線周波数トランシーバ（ＲＦユニット）１９１２、モデム１９１３、信号処理ユニット１９１４、制御ユニット１９１５、外部インタフェース・ユニット（外部Ｉ／Ｆ）１９１６、スピーカ（ＳＰ）１９１７、マイクロホン（ＭＩＣ）１９１８、ディスプレイ・ユニット１９１９、演算ユニット１９２０、及びメモリ１９２１を含む。これらの構成要素及び動作は当技術分野で周知である。
【０１３２】
[00155]一実施形態において、制御ユニット１９１５はＣＰＵ（中央処理ユニット）を含む。ＣＰＵはメモリ１９２１と協力して、前述した演算を実行する。
【０１３３】
（例示的コンピュータ・システム）
[00156]図２０は、前述した演算の１つ以上を実行する例示的コンピュータ・システムのブロック図である。図２０を参照すると、コンピュータ・システム２０００は、例示的なクライアント又はサーバ・コンピュータ・システムを構成してよい。そのようなクライアントは、他のデバイス、例えば、移動デバイスの一部分であってよい。
【０１３４】
[00157]コンピュータ・システム２０００は、情報を通信するための通信メカニズム又はバス２０１１、及び情報を処理するためバス２０１１と結合されたプロセッサ２０１２を備える。プロセッサ２０１２は、マイクロプロセッサを含むが、マイクロプロセッサ、例えば、Ｐｅｎｔｉｕｍ（商標）、ＰｏｗｅｒＰＣ（商標）などに限定されない。
【０１３５】
[00158]システム２０００は、更に、情報及びプロセッサ２０１２によって実行される命令を記憶するため、バス２０１１に結合されたランダム・アクセス・メモリ（ＲＡＭ）又は他の動的記憶デバイス２００４（メイン・メモリと呼ばれる）を備える。メイン・メモリ２００４は、更に、命令がプロセッサ２０１２によって実行される間、一時変数又は他の中間情報を記憶するために使用されてよい。
【０１３６】
[00159]コンピュータ・システム２０００は、更に、プロセッサ２０１２のために静的情報及び命令を記憶するためバス２０１１へ結合された読み出し専用メモリ（ＲＯＭ）及び／又は他の静的記憶デバイス２００６、及びデータ記憶デバイス２００７、例えば、磁気ディスク又は光ディスク及びその対応するディスク・ドライブを含む。データ記憶デバイス２００７は、情報及び命令を記憶するためバス２０１１へ結合される。
【０１３７】
[00160]コンピュータ・システム２０００は、更に、情報をコンピュータ・ユーザへ表示するため、バス２０１１へ結合されたディスプレイ・デバイス２０２１、例えば、陰極線管（ＣＲＴ）又は液晶ディスプレイ（ＬＣＤ）へ結合されてよい。英数字及び他のキーを含む英数字入力デバイス２０２２も、プロセッサ２０１２へ情報及びコマンド選択を通信するためバス２０１１へ結合されてよい。追加のユーザ入力デバイスは、カーソル・コントロール２０２３、例えば、マウス、トラックボール、トラックパッド、スタイラス、又はカーソル方向キーである。これらは、プロセッサ２０１２へ方向情報及びコマンド選択を通信し、またディスプレイ２０２１の上でカーソル移動を制御するため、バス２０１１へ結合される。
【０１３８】
[00161]バス２０１１へ結合されてもよい他のデバイスは、ハードコピー・デバイス２０２４である。デバイス２０２４は、媒体、例えば、紙、フィルム、又は類似した種類の媒体の上に情報をマークするために使用されてもよい。バス２０１１へ結合されてもよい他のデバイスは、電話又はハンドヘルド・パーム・デバイスへ通信するための有線／無線通信機能２０２５である。注意すべきは、システム２０００及び関連ハードウェアの構成要素の任意のもの、又は全部が、本発明で使用されてもよいことである。しかし、コンピュータ・システムの他の構成は、デバイスの幾つか又は全部を含んでもよいことを理解することができる。
【０１３９】
[00162]これまでの説明を読んだ後の当業者にとって、本発明の多くの代替及び修正は疑いもなく明らかであろうが、理解すべきは、例を介して図示及び説明された特定の実施形態は、如何なる意味でも限定と考えてはならないことである。したがって、様々な実施形態の詳細への参照は、特許請求の範囲を限定する意図を有しない。特許請求の範囲は、それら自身、発明に必須であると考えられる特徴のみを列記している。
【図面の簡単な説明】
【０１４０】
【図１Ａ】情報フロー強制のプロセスの流れ図である。
【図１Ｂ】図１Ａの情報フロー強制が実現される環境を示す図である。
【図２】原始言語レベルでの簡単なセキュリティシステムを示す図である。
【図３】幾つかのプログラム構造の流れ図である。
【図４】再命名による情報フローの例を示す図である。
【図５】コード・ポインタによる例示的情報フローを示す図である。
【図６】分岐を有しない例示的コンテキスト強制型変換を示す図である。
【図７Ａ】低レベル検証の利点を示す図である。
【図７Ｂ】低レベル検証の利点を示す図である。
【図８】セキュリティレベルを管理する流れ図である。
【図９】非干渉を確立する流れ図である。
【図１０】プログラムの検証の流れ図である。
【図１１】命令シーケンスの検証の流れ図である。
【図１２】ＴＡＬＣの構文を示す図である。
【図１３】ＴＡＬＣの操作的意味論を示す図である。
【図１４】ＴＡＬＣ型付け判断を示す図である。
【図１５】非命令のＴＡＬＣ型付け規則を示す図である。
【図１６】ＴＡＬＣ命令の型付け規則を示す図である。
【図１７Ａ】式変換（コンパイル認証の一部分）を示す図である。
【図１７Ｂ】プログラム及び手続き宣言変換（コンパイル認証の一部分）を示す図である。
【図１７Ｃ１】コマンド変換（コンパイル認証の一部分）を示す図である。
【図１７Ｃ２】図１７Ｃ１から続く図である。
【図１８】セキュリティ多相性関数の例を示す図である。
【図１９】移動デバイスの一実施形態のブロック図である。
【図２０】コンピュータ・システムの一実施形態のブロック図である。
【図１Ａ】
2008524726.tif 000022
【図１Ｂ】
2008524726.tif 000023
【図２】
2008524726.tif 000024
【図３】
2008524726.tif 000025
【図４】
2008524726.tif 000026
【図５】
2008524726.tif 000027
【図６】
2008524726.tif 000028
【図７Ａ】
2008524726.tif 000029
【図７Ｂ】
2008524726.tif 000030
【図８】
2008524726.tif 000031
【図９】
2008524726.tif 000032
【図１０】
2008524726.tif 000033
【図１１Ａ】
2008524726.tif 000034
【図１１Ｂ】
2008524726.tif 000035
【図１２】
2008524726.tif 000036
【図１３】
2008524726.tif 000037
【図１４】
2008524726.tif 000038
【図１５】
2008524726.tif 000039
【図１６】
2008524726.tif 000040
【図１７Ａ】
2008524726.tif 000041
【図１７Ｂ】
2008524726.tif 000042
【図１７Ｃ１】
2008524726.tif 000043
【図１７Ｃ２】
2008524726.tif 000044
【図１８】
2008524726.tif 000045
【図１９】
2008524726.tif 000046
【図２０】
2008524726.tif 000047
【手続補正書】
【提出日】平成19年7月24日(2007.7.24)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
セキュアに型付けされたネイティブコードを受け取る受け取りステップと、
セキュリティポリシーに基づいて、前記セキュアに型付けされたネイティブコードに対して情報フローに関する検証を実行する検証ステップと、
を備える、方法。
【請求項２】
前記セキュアに型付けされたネイティブコードが、注釈を有するアセンブリコードを含む、請求項１に記載の方法。
【請求項３】
前記注釈が、所定の情報に基づく２つの実行経路が出会う前記コードの領域の始まり及び終わりをマークする演算を含む、請求項２に記載の方法。
【請求項４】
前記コードから前記注釈を除去する除去ステップと、
前記コードが前記セキュリティポリシーに違反しないと前記検証ステップが判定する場合に、前記コードを実行する実行ステップと、
を更に備える、請求項２に記載の方法。
【請求項５】
デバイスが前記コードを実行する前に、前記検証ステップが前記デバイス上で行われる、請求項１に記載の方法。
【請求項６】
前記検証ステップが、前記コードの振る舞いを静的に検査し前記コードが前記セキュリティポリシーに違反しないかどうかを判定する検査工程を含む、請求項１に記載の方法。
【請求項７】
前記コードが実行されたとき、該コードを実行するデバイスから、識別された型の情報を該コードが流出させない場合に、該コードが前記セキュリティポリシーに違反しない、請求項６に記載の方法。
【請求項８】
前記コードが前記セキュリティポリシーに違反しないと前記検証ステップが判定する場合に、前記コードを実行する実行ステップを更に備える、請求項１に記載の方法。
【請求項９】
前記コードの受け取りステップが、前記コードのダウンロードを含む、請求項１に記載の方法。
【請求項１０】
セキュアに型付けされたネイティブコードの受け取りステップが、セキュリティ型保存変換を受けたアセンブリコードの受け取ることを含み、
前記セキュリティ型保存変換が、アセンブリコードに型情報によって注釈することを含み、
更に、前記検証ステップが、前記アセンブリコードの実行時の制御のもとで起こる情報フローを前記セキュリティポリシーに関して静的に検査することによって、前記型情報を検証することを含む、請求項１に記載の方法。
【請求項１１】
システムによって実行されるときに該システムに方法を実行させる命令を記憶した１つ以上の記録可能媒体を有する製造品であって、
前記方法が、
セキュアに型付けされたネイティブコードを受け取る受け取りステップと、
セキュリティポリシーに基づいて、前記セキュアに型付けされたネイティブコードに対して情報フローに関する検証を実行する検証ステップと、
を備える、製造品。
【請求項１２】
前記セキュアに型付けされたネイティブコードが、注釈を有するアセンブリコードを含む、請求項１１に記載の製造品。
【請求項１３】
前記注釈が、所定の情報に基づく２つの実行経路が出会う前記コードの領域の始まり及び終わりをマークする演算を含む、請求項１２に記載の製造品。
【請求項１４】
前記方法が、
前記コードから前記注釈を除去する除去ステップと、
前記コードが前記セキュリティポリシーに違反しないと前記検証ステップが判定する場合に、前記コードを実行するする実行ステップと、
を更に備える、請求項１２に記載の製造品。
【請求項１５】
前記検証ステップが、前記コードの振る舞いを静的に検査し、前記コードが前記セキュリティポリシーに違反しないかどうかを判定する検査工程を含む、請求項１１に記載の製造品。
【請求項１６】
前記コードが実行されたとき、該コードを実行するデバイスから、識別された型の情報を該コードが流出させない場合に、該コードが前記セキュリティポリシーに違反しない、請求項１４に記載の製造品。
【請求項１７】
前記コードが前記セキュリティポリシーに違反しないと前記検証ステップが判定する場合に、前記コードを実行する実行ステップを前記方法が更に含む、請求項１１に記載の製造品。
【請求項１８】
前記コードの受け取りステップが、前記コードのダウンロードを含む、請求項１１に記載の製造品。
【請求項１９】
セキュアに型付けされたネイティブコードの受け取りステップが、セキュリティ型保存変換を受けたアセンブリコードを受け取ることを含み、
前記セキュリティ型保存変換が、アセンブリコードに型情報によって注釈することを含み、
更に、前記検証ステップが、前記アセンブリコードの実行時の制御のもとで起こる情報フローを前記セキュリティポリシーに関して静的に検査することによって、前記型情報を検証することを含む、請求項１１に記載の製造品。
【請求項２０】
注釈されたアセンブリコード、検証モジュール及びコード修正モジュールを記憶するメモリと、
前記検証モジュールを実行し、セキュリティポリシーに基づいて、前記注釈されたコードに対して情報フローに関する検証を実行するプロセッサと、
を備える装置。
【請求項２１】
前記注釈されたアセンブリコードの中の注釈が、所定の情報に基づく２つの実行経路が出会う前記コードの領域の始まり及び終わりをマークする演算を含む、請求項２０に記載の装置。
【請求項２２】
前記プロセッサが、前記コードの振る舞いを静的に検査し、前記コードが前記セキュリティポリシーに違反しないかどうかを判定することによって、検証を実行する、請求項２０に記載の装置。
【請求項２３】
前記コードが実行されたとき、該コードを実行するデバイスから、識別された型の情報を該コードが流出させない場合に、該コードが前記セキュリティポリシーに違反しない、請求項２２に記載の装置。
【請求項２４】
前記プロセッサが、前記注釈を除去し、前記コードがセキュリティポリシーに違反しないと検証中に判定した後、前記コードを実行する、請求項２０に記載の装置。
【請求項２５】
前記プロセッサが、前記アセンブリコードの実行時の制御のもとで起こる情報フローを前記セキュリティポリシーに関して静的に検査することによって、型情報による検証を実行する、請求項２０に記載の装置。
【請求項２６】
無線通信を送受信するための無線通信ハードウェア及びソフトウェアを更に備える、請求項２０に記載の装置。
【請求項２７】
アセンブリコード上でセキュリティ型保存変換を実行するステップであって、
メモリ、スタック、及びレジスタの内容にセキュリティレベルによって注釈する工程と、
機密情報に基づく２つの実行経路が出会う前記アセンブリコードのセキュリティ領域の始まり及び終わりをマークする演算を前記アセンブリコードに付加することによって、注釈を有する前記アセンブリコードのソースレベル構造を再構築する工程と、
を含むステップと、
実行されたときの前記アセンブリコードから生じる情報フローについてコンパイルを認証するステップと、
前記セキュアに型付けされたアセンブリコードをネットワークへ送るステップと、
を備える方法。
【国際調査報告】
2008524726.tif 000048
2008524726.tif 000049
2008524726.tif 000050