Trustworthy Systems

a nondeterministic lattice of information


Carroll Morgan




In 1993 Landauer and Redmond [2] defined a “lattice of in- formation,” where a partition over the type of secret’s possible values could express the security resilience of a sequential, deterministic pro- gram: values within the same cell of the partition are those that the programs does not allow an attacker to distinguish. That simple, compelling model provided not only a refinement order for deterministic security (inverse refinement of set-partitions) but, since it is a lattice, allowed the construction of the “least-secure deterministic program more secure than these other deterministic programs”, and its obvious dual. But Landauer treated neither demonic nor probabilistic choice. Later work of our own, and independently of others, suggested a prob- abilistic generalisation of Landauer’s lattice [1, 3] — although it turned out that the generalisation is only a partial order, not a lattice [5]. This talk looks between the two structures above: I will combine earlier qualitatitve ideas [6] with very recent quantitative results [4] in order to explore – What an appropriate purely demonic lattice of information might be, the “meat in the sandwich” that lies between Landauer’s deter- ministic, qualitative lattice and our probabilistic partial order. – The importance of compositionality in determining its structure. – That it is indeed a lattice, that it generalises [2] and that it is gen- eralised by [1, 3]. – Its operational significance and, of course, – Thoughts on how it might help with constructing (secure) programs.

BibTeX Entry

    address          = {K\"onigswinter, Germany},
    author           = {Morgan, Carroll},
    booktitle        = {Mathematics of Program Construction},
    month            = jun,
    note             = {One-hour invited talk at Mathematics of Program Construction},
    paperurl         = {},
    slides           = {},
    title            = { A nondeterministic lattice of information},
    year             = {2015}