The PER model of Abstract Non-Interference
By: Sebastian Hunt and Isabella Mastroeni
Sebastian Hunt
Dept. of Computing, School of Informatics
City Univarsity
London EC1V OHB, UK
seb@soi.city.ac.uk
Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
mastroeni@sci.univr.it
Abstract:
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.
Related papers:
mastroeni@sci.univr.it