Algebra for quantitative information flow

A. K. McIver*, C. C. Morgan, T. Rabehaja

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

4 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationRelational and algebraic methods in computer science
Subtitle of host publication16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017. Proceedings
EditorsPeter Höfner, Damien Pous, Georg Struth
PublisherSpringer, Springer Nature
Pages3-23
Number of pages21
ISBN (Electronic)9783319574189
ISBN (Print)9783319574172
DOIs
Publication statusPublished - 2017
Event16th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2017 - Lyon, France
Duration: 15 May 201718 May 2017

Publication series

NameLecture Notes in Computer Science
Volume10226
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other16th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2017
CountryFrance
CityLyon
Period15/05/1718/05/17

Keywords

  • Compositional reasoning
  • Dalenius desideratum
  • Information flow
  • Monotonicity
  • Probabilistic semantics
  • Refinement
  • Security

Fingerprint Dive into the research topics of 'Algebra for quantitative information flow'. Together they form a unique fingerprint.

Cite this