Abstract

The Lattice of Information (Landauer and Redmond) was an early and influential formalisation of the structure of secure systems: a partial order was defined that related to each other the mechanisms of deterministic information-flow out of a hidden state. In modern terms we would say that more-secure systems were refinements of less-secure ones under this order. In this deterministic case the refinement order is a lattice.

In more recent work the same approach has been taken to information flow in purely probabilistic systems, that is those in which information is released by a (probabilisitic) channel in the sense of Shannon. There too a refinement order can be defined (Alvim, Chatzikokolakis, McIver, Morgan, Palamidessi, Smith); but it is not a lattice.

In between those two structures above there are purely demonic systems, that is those whose information flow can be described by ``demonic channels'' whose behaviour is not determinstic but neither can it be quantified probabilistically. We show here that these demonic systems can be treated in the same style as in the the deterministic- and the probabilistic case, and there are results concerning compositionality, testing, soundness and completeness that allow interesting comparisons between all three.

And all three of these structures can be used as security-oriented semantics for sequential programming languages: the hierarchy is deterministic languages, languages with demonic nondeterminism (à la Dijkstra) and languages with probabilistic choice (à la Kozen). Adapting the security-oriented semantics to languages with both probabilistic- and demonic choice (our own work McIver, Morgan et al) remains a tougher challenge.


Last modified: Mon Aug 22 14:12:20 CEST 2016