文献类型：期刊文献

英文题名：Automatic analysis of DIFC systems using noninterference with declassification

作者：Li, Wenfa[1];Yang, Zhi[2];Liu, Jia[3]

通讯作者：Liu, J[1]

机构：[1]Beijing Union Univ, Beijing 100101, Peoples R China;[2]PLA Informat Engn Univ, Zhengzhou 450001, Peoples R China;[3]Beijing Union Univ, Smart City Coll, Beijing 100101, Peoples R China

第一机构：北京联合大学

通讯机构：[1]corresponding author), Beijing Union Univ, Smart City Coll, Beijing 100101, Peoples R China.|[1141733]北京联合大学继续教育学院;[11417]北京联合大学;

年份：2022

卷号：34

期号：12

起止页码：9385-9396

外文期刊名：NEURAL COMPUTING & APPLICATIONS

收录：;EI(收录号：20214211021824);Scopus(收录号：2-s2.0-85116937524);WOS:【SCI-EXPANDED(收录号:WOS:000706573200001)】；

基金：This work was supported by National Natural Science Foundation of China under Grant 61972040, and the Premium Funding Project for Academic Human Resources Development in Beijing Union University under Grant BPHR2020AZ03.

语种：英文

外文关键词：DIFC; Noninterference; Covert channel; CSP

摘要：Information flow control (IFC) can effectively resist Trojans and viruses that steal information from systems, and is usually adopted to protect the confidentiality of systems with a high security level. However, covert channel attacks can bypass IFC by exploiting its implementation defects. Thus, it is crucial to verify the system security and identify potential covert channels. Decentralized IFC (DIFC) is a key innovation that provides new flexible mechanisms, including decentralized declassification and taint tracking. However, the flexibility of DIFC systems also brings security risks. At present, there is a lack of a systematic and automatic security analysis approach for complex DIFC systems. In this paper, we propose a formal and automatic method to analyze the security of DIFC systems by using the FDR2 tool. We provide a new definition of noninterference, based on which the security analysis is performed. The analysis results indicate that our approach can both effectively detect covert channels in DIFC systems and accommodate conditional declassification information. The proposed method is more efficient and accurate than existing manual methods of covert channel detection.