对一类多级安全模型安全性的形式化分析

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

Formal Safety Analysis of a Class of Multilevel Security Models

How to improve the traditional BLP model to make it more applicable is one of the major problems to be solved in the design of secure operating systems. There are several improved BLP models that have been applied to real systems. However, the security property of these models must be verified and assured, if not the models will lose its function as a security model. In this paper, the essence of multilevel security (MLS) is analyzed and the security theorem applicable for improved BLP models involved in multi-level objects is proposed for the first time. Then the effect of security invariants on the definition of system security is analyzed and emphasized. The assertion that the security invariant of various MLS models must be verified to be consistent with the MLS security policy is also introduced. To justify the assertion, an improved BLP model, DBLP, is analyzed as an example. To enhance the clarity, the Z formal language is used to specify the system and the theorem prover Z/EVES used to analyze and verify whole specification and relevant theorems. The verification result shows that the invariant of DBLP model does not satisfy the security theorem introduced in this paper, and therefore the DBLP is insecure. The research provides a way of specification and verification for the analysis of various improved BLP models. In addition, it presents a theoretical foundation for selection of MLS models.