文献类型：期刊文章

作　　者：何建波[1,2,3] 卿斯汉[1,2,4] 王超[5,4,3]

机构地区：[1]中国科学院软件研究所基础软件国家工程研究中心 [2]中国科学院软件研究所信息安全技术工程研究中心北京100080 [3]中国科学院研究生院北京100049 [4]北京中科安胜信息技术有限公司北京100086 [5]中国科学院软件研究所信息安全技术工程研究中心

出　　处：《计算机学报》

基　　金：北京市自然科学基金(4052016);国家自然科学基金(60573042);国家"九七三"重点基础研究发展规划项目基金(G1999035802)资助.

年　　份：2006

卷　　号：29

期　　号：8

起止页码：1468-1479

语　　种：中文

收录情况：BDHX、BDHX2004、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：20064110165641)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、核心刊

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

关 键 词：BLP模型 MLS策略  安全不变式  Z语言 Z/EVES定理证明器  

分 类 号：TP309]