Game semantics for non-deterministic security

The Shadow Semantics [47, 48, 50] models secure refinement, i.e. preservation of privacy under adversarial inference attacks. 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) programs 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 game semantics 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 order-theoretic 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.