The PER Model of Abstract Non-Interference

In this paper we study the relationship between two models of secure information flow: the PER model (which uses equivalence relations) and the abstract non-interference model (which uses upper closure operators). Using the partitioning closures we embed the lattice of equivalence relations into the full lattice of closures and show how the definitions of both narrow and abstract non-interference can thus be re-interpreted over the lattice of equivalence relations. For narrow abstract non-interference, we show that the new definition is equivalent to the original, whereas for abstract non-interference it is strictly less general. We show how the relational presentation of narrow abstract non-interference leads to a simplified construction of the most concrete harmless attacker. Moreover, the generalization of the PER model of secure information flow allows us to derive unconstrained attacker models, which do not necessarily either observe all public information or ignore all private information. Finally, we show how abstract domain completeness can be used for enforcing the PER model of abstract non-interference, proving that abstract non-interference corresponds to abstract domain completeness of the corresponding partitioning closures