计算机工程

• 安全技术 • 上一篇    下一篇

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

徐 亮1,2,谭 煌1,2   

  1. (1. 湖南师范大学数学与计算机科学学院,长沙 410081;2. 高性能计算与随机信息处理省部共建教育部重点实验室,长沙 410081)
  • 收稿日期:2012-11-26 出版日期:2013-12-15 发布日期:2013-12-13
  • 作者简介:徐 亮(1981-),男,讲师、博士、CCF会员,主研方向:形式化方法,安全策略模型,语义检索;谭 煌,讲师
  • 基金项目:
    国家自然科学基金资助项目(60903168);湖南省科技计划基金资助项目(2012FJ6012);湖南省重点学科建设基金资助项目(湘教发[2011]76号);湖南省教育厅科学研究基金资助项目(13C527);长沙市科技计划基金资助项目(K1109020-11)

Formal Description and Automated Verification of Improved BLP Model

XU Liang 1,2, TAN Huang 1,2   

  1. (1. College of Mathematics and Computer Science, Hunan Normal University, Changsha 410081, China; 2. Key Laboratory of High Performance Computing and Stochastic Information Processing, Ministry of Education of China, Changsha 410081, China)
  • Received:2012-11-26 Online:2013-12-15 Published:2013-12-13

摘要: 在《信息安全技术操作系统安全技术要求》中,提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况,对经典的数据机密性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

中图分类号: