Sign in for Members and Observers

IFIP WG1.3 Foundations of System Specification

Talk "A demonic lattice of information"

by Carroll Morgan

Sat, 27 June 2015 at 05:00 pm in Nijmegen, The Netherlands

Joint work with: Annabelle McIver, Tahiry Rabehaja

Abstract: In between the Lattice of Information pioneered by Landauer and Redmond (1993), and recent work in Quantitative Information Flow that introduced hyper-distributions (ICALP 2010 -> LiCS 2015), there seems to be a vacancy for a demonic lattice of information. That is, whereas Landauer considered deterministic leaks (simple) and QIF considers leaking (probabilistic) channels (complicated), we should also be able to treat leaks that are unpredictable (not deterministic) but also unquantified (i.e. not governed by a distribution). That is of course demonic nondeterminism. This talk will describe such a model, based on union-closed sets of subsets of the hidden state, and will show how it generalises L&R's partitions, how it specialises hyper-distributions, and how it admits a backwards weakest-precondition style of reasoning about demonic security. [ Disclaimer: These models, in an earlier form, were the subject of a talk I gave at WG1.3 in 2011; but the current talk takes advantage of much more recent insights in order to put everything in its proper place and to produce a much clearer structure. ]