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

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

通过研究信道与那些向其输入信息或从其获得信息的信息域之间直接或间接的干扰关系,来定义信道的语义和作用。明确描述和严格控制系统模块和进程之间的信息通道,有利于最大限度地保障模块或进程的完整性和可控性。所提出的信道控制策略正是基于上述目的。而针对信道控制策略复杂而不便于手工验证的特点,提出了基于通信顺序进程(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.