论文部分内容阅读
在不干扰理论的基础上，提出扩展不干扰模型ENISM及其验证方法，用以描述和分析操作系统中的信息流策略．工作包括：（1）依据系统功能模块定义多个执行域，以即将执行的可能动作序列集合与可读取的数据存储值集合一同作为ENISM定义执行域安全状态的基础；（2）给出判定系统中不存在违反策略的执行轨迹和数据流动的条件ENISM-CC（3）基于通信顺序进程给出ENISM—CC的语义及操作系统模块设计的形式化描述和验证方法．