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

Abstract: 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.

Key words: noninterference model, channel control, information flow, Communicating Sequential Processes (CSP), formal verification