| 研究概要 |
アクセス行列における安全問題とは,ある実体に対するアクセス権限を、ある主体が持つことができるかを判定する問題である。残念ながら、安全問題は決定不能であり,決定可能となる場合でも,多くは単調システム(実体を消去したり,権限を取り消したりすることができない)のように,強い制約が課せられる。そのため我々は,動的な型付きアクセス行列モデルを研究している。このモデルでは,すべての実体に,動的に変更可能な型が割り当てられる。これにより、従来知られていなかった,非単調システムにおける安全問題の決定可能性を示すことができる。しかしながら、これらには、生成される実体の数が有限であるという制約があった。
そこで本研究では,このような制約を除くことを本年度の目標とした。このために、非単調システムで安全問題が決定可能な状況における,孤児の型があってはならないという制約に着目した。孤児の型とは、実体の型の親子関係を考えたときに、親の型が存在しない子の型のことである。そこで、アクセス制御を状態遷移機械によってモデル化したとき,孤児の型を持つコマンドは,任意の状態で適用できるために,実体の数は無限になる。すなわち、孤児の型を持つコマンドを含むような非単調システムで、安全問題が決定可能な場合があれば,実体の数を無限にすることができる。これを実現するために,状態遷移がcanonicalであるような場合(孤児の型のコマンドを最初に適用する)を考慮すれば十分であることを示し,実体の数に関する制約を外すことに成功した。現在,ここまでの結果を投稿準備中である。ただし、この結果は、まだ十分に一般的なものではない。そこで、次年度は,本年度の研究成果をさらに推し進め,安全問題が決定可能となるような,より一般的な非単調システムについて研究をする予定である。
|
