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

• 作者: 崔隽 高晓春 黄皓
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 不干扰模型 通信顺序进程 形式化描述 形式化验证 完整性
• 年，卷（期）: 2010,（5）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 877-889
• 分类号: TP309
• 字数: 12775字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2010.00877

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄皓	南京大学软件新技术国家重点实验室	140	1805	24.0	35.0
5	高晓春	南京大学软件新技术国家重点实验室	2	2	1.0	1.0
9	崔隽	南京大学软件新技术国家重点实验室	7	56	3.0	7.0