| 安全策略模型规范及其形式分析技术研究 |
| 李丽萍; 卿斯汉; 周洲仪; 何建波; 温红子
|
| 2006
|
| 发表期刊 | 通信学报
 |
| 期号 | 6页码:94-101 |
| 摘要 | 形式化是开发高安全等级计算机系统的核心技术之一,但目前形式开发方法无法直接借助于机器证明获得较之手工证明更加严格的安全策略模型正确性保证,以及安全策略模型和安全功能规范之间的精确对应。通过把安全功能规范开发技术应用于安全策略模型的开发中,提出了一种新颖的安全策略模型形式规范构造方法及其证明机理,从而有效解决了上述问题。还以Bell-LaPadula多级安全策略为实例,具体说明了规范的形式开发和形式分析过程。 |
| 关键词 | 安全策略模型
形式规范
形式分析
定理证明
Bell-lapadula模型
|
| 部门归属 | 中国科学院软件研究所,中国科学院软件研究所,中国科学院软件研究所,中国科学院软件研究所,国家电力监管委员会信息中心 北京100080,中国科学院研究生院,北京100049,北京100080,北京100080,中国科学院研究生院,北京100049,北京100080,中国科学院研究生院,北京100049,北京100045
|
| 内容类型 | 期刊论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/11618
|
| 专题 | 基础软件国家工程研究中心
|
推荐引用方式
GB/T 7714 |
李丽萍,卿斯汉,周洲仪,等. 安全策略模型规范及其形式分析技术研究[J]. 通信学报,2006(6):94-101.
|
| APA |
李丽萍,卿斯汉,周洲仪,何建波,&温红子.(2006).安全策略模型规范及其形式分析技术研究.通信学报(6),94-101.
|
| MLA |
李丽萍,et al."安全策略模型规范及其形式分析技术研究".通信学报 .6(2006):94-101.
|
修改评论