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

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

实时系统中最急优先调度策略的二进表示模型

本文提出一个实时系统中最急优先调度策略的二进表示Markov过程模型。以减少软实时系统中任务损失率为衡量标准,最急优先调度策略被证明是一个最佳策略,但其效率却极难分析。本文的模型使这一策略的分析变得可行和简单。基于本文的理论,已得到一系列有关最急优先策略的重要的性能评价分析结果。