Noninterference security (due to Goguen and Meseguer) considers breaches that result from the -interference- that hidden (high security) data might cause, via a computer system, to visible (low security) data. Attackers can then observe the visible values and, from that, infer properties of the hidden values. Program algebra is an approach to designing correct software in which source-level program texts are manipulated in correctness preserving (or enhancing) ways, usually to take a specification (eg an inefficient one) to an implementation (more efficient) — one that is as good as the specification, or better, according to properties agreed-on beforehand.

Program algebra for noninterference security thus begins with very simple, direct specifications such as “reveal the exclusive-or of three secret Booleans without revealing them individually” (as in Chaum’s Dining Cryptographers protocol). Then via correctness-preserving source-level steps, it is transformed into an actual implementable protocol involving flips of secret coins.

The talk will explain and illustrate this kind of construction as it applies to noninterference security, and then briefly look at the mathematical machinery [1,2,3] that makes it possible.

The following are available at http://www.cse.unsw.edu.au/~carrollm/probs/

[1] The Shadow Knows. Carroll Morgan. Science of Computer Programming 74(8):629-53. 2009. [2] Compositional closure for Bayes Risk in probabilistic noninterference. McIver, Meinicke, Morgan. Proc ICALP 2010 (Part II), 223-35. 2010. [3] A Kantorovich-Monadic Powerdomain for Information Hiding, with Probability and Nondeterminism. McIver, Meinicke, Morgan. Proc LiCS 2012.