作者：李丽萍; 卿斯汉; 周洲仪; 何建波; 温红子安全策略模型形式规范形式分析定理证明
摘要：形式化是开发高安全等级计算机系统的核心技术之一,但目前形式开发方法无法直接借助于机器证明获得较之手工证明更加严格的安全策略模型正确性保证,以及安全策略模型和安全功能规范之间的精确对应.通过把安全功能规范开发技术应用于安全策略模型的开发中,提出了一种新颖的安全策略模型形式规范构造方法及其证明机理,从而有效解决了上述问题.还以Bell-LaPadula多级安全策略为实例,具体说明了规范的形式开发和形式分析过程.
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
