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
摘要：

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

国家“863”高技术研究发展计划资助项目（2006AA01Z431）；国家“十一五”科技支撑计划资助项目（2008BAH21B03）；浙江省科技计划资助项目（2007L11068）.
通讯作者: 平玲娣，女，教授，博导     E-mail: ldping@cs.zju.edu.cn
作者简介: 姜励（1981—），男，湖北仙桃人，博士生，从事基于语言的信息流安全相关领域研究．E-mail: ljiang@zju.edu.cn
服务　　
把本文推荐给朋友
加入引用管理器
E-mail Alert
RSS
作者相关文章　　

引用本文:

姜励, 陈健, 平玲娣, 陈小平. 多线程程序的信息抹除和降密安全策略[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.

链接本文:

http://www.zjujournals.com/eng/CN/10.3785/j.issn.1008-973X.2010.05.004    或    http://www.zjujournals.com/eng/CN/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] 王友卫, 刘元宁, 朱晓冬. 用于图像内容认证的半脆弱水印新算法[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.