Compositional security and collateral leakage

TL;DR

This paper explores collateral information leaks in secure program refinement, emphasizing the importance of accounting for leaks outside declared variables, and proposes a collateral-aware semantic model to analyze and bound such leaks.

Contribution

It introduces a formal treatment of collateral leaks in compositional security models and adapts a Hidden-Markov framework to quantify and bound these leaks.

Findings

Collateral leaks can occur outside declared variables affecting security.

A collateral-aware semantic model enables calculation of leak severity.

Techniques are provided to bound collateral leakage in cryptographic contexts.

Abstract

In quantitative information flow we say that program $Q$ is "at least as secure as" $P$ just when the amount of secret information flowing from $Q$ is never more than flows from $P$, with of course a suitable quantification of "flow". This secure-refinement order $\sqsubseteq$ is compositional just when $P{\sqsubseteq}Q$ implies ${\cal C}(P){\sqsubseteq}{\cal C}(Q)$ for any context ${\cal C}$, again with a suitable definition of "context". Remarkable however is that leaks caused by executing $P,Q$ might not be limited to their declared variables: they might impact correlated secrets in variables declared and initialised in some broader context to which $P,Q$ do not refer even implicitly. We call such leaks collateral because their effect is felt in domains of which (the programmers of) $P, Q$ might be wholly unaware: our inspiration is the "Dalenius" phenomenon for statistical databases. We show that a proper treatment of these collateral leaks is necessary for a compositional program semantics for read/write "open" programs. By adapting a recent Hidden-Markov denotational model for non-interference security, so that it becomes "collateral aware", we give techniques and examples (e.g.\ public-key encryption) to show how collateral leakage can be calculated and then bounded in its severity.