ベル・ラパドゥラモデル
ベル・ラパドゥラモデルは、データの完全性を保護するためのルールを記述するBiba Integrity Modelとは対照的に、データの機密性と機密 情報への制御されたアクセスに焦点を当てている。この正式なモデルでは、情報システムのエンティティはサブジェクトとオブジェクトに分割される。「 安全な状態 」の概念が定義されており、各状態遷移は安全な状態から安全な状態に移行することによりセキュリティを維持し、それによりシステムがモデルのセキュリティ目標を満たしていることを帰納的に証明する。ベル・ラパドゥラモデルは、コンピューターシステムで許可される状態のセットを持つ状態マシンの概念に基づいて構築されている。ある状態から別の状態への遷移は、遷移関数によって定義される。
システム状態は、オブジェクトに対するサブジェクトの許可されたアクセスモードのみがセキュリティポリシーに従っている場合、「セキュア」であると定義される。特定のアクセスモードが許可されているかどうかを判断するには、対象のクリアランスをオブジェクトの分類(より正確には、セキュリティレベルを構成する分類とコンパートメントの組み合わせ)と比較して、対象が許可されているかどうかを判断します特定のアクセスモード用。クリアランス/分類スキームは、格子の観点から表現される。このモデルでは、1つの任意アクセス制御 (DAC)ルールと2つの必須アクセス制御 (MAC)ルールを3つのセキュリティプロパティで定義する:
シンプルセキュリティプロパティは、特定のセキュリティレベルのサブジェクトがより高いセキュリティレベルのオブジェクトを読み取れないことを示している。