Modelling downgrading in information flow security
- 1 January 2004
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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 resultsKeywords
This publication has 16 references indexed in Scilit:
- Robust declassificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Unwinding in Information Flow SecurityElectronic Notes in Theoretical Computer Science, 2004
- Intransitive non-interference for cryptographic purposesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- CoPS – Checker of Persistent SecurityPublished by Springer Nature ,2004
- Quantifying information flowPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- What is intransitive noninterference?Published by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Refinement operators and information flow securityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Absorbing covers and intransitive non-interferencePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Bisimulation-based Non-deterministic Admissible Interference and its Application to the Analysis of Cryptographic ProtocolsElectronic Notes in Theoretical Computer Science, 2002
- Process algebra and non-interferencePublished by Institute of Electrical and Electronics Engineers (IEEE) ,1999