摘要： 在《信息安全技术操作系统安全技术要求》中，提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况，对经典的数据机密性BLP模型进行相应改进，为系统中的主客体引入多级安全标签以及安全迁移规则，使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述，使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性，从而实现对模型正确性的自动形式化验证，并保证了模型的可靠性。
关键词:
BLP模型,
安全策略,
形式化方法,
自动化验证,
定理证明,
安全操作系统
Abstract: 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.
Key words:
BLP model,
security policy,
formal method,
automated verification,
theorem proving,
security operating system
中图分类号: