Options
Preserving information flow properties under refinement
Publikationstyp
Conference Paper
Date Issued
2001-05
Sprache
English
Author(s)
Mantel, Heiko
Start Page
78
End Page
90
Citation
Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy: 78-90 (2001)
Contribution to Conference
Scopus ID
Publisher
IEEE
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 stepwise development. Moreover, we show that our operators are an optimal solution.
DDC Class
004: Informatik