中文摘要：

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

英文摘要：

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.