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

• 作者: 何建波 卿斯汉 周洲仪 李丽萍 温红子
• 来源期刊: 通信学报
• 学科: 工学
• 关键词: 安全策略模型 形式规范 形式分析 定理证明 Bell-LaPadula模型
• 年，卷（期）: 2006,（6）
• 所属期刊栏目: 技术报告
• 页码范围: 94-101
• 页数: 8页
• 分类号: TP309
• 字数: 4657字
• 语种: 中文
• DOI: 10.3321/j.issn:1000-436X.2006.06.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	卿斯汉	中国科学院软件研究所	145	4238	29.0	62.0
2	温红子	国家电力监管委员会信息中心	1	14	1.0	1.0