10.3969/j.issn.1000-3428.2013.12.028
BLP改进模型的形式化描述及自动化验证
在《雷息安全技术操作系统安全技术要求》中,提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况,对经典的数据机密性BLP模型进行陒应改进,为系统中的主客体引入多级安全标签以及安全迁移规则,使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述,使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性,从而实现对模型正确性的自动形式化验证,并保证了模型的可靠性。
BLP模型、安全策略、形式化方法、自动化验证、定理证明、安全操作系统
TP301.2(计算技术、计算机技术)
国家自然科学基金资助陠目60903168;湖南省科技计划基金资助陠目2012FJ6012;湖南省重点学科建设基金资助陠目陘教发[2011]76号;湖南省教育厅科学研究基金资助陠目13C527;长沙市科技计划基金资助陠目K1109020-11
2013-12-30(万方平台首次上网日期,不代表论文的发表时间)
共6页
130-135