Semantics for Noninterference Security

When?

Thursday 1 December 2011, 10:00 to 11:00

Where?

39BB02

Open to:

Staff, Students, Public

Speaker:

Dr. Annabelle McIver

Abstract

The Shadow model [1] for qualitative noninterference security of sequential programs is a denotational model, complete with a refinement relation that preserves both functional- and security properties (the latter within its terms of reference). It was derived from a series of "gedanken" experiments in program-refinement algebra, then applied to Kripke structures as used for logics of knowledge.

The Hyperdistribution model for quantitative noninterference [2] was later constructed with the Shadow in mind, but essentially independently. It turns out to have strong structural links to Hidden Markov Models.

The technical component of this talk will be to describe the two kinds of semantics, i.e. the Shadow- (qualitative, possibilistic) and Hyperdistribution- (quantitative, probabilistic) structures we have built for noninterference with a refinement partial order (ie an implementation order that respects secrecy). Unusually, the two models will be described at the same time, interleaved; in this way I will try to bring out their similarities and differences.

If time permits, an example will be given of the kind of program algebra that results, and how the qualitative- and quantitative algebras can work together.

[1] CC Morgan, The Shadow Knows: Refinement of ignorance in sequential programming, Science Comp\Prog. 74(8), 2009.
[2] AK McIver, L Meinicke, CC Morgan, Compositional closure for Bayes Risk in probabilistic noninterference. Proc.ICALP 2010, LNCS 6199.

Biography

Annabelle McIver has published two texts in Formal Methods: one is a collection of articles by the internationally renowned membership of the IFIP Working Group 2.3 Programming Methodology [McIver 03]; the other is, to date, the only full research text on probabilistic program abstraction, refinement and proof [McIver 05]. She is the author of dozens of papers on Formal Methods ranging from highly theoretical (quantitative modal algebra) to extremely practical (automatic correctness verifiers for probabilistic systems). She holds degrees in mathematics from Cambridge and Oxford (UK), and has worked in industry. Currently she is based at Macquarie University in Sydney, and is affiliated with Australia's ICT centre where she applies mathematically based program-correctness techniques to the design and deployment of wireless sensor networks.

[McIver 03] Programming Methodology, A McIver and C Morgan (editors), Monographs in Computer Science, Springer, 2003.
[McIver 05] Abstraction, Refinement and Proof for Probabilistic Systems, A McIver and C Morgan, Monographs in Computer Science, Springer, 2005.