对一类多级安全模型安全性的形式化分析

• 作者: 何建波 卿斯汉 王超
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: BLP模型 MLS策略 安全不变式 Z语言 Z/EVES定理证明器
• 年，卷（期）: 2006,（8）
• 所属期刊栏目: 操作系统与数据库
• 页码范围: 1468-1479
• 页数: 12页
• 分类号: TP3
• 字数: 9229字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2006.08.026

摘要

深入分析了MLS的核心思想,给出了MLS在包含多级客体的系统中的表述形式,分析了安全不变式(invariant)在系统安全定义中的作用.为了保证模型的安全,必须验证模型的不变式满足MLS策略.为了说明不变式验证的重要性,借助Z语言和形式验证工具Z/EVES分析了一个改进的BLP模型--DBLP模型.分析表明,DBLP模型的不变式不满足MLS策略的要求,因此是不安全的.这项研究为分析各种改进BLP模型的安全性提供了理论依据和形式化规范与验证的方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	卿斯汉	中国科学院软件研究所基础软件国家工程研究中心	145	4238	29.0	62.0
10	何建波	中国科学院软件研究所基础软件国家工程研究中心	9	87	5.0	9.0