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's Separation also satisfy Rushby'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.
Isabelle/HOL Proof Scripts here