許可取得保護モデル

テイク・グラント保護モデルは、特定のルールに従う特定のコンピュータ システムの安全性を確立または反証するためにコンピュータ セキュリティの分野で使用される正式なモデルです。このモデルは、安全性の問題は一般には決定不可能であるものの、特定のシステムでは線形時間で決定可能であることを示しています。

このモデルは、システムを有向グラフとして表現します。有向グラフでは、頂点はサブジェクトまたはオブジェクトです。頂点間のエッジにはラベルが付けられ、ラベルはエッジのソースがデスティネーションに対して持つ権限を示します。モデルのすべてのインスタンスには、takeとgrantという 2 つの権限があります。これらは、グラフの許容される変更を記述するグラフ書き換えルールで特別な役割を果たします。

このようなルールは全部で 4 つあります。

• テイクルールは、サブジェクトが別のオブジェクトの権利を取得できるようにします（サブジェクトから始まるエッジを追加します）
• 許可ルールは、サブジェクトが別のオブジェクトに独自の権限を付与することを許可する（サブジェクトで終了するエッジを追加する）
• 作成ルールにより、サブジェクトは新しいオブジェクトを作成できます (サブジェクトから新しい頂点に頂点と辺を追加します)
• 削除ルールにより、サブジェクトは別のオブジェクトに対して持っている権限を削除できます（サブジェクトから始まるエッジを削除します）。

前提条件: ${\displaystyle take(o,p,r)}$

• 主語s はoに対して Take 権を持ちます。
• オブジェクトo はpに対して右r を持ちます。

前提条件: ${\displaystyle 付与(o,p,r)}$

• 対象s にはoに対する許可の権利があります。
• s はp上で右r を持ちます。

テイク・グラント保護モデルのルールを使用すると、権利の分配に関して、システムがどの状態に変化できるかを再現できます。したがって、特定の安全モデルに関して権利が漏洩する可能性があるかどうかを示すことができます。

• Lipton, Richard J. ; Snyder, Lawrence (1977). 「サブジェクトセキュリティを決定するための線形時間アルゴリズム」(PDF) . Journal of the ACM . 24 (3): 455–464. CiteSeerX  10.1.1.149.4807 . doi :10.1145/322017.322025.
• ビショップ、マット (2004)。『コンピュータセキュリティ：芸術と科学』Addison-Wesley。

• 図とサンプル問題
• 分析
• 技術レポート PCS-TR90-151 (NASA)