Talk "Refinement-oriented noninterference: Comparison of a qualitative and a quantitative model "

by Carroll Morgan

Sat, 03 September 2011 at 11:00 am in Winchester, United Kingdom

Joint work with: Annabelle McIver (Macquarie University), Larissa Meinicke (Macquarie University)

Abstract: Qualitative vs quantitative semantics for noninterference: an evolution in parallel <BR><BR> The Shadow model for qualitative noninterference of sequential programs [a] 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. <BR><BR> The Hyperdistribution model for quantitative noninterference [b] was later constructed with the Shadow in mind, but essentially independently. It turns out to have strong structural links to Hidden Markov Models. <BR><BR> 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 in parallel (interleaved concurrency, not truly concurrent with two screens); in this way I will try to bring out their similarities and differences. <BR><BR> 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. <BR><BR> [a] C.C. Morgan. The Shadow Knows: Refinement of ignorance in sequential programs.<BR> Conference version in Proc. Math Prog Construction 2006, LNCS 4014:359-78, 2006.<BR> Journal version in Science of Computer Programming, 74(8):629-653, 2009. <BR><BR> [b] Annabelle McIver, Larissa Meinicke, and Carroll Morgan.<BR> Compositional closure for Bayes Risk in probabilistic noninterference.<BR> ICALP'10 Part II, pages 223-235, 2010.