セキュリティ型システム

コンピュータサイエンスでは、型システムは、変数や関数など、コンピュータプログラムのさまざまなコンポーネントに型プロパティ（int、boolean、charなど）を割り当てるために使用される一連のルールを含む構文フレームワークとして説明できます。セキュリティ型システムは同様に機能しますが、情報フロー制御を通じてコン​​ピュータプログラムのセキュリティに主に焦点を当てています。したがって、プログラムのさまざまなコンポーネントには、セキュリティタイプまたはラベルが割り当てられます。このようなシステムの目的は、最終的に、特定のプログラムが型システムのルールに準拠し、非干渉性を満たしていることを検証できるようにすることです。セキュリティ型システムは、言語ベースのセキュリティの分野で使用される多くのセキュリティ手法の1つであり、情報フローと情報フローポリシーに密接に関連しています。

簡単に言えば、セキュリティ タイプのシステムは、プログラムに機密性または整合性の違反があるかどうかを検出するために使用できます。つまり、プログラマーは、プログラムが情報フロー ポリシーに準拠しているかどうかを検出したいのです。

ユーザー A と B の 2 人がいるとします。プログラムでは、次のセキュリティ クラス(SC) が導入されています。

• SC = {∅, {A}, {B}, {A,B}}ここで、∅は空集合です。

情報フロー ポリシーでは、情報のフローが許可される方向を定義する必要があります。これは、ポリシーが読み取り操作と書き込み操作のどちらを許可するかによって異なります。この例では、読み取り操作 (機密性)を考慮します。次のフローが許可されます。

• → = {({A}, {A}), ({B}, {B}), ({A,B}, {A,B}), ({A,B}, {A}), ({A,B}, {B}), ({A}, ∅), ({B}, ∅), ({A,B}, ∅)}

これはスーパーセット (⊇) として記述することもできます。言葉で言えば、情報はより厳格なレベルの機密性に向かって流れることが許可されます。組み合わせ演算子 (⊕) は、セキュリティ クラスが他のセキュリティ クラスに関して読み取り操作を実行する方法を表現できます。例:

• {A} ⊕ {A,B} = {A}{A}—と の両方から読み取ることができる唯一のセキュリティ クラスは{A,B}です{A}。
• {A} ⊕ {B} = ∅— も も、と の両方から読み取ることはできませ{A}ん。{B}{A}{B}

これは、セキュリティ クラス間の交差 (∩) として記述することもできます。

情報フロー ポリシーは、ハッセ図として表すことができます。ポリシーは格子でもあり、つまり、最大の下限と最小の上限を持ちます (セキュリティ クラス間の組み合わせは常に存在します)。整合性の場合、情報は反対方向に流れるため、ポリシーは反転されます。

ポリシーが確立されると、ソフトウェア開発者はプログラム コンポーネントにセキュリティ クラスを適用できます。セキュリティ型システムの使用は、通常、型システム ルールに従って情報フローの検証を実行できるコンパイラと組み合わせて行われます。簡単にするために、前のセクションで説明した情報フロー ポリシーと非常に単純なコンピュータ プログラムをデモンストレーションとして使用できます。単純なプログラムは、次の疑似コードで示されます。

if y{A} = 1 then x{A,B} := 0 else x{A,B} := 1

ここでは、セキュリティ クラス が割り当てられた変数 y に対して等価性チェックが行われます{A}。セキュリティ クラスが低い ( ) 変数 x は、このチェックの影響を受けます。これは、クラス からクラス に{A,B}情報が漏洩していることを意味し、機密性ポリシーに違反しています。この漏洩は、セキュリティ型システムによって検出される必要があります。 {A}{A,B}

セキュリティ型システムを設計するには、変数からセキュリティ型またはクラスへのマッピングを作成する関数 (セキュリティ環境とも呼ばれます) が必要です。この関数は Γ と呼ばれΓ(x) = τ、 はx変数、τはセキュリティ クラスまたは型です。セキュリティ クラスは、次の表記法を使用してプログラム コンポーネントに割り当てられます (「判断」とも呼ばれます)。

• 読み取り操作には次の方法で型が割り当てられますΓ ⊢ e : τ。
• 書き込み操作には、次の方法で型が割り当てられますΓ ⊢ S : τ cmd。
• 定数には任意の型を割り当てることができます。

プログラムを分解するには、次のボトムアップ表記法を使用できます。仮定₁ ... 仮定_n/結論⁠。プログラムが簡単な判断に分解され、それによって型を簡単に決定できるようになると、プログラムのそれほど重要でない部分の型を導出できます。各「分子」は個別に検討され、各ステートメントの型を調べて、定義された型システムの「ルール」に基づいて、「分母」に対して許可された型を導出できるかどうかが確認されます。

セキュリティ型システムの主要部分はルールです。ルールは、プログラムをどのように分解し、型検証をどのように実行するかを示します。このおもちゃのプログラムは、条件テストと 2 つの可能な変数割り当てで構成されています。これら 2 つのイベントのルールは次のように定義されています。

これを上で紹介した簡単なプログラムに適用すると、次のようになります。

型システムは、セキュリティ クラスの読み取り操作{A}が実行され、その後にそれほど厳密ではないセキュリティ クラスの 2 つの書き込み操作が続く2 行目でポリシー違反を検出します{A,B}。より形式化された用語で言えば、{A} ⋢ {A,B}, {A,B}(条件テストのルールから)、プログラムは「型指定不可」として分類されます。

セキュリティ型システムの健全性は、非公式には次のように定義できます。プログラムがP適切に型付けされている場合、P非干渉性を満たします。Volpano、Smith、Irvine は、非干渉の概念を使用して、標準的な (非インストルメント化) セマンティクスを備えた決定論的命令型プログラミング言語のセキュリティ型システムの健全性を初めて証明しました。^[1]

• Fred B. Schneider、Greg Morrisett、Robert Harper、「セキュリティに対する言語ベースのアプローチ」。
• Andrei Sabelfeld、Andrew C. Myers、「言語ベースの情報フロー セキュリティ」。