a multi-compositional enforcement on information flow security

ISCAS OpenIR

	a multi-compositional enforcement on information flow security
	Sun Cong; Zhai Ennan; Chen Zhong; Ma Jianfeng
	2011
会议名称	13th International Conference on Information and Communications Security, ICICS 2011
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	345-359
会议日期	November 2
会议地点	Beijing, China
收录类别	EI
ISSN	0302-9743
ISBN	9783642252426
部门归属	(1) Key Lab. of Computer Networks and Information Security Xidian Univ. MoE China; (2) Key Lab. of High Confidence Software Technologies Peking Univ. MoE China; (3) Key Lab. of Network and Software Security Assurance Peking Univ. MoE China; (4) Institute of Software Chinese Academy of Sciences China
摘要	Interactive/Reactive computational model is known to be proper abstraction of many pervasively used systems, such as client-side web-based applications. The critical task of information flow control mechanisms aims to determine whether the interactive program can guarantee the confidentiality of secret data. We propose an efficient and flow-sensitive static analysis to enforce information flow policy on program with interactive I/Os. A reachability analysis is performed on the abstract model after a form of transformation, called multi-composition, to check the conformance with the policy. In the multi-composition we develop a store-match pattern to avoid duplicating the I/O channels in the model, and use the principle of secure multi-execution to generalize the security lattice model which is supported by other approaches based on automated verification. We also extend our approach to support a stronger version of termination-insensitive noninterference. The results of preliminary experiments show that our approach is more precise than existing flow-sensitive analysis and the cost of verification is reduced through the store-match pattern. © 2011 Springer-Verlag.; Interactive/Reactive computational model is known to be proper abstraction of many pervasively used systems, such as client-side web-based applications. The critical task of information flow control mechanisms aims to determine whether the interactive program can guarantee the confidentiality of secret data. We propose an efficient and flow-sensitive static analysis to enforce information flow policy on program with interactive I/Os. A reachability analysis is performed on the abstract model after a form of transformation, called multi-composition, to check the conformance with the policy. In the multi-composition we develop a store-match pattern to avoid duplicating the I/O channels in the model, and use the principle of secure multi-execution to generalize the security lattice model which is supported by other approaches based on automated verification. We also extend our approach to support a stronger version of termination-insensitive noninterference. The results of preliminary experiments show that our approach is more precise than existing flow-sensitive analysis and the cost of verification is reduced through the store-match pattern. © 2011 Springer-Verlag.
关键词	Abstracting Flow Control Public Policy Static Analysis
主办者	National Natural Science Foundation of China (NNSFC); The Microsoft Corporation; Beijing Tip Technology Corporation; Trusted Computing Group (TCG)
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16226
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Sun Cong,Zhai Ennan,Chen Zhong,et al. a multi-compositional enforcement on information flow security[C],2011:345-359.