Institutional Repository
| 对一类多级安全模型安全性的形式化分析 | |
| Alternative Title | formal safety analysis of a class of multilevel security models |
| 何建波; 卿斯汉; 王超 | |
| 2006 | |
| Source | 计算机学报
 |
| ISSN | 0254-4164 |
| Volume | 29Issue:8Pages:1468-1479 |
| English Abstract | 深入分析了MLS的核心思想,给出了MLS在包含多级客体的系统中的表述形式,分析了安全不变式(invariant)在系统安全定义中的作用.为了保证模型的安全,必须验证模型的不变式满足MLS策略.为了说明不变式验证的重要性,借助Z语言和形式验证工具Z/EVES分析了一个改进的BLP模型--DBLP模型.分析表明,DBLP模型的不变式不满足MLS策略的要求,因此是不安全的.这项研究为分析各种改进BLP模型的安全性提供了理论依据和形式化规范与验证的方法. |
| Indexed Type | EI |
| Keyword | Blp模型 Mls策略 安全不变式 Z语言 Z/eves定理证明器 多级安全模型 安全性 形式化分析 不变式 验证模型 形式化规范 验证工具 系统安全 策略 表述形式 分析表 语言 思想 理论 客体 方法computer Programming Languages Formal Languages Functions Mathematical Models Security Of Data Security Systems Specifications Theorem Prov |
| Department | 中国科学院软件研究所基础软件国家工程研究中心,北京,100080;中国科学院软件研究所信息安全技术工程研究中心,北京,100080;中国科学院研究生院,北京,100049;中国科学院软件研究所基础软件国家工程研究中心,北京,100080;中国科学院软件研究所信息安全技术工程研究中心,北京,100080;北京中科安胜信息技术有限公司,北京,100086;中国科学院软件研究所信息安全技术工程研究中心,北京,100080;北京中科安胜信息技术有限公司,北京,100086;中国科学院研究生院,北京,100049 |
| Language | 中文 |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/11640 |
| Collection | 基础软件国家工程研究中心 |
| Recommended Citation GB/T 7714 | 何建波,卿斯汉,王超. 对一类多级安全模型安全性的形式化分析[J]. 计算机学报,2006,29(8):1468-1479. |
| APA | 何建波,卿斯汉,&王超.(2006).对一类多级安全模型安全性的形式化分析.计算机学报,29(8),1468-1479. |
| MLA | 何建波,et al."对一类多级安全模型安全性的形式化分析".计算机学报 29.8(2006):1468-1479. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 对一类多级安全模型安全性的形式化分析.p（325KB） | 开放获取 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment