BLP改进模型的形式化描述及自动化验证

摘要

According to the《Information Security Technology--Security Techniques Requirement for Operating System》, formal security policy model is required in the development of access verification and protection level of security operating systems. Aiming at the situation, an improved BLP model which has multi-level security labels and security transition rules is proposed based on the traditional data confidentiality BLP model to satisfy the development of actual systems. The states, invariants, transition rules are described by formal method and theorem prover Isabelle is used to prove that all the rules hold the invariants in the model which guarantees the model’s reliability, and it realizes the automatic formal verification of model correctness.%在《雷息安全技术操作系统安全技术要求》中，提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况，对经典的数据机密性BLP模型进行陒应改进，为系统中的主客体引入多级安全标签以及安全迁移规则，使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述，使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性，从而实现对模型正确性的自动形式化验证，并保证了模型的可靠性。