Compositional noninterference from first principles

摘要

The recently formulated Shadow Semantics for noninterference-style security of sequential programs avoids the Refinement Paradox by preserving demonic nondeterminism in those cases where reducing it would compromise security. The construction (originally) of the semantic domain for The Shadow, and the interpretation of programs in it, relied heavily on intuition, guesswork and the advice of others. That being so, it is natural after the fact to try to reconstruct an idealised "inevitable" path from first principles to where we actually ended up: not only does one learn (more) about semantic principles by doing so, but the "rational reconstruction" helps to expose the choices made, along the way, and to legitimise the decisions that resolved them. Unlike our other papers on noninterference, this one does not contain a significant case study: instead its aim is to provide the most accessible account we can of the methods we use and why our model, in its details, has turned out the way it has. In passing, it might give some insight into the general role and significance of compositionality and testing-with-context for program semantics. Finally, a technical contribution here is a new "Transfer Principle" that captures uniformly a large class of classical refinements that remain valid when noninterference is taken into account in our style.