Trustworthy Systems

Algebra for quantitative information flow

Authors

Annabelle McIver, Carroll Morgan and Tahiry Rabehaja

Macquarie University

Data61
CSIRO

UNSW

Abstract

A core property of program semantics is that local reasoning about program fragments remains sound even when the fragments are executed within a larger system. Mathematically this property corresponds to monotonicity of refinement: if A refines B then C(A) refines C(B) for any (valid) context defined by C(_). In other work we have studied a refines order for information flow in programs where the comparison defined by the order preserves both functional and confidentiality properties of secrets. However the semantic domain used in that work is only sufficient for scenarios where either the secrets are static (i.e. once initialised they never change), or where contexts C(_) never introduce fresh secrets. In this paper we show how to extend those ideas to obtain a model of information flow which supports local reasoning about confidentiality. We use our model to explore some algebraic properties of programs which contain secrets that can be updated, and which are valid in arbitrary contexts made up of possibly freshly declared secrets.

BibTeX Entry

  @inproceedings{McIver_MR_17,
    address          = {Lyon, France},
    author           = {McIver, Annabelle and Morgan, Carroll and Rabehaja, Tahiry},
    booktitle        = {International Conference on Relational and Algebraic Methods in Computer Science},
    doi              = {10.1007/978-3-319-57418-9_1},
    editor           = {{Peter H\"{o}fner, Damien Pous, Georg Struth}},
    keywords         = {refinement; information flow; security; monotonicity; probabilistic semantics; compositional
                        reasoning; dalenius desideratum},
    month            = may,
    pages            = {3--23},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9545.pdf},
    publisher        = {Springer},
    title            = {Algebra for Quantitative Information Flow},
    year             = {2017}
  }

Download