论文部分内容阅读
由于BLP模型的基本安全公理不能完全证明模型的安全性，因此，在分析BLP改进模型的安全性时，如果模型的安全策略十分复杂而不能直接判断其安全性，或者模型由于改变了安全属性定义等而动摇了基本安全公理的推理基础时，应从其他角度证明改进模型的安全性．利用基于系统动作的不干扰模型，从信息流的角度给出一种对多级安全模型的形式化分析方法，为多级安全模型的安全性验证提供了一种新的途径．该不干扰模型把不干扰关系扩展到系统动作之间，提出了新的单步展开定理，可描述多级安全模型中的动态策略．通过以ABLP与DBLP模型为实例进行