Game semantics for non-deterministic security

<p>The <em>Shadow</em> <em>Semantics</em> [47, 48, 50] models <em>secure</em> <em>refinement</em>, i.e. preservation of privacy under adversarial <em>inference attacks</em>. Previous work has given a structural (affirmative) account of secure refinement and its primitives, with some progress towards a testing (refutational) account. At the same time, (mutable-state) <em>programs </em>in the Shadow Se- mantics can be modelled readily as functions, but lack ‘healthiness conditions’ [11, 53] to characterise the underlying properties of information flow. Our contributions are twofold. First, we provide a testing (refutational) account of secure refinement as a <em>game</em> <em>semantics</em> for a certain adversarial game. In so doing we develop and characterise the ‘predicates’ first proposed in [47]. This game semantics provides an interpretation of the Shadow Semantics in terms of a security threat model. Its structure hints at connections to the quantitative analogue, qif [4]. Second, we give an <em>order-theoretic</em> account of the Shadow Semantics, adapting a recently developed framework from category theory [27, 32]. The Shadow Semantics’s main primitives are shown to arise from an adjunction on a certain ‘lax’ category. This account gives an alternative ‘first-principles’ derivation of the Shadow Semantics, and hints at future foundational work in the category theory of inference attacks.</p>