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

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

在不干扰理论的基础上,提出扩展不干扰模型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.