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

An Extended Non-Interference Security Model(ENISM) and Its CSP-Based Description and Verification Method

作　　者：崔隽[1,2] 黄皓[1,2] 高晓春[1,2] 

机构地区：[1]南京大学软件新技术国家重点实验室,南京210093 [2]南京大学计算机科学与技术系,南京210093

出　　处：《计算机学报》2010年第5期877-889,共13页Chinese Journal of Computers

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

摘　　要：在不干扰理论的基础上,提出扩展不干扰模型ENISM及其验证方法,用以描述和分析操作系统中的信息流策略.工作包括:(1)依据系统功能模块定义多个执行域,以即将执行的可能动作序列集合与可读取的数据存储值集合一同作为ENISM定义执行域安全状态的基础;(2)给出判定系统中不存在违反策略的执行轨迹和数据流动的条件ENISM-CC;(3)基于通信顺序进程给出ENISM-CC的语义及操作系统模块设计的形式化描述和验证方法.Based on the theory of non-interference, this paper proposes an extended non-interference security model ENISM, for the purpose of specification and analysis of information flow policies in operating systems. This paper includes the following works, firstly, system modules would be recognized as domains, and the traces set which contains traces may be implemented after a system state and the data values set at the state are two most important analysis gist for defining the secure states in ENISM. Secondly, the sufficient conditions ENISM-CC are proposed on which unsafe traces and data flow is not existed. Thirdly, this paper gives out a formal description method for system design and describes the semantic ENISM-CC based on the Communicating Sequential Processes CSP.

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]