Mantel, Heiko (2001)
Preserving Information Flow Properties under Refinement.
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (Abstract)
In a stepwise development process, it is essential thatsystem properties that have been already investigated insome phase need not be re-investigated in later phases. Informal developments, this corresponds to the requirementthat properties are preserved under refinement. While safetyand liveness properties are indeed preserved under moststandard forms of refinement, it is well known that this is,in general, not true for information flow properties, a largeand useful class of security properties. In this article, wepropose a collection of refinement operators as a solutionto this problem. We prove that these operators preserve informationflow as well as other system properties. Thus,information flow properties become compatible with stepwisedevelopment. Moreover, we show that our operatorsare an optimal solution.
Typ des Eintrags: | Konferenzveröffentlichung |
---|---|
Erschienen: | 2001 |
Autor(en): | Mantel, Heiko |
Art des Eintrags: | Bibliographie |
Titel: | Preserving Information Flow Properties under Refinement |
Sprache: | Englisch |
Publikationsjahr: | 2001 |
Verlag: | IEEE Computer Society |
Buchtitel: | Proceedings of the IEEE Symposium on Security and Privacy |
Kurzbeschreibung (Abstract): | In a stepwise development process, it is essential thatsystem properties that have been already investigated insome phase need not be re-investigated in later phases. Informal developments, this corresponds to the requirementthat properties are preserved under refinement. While safetyand liveness properties are indeed preserved under moststandard forms of refinement, it is well known that this is,in general, not true for information flow properties, a largeand useful class of security properties. In this article, wepropose a collection of refinement operators as a solutionto this problem. We prove that these operators preserve informationflow as well as other system properties. Thus,information flow properties become compatible with stepwisedevelopment. Moreover, we show that our operatorsare an optimal solution. |
Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Modellierung und Analyse von Informationssystemen (MAIS) |
Hinterlegungsdatum: | 31 Dez 2016 09:57 |
Letzte Änderung: | 03 Jun 2018 21:30 |
PPN: | |
Export: | |
Suche nach Titel in: | TUfind oder in Google |
Frage zum Eintrag |
Optionen (nur für Redakteure)
Redaktionelle Details anzeigen |