| 对一类多级安全模型安全性的形式化分析 |
| 其他题名 | formal safety analysis of a class of multilevel security models
|
| 何建波; 卿斯汉; 王超
|
| 2006
|
| 发表期刊 | 计算机学报
 |
| ISSN | 0254-4164
|
| 卷号 | 29期号:8页码:1468-1479 |
| 摘要 | 深入分析了MLS的核心思想,给出了MLS在包含多级客体的系统中的表述形式,分析了安全不变式(invariant)在系统安全定义中的作用.为了保证模型的安全,必须验证模型的不变式满足MLS策略.为了说明不变式验证的重要性,借助Z语言和形式验证工具Z/EVES分析了一个改进的BLP模型--DBLP模型.分析表明,DBLP模型的不变式不满足MLS策略的要求,因此是不安全的.这项研究为分析各种改进BLP模型的安全性提供了理论依据和形式化规范与验证的方法. |
| 收录类别 | EI
|
| 关键词 | Blp模型
Mls策略
安全不变式
Z语言
Z/eves定理证明器
多级安全模型
安全性
形式化分析
不变式
验证模型
形式化规范
验证工具
系统安全
策略
表述形式
分析表
语言
思想
理论
客体
方法computer Programming Languages
Formal Languages
Functions
Mathematical Models
Security Of Data
Security Systems
Specifications
Theorem Prov
|
| 部门归属 | 中国科学院软件研究所基础软件国家工程研究中心,北京,100080;中国科学院软件研究所信息安全技术工程研究中心,北京,100080;中国科学院研究生院,北京,100049;中国科学院软件研究所基础软件国家工程研究中心,北京,100080;中国科学院软件研究所信息安全技术工程研究中心,北京,100080;北京中科安胜信息技术有限公司,北京,100086;中国科学院软件研究所信息安全技术工程研究中心,北京,100080;北京中科安胜信息技术有限公司,北京,100086;中国科学院研究生院,北京,100049
|
| 语种 | 中文
|
| 内容类型 | 期刊论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/11640
|
| 专题 | 基础软件国家工程研究中心
|
推荐引用方式
GB/T 7714 |
何建波,卿斯汉,王超. 对一类多级安全模型安全性的形式化分析[J]. 计算机学报,2006,29(8):1468-1479.
|
| APA |
何建波,卿斯汉,&王超.(2006).对一类多级安全模型安全性的形式化分析.计算机学报,29(8),1468-1479.
|
| MLA |
何建波,et al."对一类多级安全模型安全性的形式化分析".计算机学报 29.8(2006):1468-1479.
|
修改评论