非干渉（セキュリティ）

非干渉は、1982 年に Goguen と Meseguer によって最初に説明され、1984 年にさらに開発された、 厳密な多層セキュリティポリシー モデルです。

簡単に言えば、コンピューターは入力と出力を持つ機械としてモデル化されます。入力と出力は、低(低感度、高度に機密ではない) または高(機密、許可されていない個人が閲覧できない) のいずれかに分類されます。高レベルの入力が何であるかに関係なく、低レベルの入力のシーケンスが同じ低レベルの出力を生成する場合にのみ、コンピューターは非干渉性を持ちます。

つまり、低い (承認されていない) ユーザーがマシンで作業している場合、高い (承認された) ユーザーが機密データを操作しているかどうかに関係なく、マシンはまったく同じ方法で (低い出力に対して) 応答します。低いユーザーは、高いユーザーのアクティビティ (もしあれば) に関する 情報を取得できません。

をメモリ構成とし、 と をそれぞれメモリの低位部分と高位部分への投影とします。をメモリ構成の低位部分を比較する関数とします。つまり、の場合に限ります。をメモリ構成で開始し、メモリ構成で終了するプログラムの実行とします。 ${\displaystyle M}$${\displaystyle M_{\text{L}}}$${\displaystyle M_{H}}$${\displaystyle M}$${\displaystyle {=_{\text{L}}}}$${\displaystyle M\ {=_{\text{L}}}\ M^{\prime }}$${\displaystyle M_{\text{L}}=M_{\text{L}}^{\prime}}$${\displaystyle (P,M)\rightarrow ^{*}M^{\prime }}$${\displaystyle P}$${\displaystyle M}$${\displaystyle M^{\prime}}$

決定論的プログラムにおける非干渉の定義は以下の通りである: ^[1]${\displaystyle P}$

${\displaystyle {\begin{array}{rrl}\forall M_{1},M_{2}:\;&M_{1}\ {=_{\text{L}}}\ M_{2}&\land \\&(P,M_{1})\rightarrow ^{*}M_{1}^{\prime }&\land \\&(P,M_{2})\rightarrow ^{*}M_{2}^{\prime }&\Rightarrow \\&M_{1}^{\prime }\ {=_{\text{L}}}\ M_{2}^{\prime }\end{array}}}$

これは非常に厳格なポリシーであり、秘密チャネルを備えたコンピュータ システムは、たとえばBell-LaPadula モデルに準拠しているかもしれませんが、非干渉には準拠しません。逆の場合も当てはまります (システムがラベル付きのファイルを持っているなど、妥当な条件下で)。ただし、以下に示す「起動時に機密情報がない」という例外は除きます。ただし、非干渉は非推論可能性よりも強力であることが示されています。

この厳密さには代償が伴います。この特性を持つコンピュータ システムを作るのは非常に困難です。このポリシーに準拠していることが検証されている市販製品は 1 つか 2 つだけかもしれませんが、これらは基本的にスイッチと一方向の情報フィルターと同じくらい単純なものになります (ただし、これらを調整して有用な動作を提供することもできます)。

コンピュータに (time = 0 の時点で) 何らかの高 (つまり機密) 情報が含まれている場合、または低ユーザーが time = 0 以降に高情報を作成した場合 (多くのコンピュータ セキュリティ ポリシーで許可されているいわゆる「書き込み」)、コンピュータはすべての高情報を合法的に低ユーザーに漏洩することができ、非干渉ポリシーに準拠していると言えます。低ユーザーは高ユーザーのアクティビティについて何も知ることはできませんが、高ユーザーのアクション以外の手段で作成された高情報については知ることができます (von Oheimb、2004)。

Bell-LaPadula モデルに準拠するコンピュータ システムは、明示的に「リードアップ」を禁止しているため、この問題に悩まされることはありません。したがって、非干渉に準拠するコンピュータ システムは、必ずしも Bell-LaPadula モデルに準拠するわけではありません。したがって、Bell-LaPadula モデルと非干渉モデルは比較できません。Bell-LaPadula モデルはリードアップに関して厳格であり、非干渉モデルは隠れチャネルに関して厳格です。

一部の合法的なマルチレベル セキュリティ活動では、個々のデータ レコード (個人情報など) を機密として扱いますが、データの統計機能 (平均、合計数など) はより広範囲に公開できます。これは、非干渉マシンでは実現できません。

非干渉性は、システムがさまざまな低入力に対する観測可能な出力から高入力に関する情報を一切漏らさないことを要求します。しかし、非干渉性を達成することは、実用システムの多くでは不可能であることが多く、さらに望ましくない場合もあります。プログラムは、秘密の入力に依存する情報を漏らす必要があります。たとえば、ユーザーが正しい資格情報を入力した場合と間違った資格情報を入力した場合では、出力が異なる必要があります。シャノンエントロピー、推測エントロピー、最小エントロピーは、非干渉性を一般化する定量的情報漏洩の一般的な概念です。^[2]

• McLean, John (1994)。「セキュリティ モデル」。ソフトウェア エンジニアリング百科事典。第 2 巻。ニューヨーク: John Wiley & Sons, Inc.、pp. 1136–1145。

• von Oheimb, David (2004)。「情報フロー制御の再考: 非影響 = 非干渉 + 非漏洩」。欧州コンピュータ セキュリティ研究シンポジウム (ESORICS)。ソフィア アンティポリス、フランス: LNCS、Springer-Verlag。pp. 225–243。