Automated enforcement for relaxed information release with reference points

作     者：SUN Cong XI Ning GAO Sheng CHEN Zhong MA JianFeng 

作者机构：School of Computer Science and Technology Xidian University School of Electronics Engineering and Computer Science Peking University 

出 版 物：《Science China(Information Sciences)》 (中国科学:信息科学(英文版))

年 卷 期：2014年第57卷第11期

页      面：131-149页

核心收录：

学科分类：11[军事学] 0810[工学-信息与通信工程] 1105[军事学-军队指挥学] 0808[工学-电气工程] 0839[工学-网络空间安全] 08[工学] 110505[军事学-密码学] 110503[军事学-军事通信学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：supported by the Key Program of NSFC-Guangdong Union Foundation(Grant No.U1135002) the National Natural Science Foundation of China(Grant No.61303033) the Major National S&T Program(GrantNo.2011ZX03005-002) the Fundamental Research Funds for the Central Universities(Grant No.JB140309) the Natural Science Basis Research Plan in Shaanxi Province of China(Grant No.2013JQ8036) the Aviation Science Foundation of China(Grant No.2013ZC31003) 

主　　题：information flow security policy noninterference declassification pushdown system program analysis 

摘      要：Language-based information flow security is a promising approach for enforcement of strong security and protection of the data confidentiality for the end-to-end communications. Here, noninterference is the standard and most restricted security property that completely forbids confidential data from being released to public context. Although this baseline property has been extensively enforced in various cases, there are still many programs, which are considered secure enough, violating this property in some way. In order to control the information release in these programs, the predetermined ways should be specified by means of which confidential data can be released. These intentional releases, also called declassifications, are regulated by several more relaxed security properties than noninterference. The security properties for controlled declassification have been developed on different dimensions with declassification goals. However, the mechanisms used to enforce these properties are still unaccommodating, unspecific, and insufficiently studied. In this work, a new security property, the Relaxed Release with Reference Points(R3P), is presented to limit the information that can be declassified in a program. Moreover, a new mechanism using reachability analysis has been proposed for the pushdown system to enforce R3 P on programs. In order to show R3 P is competent for use, it has been proved that it complies with the well-known prudent principles of declassification, and in addition finds some restrictions on our security policy. The widespread usage, precision, efficiency, and the influencing factors of our enforcement have been evaluated.