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

Formal Description and Automated Verification of Improved BLP Model

作　　者：徐亮[1,2] 谭煌[1,2] 

机构地区：[1]湖南师范大学数学与计算机科学学院,长沙410081 [2]高性能计算与随机信息处理省部共建教育部重点实验室,长沙410081

出　　处：《计算机工程》2013年第12期130-135,共6页Computer Engineering

基　　金：国家自然科学基金资助项目(60903168);湖南省科技计划基金资助项目(2012FJ6012);湖南省重点学科建设基金资助项目(湘教发[2011]76号);湖南省教育厅科学研究基金资助项目(13C527);长沙市科技计划基金资助项目(K1109020-11)

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]