Measuring the confinement of probabilistic systems

In this paper we lay the semantic basis for a quantitative security analysis of probabilistic systems by introducing notions of approximate confinement based on various process equivalences. We re-cast the operational semantics classically expressed via probabilistic transition systems (PTS) in terms of linear operators and we present a technique for defining approximate semantics as probabilistic abstract interpretations of the PTS semantics. An operator norm is then used to quantify this approximation. This provides a quantitative measure ɛ of the indistinguishability of two processes and therefore of their confinement. In this security setting a statistical interpretation is then given of the quantity ɛ which relates it to the number of tests needed to breach the security of the system.