BLP改进模型的形式化描述及自动化验证
Formal Description and Automated Verification of Improved BLP Model作者机构：湖南师范大学数学与计算机科学学院长沙410081 高性能计算与随机信息处理省部共建教育部重点实验室长沙410081
出 版 物：《计算机工程》 (Computer Engineering)
年 卷 期：2013年第39卷第12期
页 面：130-135页
核心收录：
学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论]
基 金：国家自然科学基金资助项目(60903168) 湖南省科技计划基金资助项目(2012FJ6012) 湖南省重点学科建设基金资助项目(湘教发76号) 湖南省教育厅科学研究基金资助项目(13C527) 长沙市科技计划基金资助项目(K1109020-11)
主 题：BLP模型 安全策略 形式化方法 自动化验证 定理证明 安全操作系统
摘 要：在《信息安全技术操作系统安全技术要求》中,提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况,对经典的数据机密性BLP模型进行相应改进,为系统中的主客体引入多级安全标签以及安全迁移规则,使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述,使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性,从而实现对模型正确性的自动形式化验证,并保证了模型的可靠性。
维普期刊数据库
同方期刊数据库