Carroll Morgan

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.

A truly secure protocol is one which never violates its security requirements, no matter how bizarre the circumstances, provided those circumstances are within its terms of reference. Such cast-iron guarantees, as far as they are possible, require formal, rigorous techniques: proof or model-checking. Informally, they are difficult or impossible to achieve. Our rigorous technique is refinement , until recently not much applied to security. We argue its benefits by using refinement-based program algebra to develop several security case studies. That is one of our contributions here. The soundness of the technique follows from its compositional semantics, one which we defined (elsewhere) to support a specialisation of standard refinement by enriching standard semantics with information that tracks correlations between hidden state and visible behaviour. A further contribution is to extend the basic theory of secure refinement (Morgan in Mathematics of program construction, Springer, Berlin, vol. 4014, pp. 359–378, 2006 ) with special features required by our case studies, namely agent-based systems with complementary security requirements, and looping programs.

We use Hidden Markov Models to motivate a quantitative compositional semantics for noninterference-based security with iteration, including a refinement- or "implements" relation that compares two programs with respect to their information leakage; and we propose a program algebra for source-level reasoning about such programs, in particular as a means of establishing that an "implementation" program leaks no more than its "specification" program. This joins two themes: we extend our earlier work, having iteration but only qualitative, by making it quantitative; and we extend our earlier quantitative work by including iteration. We advocate stepwise refinement and source-level program algebra, both as conceptual reasoning tools and as targets for automated assistance. A selection of algebraic laws is given to support this view in the case of quantitative noninterference; and it is demonstrated on a simple iterated password-guessing attack.

In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that have remained open throughout the years, namely to find complete axiomatisations and alternative characterisations for these preorders. This paper solves both problems for finite processes with silent moves. It characterises the may preorder in terms of simulation, and the must preorder in terms of failure simulation. It also gives a characterisation of both preorders using a modal logic. Finally it axiomatises both preorders over a probabilistic version of CSP.

The mu-calculus is a powerful tool for specifying and verifying transition systems, including those with both demonic and angelic choice; its quantitative generalisation qMu extends that to probabilistic choice. We show that for a finite-state system the logical interpretation of qMu, via fixed-points in a domain of real-valued functions into [0,1], is equivalent to an operational interpretation given as a turn-based gambling game between two players. The logical interpretation provides direct access to axioms, laws and meta-theorems. The operational, game- based interpretation aids the intuition and continues in the more general context to provide a surprisingly practical specification tool. A corollary of our proofs is an extension of Everett's singly-nested games result in the finite turn-based case: we prove well-definedness of the minimax value, and existence of fixed memoriless strategies, for all qMu games/formulae, of arbitrary (including alternating) nesting structure.