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.

The PER Model of Abstract Non-Interference

MASTROENI, Isabella
2005-01-01

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.
2005
9783540285847
information flow; non-interference; abstract interpretation; language-based security
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/23531
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 21
  • ???jsp.display-item.citation.isi??? 16
social impact