Program algebra for quantitative information flow

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

Research output: Contribution to journalArticle

Abstract

Models for quantitative information flow traditionally assume that the secret, once set, never changes. More recently, however, Hidden Markov Models (HMM's) have been used to describe program features that include both state updates and information flow, thus supporting more realistic contexts where secrets can indeed be refreshed.

In this paper we explore HMM's further, with the aim of bringing algebraic concepts to bear in the analysis of confidentiality properties of programs. Of particular importance is the idea that local reasoning about program fragments should remain sound even when those same fragments are executed within a larger system. We show how to extend the basic HMM model to incorporate this core idea within an algebraic setting and, in so doing, show how it is related to established notion about privacy and correlated data sets in statistical databases.

Using our algebra for an HMM-style model we show how to describe and prove some foundational properties of quantitative information flow.

Original languageEnglish
Pages (from-to)55-77
Number of pages23
JournalJournal of Logical and Algebraic Methods in Programming
Volume106
DOIs
Publication statusPublished - Aug 2019

Keywords

  • Refinement
  • Information flow
  • Security
  • Probabilistic semantics
  • Compositional reasoning
  • Dalenius Desideratum

Cite this