Program algebra for quantitative information flow

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

Research output: Contribution to journalArticleResearchpeer-review

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.

LanguageEnglish
Pages55-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

@article{ace82e6a83c446338c4b36abec097962,
title = "Program algebra for quantitative information flow",
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.",
keywords = "Refinement, Information flow, Security, Probabilistic semantics, Compositional reasoning, Dalenius Desideratum",
author = "McIver, {A. K.} and Morgan, {C. C.} and T. Rabehaja",
year = "2019",
month = "8",
doi = "10.1016/j.jlamp.2019.04.002",
language = "English",
volume = "106",
pages = "55--77",
journal = "Journal of Logical and Algebraic Methods in Programming",
issn = "2352-2216",
publisher = "Elsevier",

}

Program algebra for quantitative information flow. / McIver, A. K.; Morgan, C. C.; Rabehaja, T.

In: Journal of Logical and Algebraic Methods in Programming, Vol. 106, 08.2019, p. 55-77.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - Program algebra for quantitative information flow

AU - McIver, A. K.

AU - Morgan, C. C.

AU - Rabehaja, T.

PY - 2019/8

Y1 - 2019/8

N2 - 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.

AB - 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.

KW - Refinement

KW - Information flow

KW - Security

KW - Probabilistic semantics

KW - Compositional reasoning

KW - Dalenius Desideratum

U2 - 10.1016/j.jlamp.2019.04.002

DO - 10.1016/j.jlamp.2019.04.002

M3 - Article

VL - 106

SP - 55

EP - 77

JO - Journal of Logical and Algebraic Methods in Programming

T2 - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

SN - 2352-2216

ER -