安全策略模型规范及其形式分析技术研究

作者：李丽萍; 卿斯汉; 周洲仪; 何建波; 温红子

来源：通信学报, 2006, (06): 94-101.

• 安全策略模型
• 形式规范
• 形式分析
• 定理证明
• Bell-LaPadula模型 security policy model
• formal specification
• formal analysis
• theorem prove
• Bell-LaPadula model

形式化是开发高安全等级计算机系统的核心技术之一,但目前形式开发方法无法直接借助于机器证明获得较之手工证明更加严格的安全策略模型正确性保证,以及安全策略模型和安全功能规范之间的精确对应。通过把安全功能规范开发技术应用于安全策略模型的开发中,提出了一种新颖的安全策略模型形式规范构造方法及其证明机理,从而有效解决了上述问题。还以Bell-LaPadula多级安全策略为实例,具体说明了规范的形式开发和形式分析过程。

• 出版日期2006
• 单位中国科学院大学; 中国科学院软件研究所