Modelling downgrading in information flow security

Information flow security properties such as noninterference ensure the protection of confidential data by strongly limiting the flow of sensitive information. However, to deal with real applications, it is often necessary to admit mechanisms for downgrading or declassifying information. In this paper, we propose a general unwinding framework for formalizing different noninterference properties permitting downgrading, i.e., allowing information to flow from a higher to a lower security level through a downgrader. The framework is parametric with respect to the observation equivalence used to discriminate between different process behaviours. We prove general compositionality properties and provide conditions under which both horizontal and vertical refinements are preserved under all the security properties obtained as instances of the unwinding framework. Finally, we present a decision procedure to check our security properties and prove some complexity results.