Modelling Downgrading in Information Flow Security.
Sabina Rossi
Abstract
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.