扩展不干扰模型(ENISM)及基于CSP的描述和验证方法

摘要：

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

关键词：不干扰模型、通信顺序进程、形式化描述、形式化验证、完整性

所属期刊栏目：33

分类号：TP309(计算技术、计算机技术)

资助基金：国家"八六三"高技术研究发展计划项目基金2007AA01Z409;国家自然科学基金60473093

在线出版日期：2010-06-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共13页

页码：877-889