Preserving information flow properties under refinement
- 13 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
In a stepwise development process, it is essential that system properties that have been already investigated in some phase need not be re-investigated in later phases. In formal developments, this corresponds to the requirement that properties are preserved under refinement. While safety and liveness properties are indeed preserved under most standard forms of refinement, it is well known that this is, in general, not true for information flow properties, a large and useful class of security properties. In this article, we propose a collection of refinement operators as a solution to this problem. We prove that these operators preserve information flow as well as other system properties. Thus, information flow properties become compatible with step-wise development. Moreover, we show that our operators are an optimal solution.Keywords
This publication has 14 references indexed in Scilit:
- On the derivation of secure componentsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Unwinding forward correctabilityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- On the refinement of non-interferencePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Possibilistic definitions of security-an assembly kitPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Unwinding Possibilistic Security PropertiesPublished by Springer Nature ,2000
- A Classification of Security Properties for Process Algebras1Journal of Computer Security, 1995
- Non-interference through determinismPublished by Springer Nature ,1994
- Refinement and ConfidentialityPublished by Springer Nature ,1992
- Information flow in nondeterministic systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Security Policies and Security ModelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982