Please wait a minute...
浙江大学学报(工学版)
J4  2010, Vol. 44 Issue (5): 854-862    DOI: 10.3785/j.issn.1008-973X.2010.05.004
    
Security policy for information erasing and leaking in multithreaded codes
JIANG Li, CHEN Jian, PING Ling-di, CHEN Xiao-ping
College of Computer Science and Technology, Zhejiang University, Hangzhou 310027, China
Download:   PDF(0KB) HTML
Export: BibTeX | EndNote (RIS)      

Abstract  

In multithreaded environment, sensitive information is often deliberately released by many real applications and sometimes information needs to become more confidential. In order to address this situation, a security policy was defined in the style of strong bisimulation equivalence, which can handle both information leaking and erasing. The policy controls what information is released and guarantees that attackers cannot exploit information releasing mechanisms to reveal more sensitive data than intended. Moreover, it ensures that public data after erasing cannot be abused by attackers. Then a secure transforming type system was proposed to enforce the security policy by using the crosscopying technique, which can eliminate internal timing covert channels resulting from the interplay between different threads. The transforming type system can transform an insecure program into a secure one, trying to close information leaks. The secure program has the same structure as the original program and models the same timing behavior. Finally, the soundness of the type system was proved with respect to the operational semantics. Results indicate that if a program can be transformed according to typing rules, the resulting program satisfies the security policy.

Published: 19 March 2012
CLC:  TP 309  
Service
E-mail this article
Add to my bookshelf
Add to citation manager
E-mail Alert
RSS
Articles by authors
Cite this article:

JIANG Li, CHEN Jian, BENG Ling-Di, CHEN Xiao-Beng. Security policy for information erasing and leaking in multithreaded codes. J4, 2010, 44(5): 854-862.

URL:

http://www.zjujournals.com/eng/10.3785/j.issn.1008-973X.2010.05.004     OR     http://www.zjujournals.com/eng/Y2010/V44/I5/854


多线程程序的信息抹除和降密安全策略

为了满足多线程环境下实际应用程序故意释放敏感信息以及加强信息机密性的需求,基于强互模拟等价的方式定义能够同时处理信息降密和抹除的安全属性.该属性能控制被释放的机密信息的内容,使得降密机制不会被攻击者破坏而获得额外的机密信息,并且保证低安全级信息被抹除后无法再被攻击者滥用；使用交叉拷贝技术构造实施该安全属性的安全转换类型系统,可消除由于线程之间互相竞争执行而引起的内部时间隐蔽通道.通过转换类型系统可将一个给定程序转换成具有相同结构以及时间行为的安全程序,消除其中的信息泄露.根据操作语义证明了该类型系统的类型可靠性,表明遵循类型规则转换后的程序可满足系统的安全属性.

［1］ FOCARDI R, GORRIERI R. A classification of security properties for process algebras ［J］. Journal of Computer Security, 1995, 3(1): 533.

［2］ VOLPANO D, SMITH G, IRVINE C. A sound type system for secure flow analysis ［J］. Journal of Computer Security, 1996, 4(3): 167187.


［3］ SABELFELD A, MYERS A C. Languagebased informationflow security ［J］. IEEE Journal on Selected Areas in Communications, 2003, 21(1): 519.

［4］ GOGUEN J A, MESEGUER J. Security policies and security models ［C］∥ Proceedings of the 1982 IEEE Symposium on Research in Security and Privacy. Oakland: IEEE, 1982: 1120.

［5］ SABELFELD A, SANDS D. Dimensions and principles of declassification ［C］∥ Proceedings of the 18th IEEE Computer Security Foundations Workshop. AixenProvence: IEEE, 2005: 255269.

［6］ MYERS A C, SABELFELD A, ZDANCEWIC S. Enforcing robust declassification ［C］∥ Proceedings of the 17th IEEE Computer Security Foundations Workshop. Pacific Grove: IEEE, 2004: 172186.

［7］ SABELFELD A, MYERS A C. A model for delimited information release ［C］∥ Proceedings of the International Symposium on Software Security 2003 (ISSS’03). Berlin: SpringerVerlag, 2004: 174191.

［8］ ROSCOE A W, GOLDSMITH M H. What is intransitive noninterference ［C］∥ Proceedings of the 12th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE, 1999: 228238.


［9］ CHONG S, MYERS A C. Security policies for downgrading［C］∥ Proceeding of 11th ACM Conference on Computer and Communications Security. Washington DC: ACM, 2004: 198209.

［10］ CHONG S, MYERS A C. Languagebased information erasure［C］∥ Proceedings of the 18th IEEE Computer Security Foundations Workshop. AixenProvence: IEEE, 2005: 241254.

［11］ MANTEL H, REINHARD A. Controlling the what and where of declassification in languagebased security［C］∥ Proceedings of the European Symposium on Programming 2007 (ESOP’07). Berlin: SpringerVerlag, 2007: 141156.

［12］ SABELFELD A, SANDS D. Probabilistic noninterference for multithreaded programs［C］∥ Proceedings of IEEE Computer Security Foundations Workshop. Cambridge: IEEE, 2000: 200215.

［13］ JOHAN A. Transforming out timing leaks ［C］∥ Proceedings of the 27th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. Washington DC: ACM, 2000: 4053.
[1] WANG You-wei, LIU Yuan-ning, ZHU Xiao-dong. Novel semi-fragile watermarking algorithm for image content authentication[J]. J4, 2013, 47(6): 969-976.
[2] LI Zhuo, CHEN Jian, JIANG Xiao-ning, ZENG Xian-ting, PAN Xue-zeng. Blind JPEG steganalysis based on multi-domain features[J]. J4, 2011, 45(9): 1528-1538.
[3] BANG Zhi-Yu, LI Shan-Beng, YANG Chao-Hui, LIN Xin. Anonymous authorization in trust management[J]. J4, 2010, 44(5): 897-902.
[4] HUANG Yong, CHEN Xiao-Ping, CHEN Wen-Zhi. Dynamically modified union model combining confidentiality and integrity[J]. J4, 2009, 43(8): 1377-1382.