基于不干扰理论的信道控制策略及其自动化验证方法  

Channel control strategy based on noninterference theory and its automated verification scheme

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

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

出　　处：《计算机应用》2010年第3期708-714,共7页journal of Computer Applications

基　　金：国家863计划项目(2007AA01Z409);江苏省高技术项目(BE2008124)

摘　　要：通过研究信道与那些向其输入信息或从其获得信息的信息域之间直接或间接的干扰关系,来定义信道的语义和作用。明确描述和严格控制系统模块和进程之间的信息通道,有利于最大限度地保障模块或进程的完整性和可控性。所提出的信道控制策略正是基于上述目的。而针对信道控制策略复杂而不便于手工验证的特点,提出了基于通信顺序进程(CSP)的系统和策略描述方法以及基于FDR2的系统信息流策略自动化验证方法。该方法能够在少量的人工参与的情况下有效地分析信道控制策略,发现大部分存储隐蔽通道。The authors defined the semantic description and functions of channels based on the study of the direct or indirect relation between any information domain and other domains who sent information to it or received from it.Exactly defining and strictly controlling the information channels between system modules or processes was beneficial to the integrity and controllability of the modules or processes.And in this paper,the new channel control strategy was used for this purpose.Channel control strategies were generally not easy to be manually verified because of their complexity.The authors presented an approach of describing system and strategies based on Communicating Sequential Processes（CSP）syntax and verifying the strategies in systems with automated verification tools FDR2.This approach can effectively and efficiently analyze the information channels and find out most of the storage covert channel.

关 键 词：不干扰模型 信道控制 信息流 通信顺序进程 形式化验证 

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