@inproceedings{040cefb081644d729a57b59c81c1f198,
title = "On two models of noninterference: Rushby and Greve, Wilding, and Vanfleet",
abstract = "We formally compare two industrially relevant and popular models of noninterference, namely, the model defined by Rushby and the one defined by Greve, Wilding, and Vanfleet (GWV). We create a mapping between the objects and relations of the two models. We prove a number of theorems showing under which assumptions a system identified as {"}secure{"} in one model is also identified as {"}secure{"} in the other model. Using two examples, we illustrate and discuss some of these assumptions. Our main conclusion is that the GWV model is more discriminating than the Rushby model. All systems satisfying GWV{\textquoteright}s Separation also satisfy Rushby{\textquoteright}s noninterference. The other direction only holds if we additionally assume that GWV systems are such that every partition is assigned at most one memory segment. All of our proofs have been checked using the Isabelle/HOL proof assistant. Keywords: Noninterference; information flow security; formal models",
author = "\{Garcia Ramirez\}, A. and J. Schmaltz and F. Verbeek and B. Langenstein and H. Blasum",
year = "2014",
doi = "10.1007/978-3-319-10506-2\_17",
language = "English",
isbn = "978-3-319-10505-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "246--261",
editor = "A. Bondavalli and \{Di Giandomenico\}, F.",
booktitle = "33rd International Conference on Computer Safety, Reliability and Security (SafeComp'14, Firenze, Italy, September 10-12, 2014)",
address = "Germany",
note = "conference; 33rd International Conference on Computer Safety, Reliability and Security ; Conference date: 01-01-2014",
}