论文部分内容阅读
深入分析了MLS的核心思想，给出了MLS在包含多级客体的系统中的表述形式，分析了安全不变式（invariant）在系统安全定义中的作用．为了保证模型的安全，必须验证模型的不变式满足MLS策略．为了说明不变式验证的重要性，借助Z语言和形式验证工具Z／EVES分析了一个改进的BLP模型——DBLP模型．分析表明，DBLP模型的不变式不满足MLS策略的要求，因此是不安全的．这项研究为分析各种改进BLP模型的安全性提供了理论依据和形式化规范与验证的方法．