Institutional Repository
| 对一类多级安全模型安全性的形式化分析 | |
| 其他题名 | 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. |
| 条目包含的文件 | ||||||
| 文件名称/大小 | 文献类型 | 版本类型 | 开放类型 | 使用许可 | ||
| 对一类多级安全模型安全性的形式化分析.p(325KB) | 开放获取 | -- | 请求全文 | |||
| 个性服务 |
| 推荐该条目 |
| 保存到收藏夹 |
| 查看访问统计 |
| 导出为Endnote文件 |
| 谷歌学术 |
| 谷歌学术中相似的文章 |
| [何建波]的文章 |
| [卿斯汉]的文章 |
| [王超]的文章 |
| 百度学术 |
| 百度学术中相似的文章 |
| [何建波]的文章 |
| [卿斯汉]的文章 |
| [王超]的文章 |
| 必应学术 |
| 必应学术中相似的文章 |
| [何建波]的文章 |
| [卿斯汉]的文章 |
| [王超]的文章 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论