Title: | a multi-compositional enforcement on information flow security |
Author: | Sun Cong
; Zhai Ennan
; Chen Zhong
; Ma Jianfeng
|
Source: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
|
Conference Name: | 13th International Conference on Information and Communications Security, ICICS 2011
|
Conference Date: | November 2
|
Issued Date: | 2011
|
Conference Place: | Beijing, China
|
Keyword: | Abstracting
; Flow control
; Public policy
; Static analysis
|
Indexed Type: | EI
|
ISSN: | 0302-9743
|
ISBN: | 9783642252426
|
Department: | (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
|
Sponsorship: | National Natural Science Foundation of China (NNSFC); The Microsoft Corporation; Beijing Tip Technology Corporation; Trusted Computing Group (TCG)
|
Abstract: | 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. |
English Abstract: | 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. |
Language: | 英语
|
Content Type: | 会议论文
|
URI: | http://ir.iscas.ac.cn/handle/311060/16226
|
Appears in Collections: | 软件所图书馆_会议论文
|
There are no files associated with this item.
|
Recommended Citation: |
Sun Cong,Zhai Ennan,Chen Zhong,et al. a multi-compositional enforcement on information flow security[C]. 见:13th International Conference on Information and Communications Security, ICICS 2011. Beijing, China. November 2.
|
|
|