Publication
Information flow control revisited: Noninfluence = Noninterference + Nonleakage
Proceedings of ESORICS 2004
Author: David von Oheimb
Year: 2004
Publisher: Springer LNCS
CR Classification: D.2.4, F.1.2, H.2.0
CR General Terms: Security, Theory, Verification
Abstract:
We revisit the classical notion of noninterference for state-based systems,
as presented by Rushby in 1992. We strengthen his results in several ways,
in particular clarifying the impact of transitive vs. intransitive policies
on unwinding. Inspired partially by Mantel's observations on unwinding for
event systems, we remove the restriction on the unwinding relation to be an
equivalence and obtain new insights in the connection between unwinding
relations and observational preorders.
Moreover, we make two major extensions.
Firstly, we introduce the new notion of nonleakage, which complements
noninterference by focusing not on the observability of actions but the
information flow during system runs, and then combine it with
noninterference, calling the result noninfluence.
Secondly, we generalize all the results to (possibilistic) nondeterminism,
introducing the notions of uniform step consistency and uniform local respect.
Finally, we share our experience using nonleakage to analyze the confidentiality
properties of the Infineon SLE66 chip.
Like Rushby's, our theory has been developed and checked using a theorem
prover, so there is maximal confidence in its rigor and correctness.
Copyright © 2004 Springer-Verlag.
This paper has been published by
Springer LNCS.
Updated version with minor corrections
Slides, Isabelle sources
BibTeX entry:
@inproceedings{DvO-Noninfluence04,
author = {Oheimb, David von},
title = {Information flow control revisited: {Noninfluence = Noninterference + Nonleakage}},
booktitle = {Computer Security -- ESORICS 2004},
editor = {P.~Samarati and P.~Ryan and D.~Gollmann and R.~Molva},
conference = {ESORICS 2004},
publisher = {Springer},
series = {LNCS},
volume = {3193},
pages = {225--243},
year = 2004,
note = {\url{http://ddvo.net/papers/Noninfluence.html}},
CRClassification = {D.2.4, F.1.2, H.2.0},
CRGenTerms = {Security, Theory, Verification},
abstract = {
We revisit the classical notion of noninterference for state-based systems,
as presented by Rushby in 1992. We strengthen his results in several ways,
in particular clarifying the impact of transitive vs. intransitive policies
on unwinding. Inspired partially by Mantel's observations on unwinding for
event systems, we remove the restriction on the unwinding relation to be an
equivalence and obtain new insights in the connection between unwinding
relations and observational preorders.
Moreover, we make two major extensions.
Firstly, we introduce the new notion of nonleakage, which complements
noninterference by focusing not on the observability of actions but the
information flow during system runs, and then combine it with
noninterference, calling the result noninfluence.
Secondly, we generalize all the results to (possibilistic) nondeterminism,
introducing the notions of uniform step consistency and uniform local respect.
Finally, we share our experience using nonleakage to analyze the confidentiality
properties of the Infineon SLE66 chip.
Like Rushby's, our theory has been developed and checked using a theorem
prover, so there is maximal confidence in its rigor and correctness.
}
}