Handling Information Release and Erasure in Multi-Threaded Programs

Language-based information flow security proper- ties such as noninterference ensure confidential data cannot interfere with public data. But in real comput- ing systems sensitive information sometimes needs to be released or to become more confidential. In this paper, we propose a new security property including support for both information release and erasure. Since the property is in the style of strong bisimulation equivalence, it is applicable to multi-threaded pro- grams. To ensure that declassification cannot be ex- ploited to reveal more secret data than intended, our property addresses what information may be released. Moreover, the property guarantees that dynamic up- grading the security label of data due to erasure re- quirement cannot affect the publicly visible behavior.