对一类多级安全模型安全性的形式化分析
文献类型：期刊论文
| 作者 | 何建波 ; 卿斯汉 ; 王超 |
| 刊名 | 计算机学报
 |
| 出版日期 | 2006 |
| 卷号 | 29期号:8页码:1468-1479 |
| 关键词 | BLP模型 MLS策略 安全不变式 Z语言 Z/EVES定理证明器 多级安全模型 安全性 形式化分析 不变式 验证模型 形式化规范 验证工具 系统安全 策略 表述形式 分析表 语言 思想 理论 客体 方法Computer programming languages Formal languages Functions Mathematical models Security of data Security systems Specifications Theorem prov |
| ISSN号 | 0254-4164 |
| 其他题名 | formal safety analysis of a class of multilevel security models |
| 中文摘要 | 深入分析了MLS的核心思想,给出了MLS在包含多级客体的系统中的表述形式,分析了安全不变式(invariant)在系统安全定义中的作用.为了保证模型的安全,必须验证模型的不变式满足MLS策略.为了说明不变式验证的重要性,借助Z语言和形式验证工具Z/EVES分析了一个改进的BLP模型--DBLP模型.分析表明,DBLP模型的不变式不满足MLS策略的要求,因此是不安全的.这项研究为分析各种改进BLP模型的安全性提供了理论依据和形式化规范与验证的方法. |
| 收录类别 | EI |
| 语种 | 中文 |
| 公开日期 | 2011-07-13 |
| 附注 | How to improve the traditional BLP model to make it more applicable is one of the major problems to be solved in the design of secure operating systems. There are several improved BLP models that have been applied to real systems. However, the security pr |
| 源URL | [http://124.16.136.157/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. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。