Please wait a minute...
J4  2010, Vol. 44 Issue (5): 854-862    DOI: 10.3785/j.issn.1008-973X.2010.05.004
姜励, 陈健, 平玲娣, 陈小平
浙江大学 计算机科学与技术学院,浙江 杭州 310027
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
 全文: PDF  HTML



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.

出版日期: 2012-03-19
:  TP 309  


通讯作者: 平玲娣,女,教授,博导     E-mail:
作者简介: 姜励(1981—),男,湖北仙桃人,博士生,从事基于语言的信息流安全相关领域研究.E-mail:
E-mail Alert


姜励, 陈健, 平玲娣, 陈小平. 多线程程序的信息抹除和降密安全策略[J]. J4, 2010, 44(5): 854-862.

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.


[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] 王友卫, 刘元宁, 朱晓冬. 用于图像内容认证的半脆弱水印新算法[J]. J4, 2013, 47(6): 969-976.
[2] 李卓,陈健,蒋晓宁,曾宪庭,潘雪增. 基于多域特征的JPEG图像盲检测算法[J]. J4, 2011, 45(9): 1528-1538.
[3] 彭志宇, 李善平, 杨朝晖, 林欣. 信任管理中的匿名授权方法[J]. J4, 2010, 44(5): 897-902.
[4] 黄勇, 陈小平, 陈文智, 等. 支持动态调节的保密性和完整性统一模型[J]. J4, 2009, 43(8): 1377-1382.