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.
| Language | English |
|---|---|
| Pages | 55-77 |
| Number of pages | 23 |
| Journal | Journal of Logical and Algebraic Methods in Programming |
| Volume | 106 |
| DOIs | |
| Publication status | Published - Aug 2019 |
Keywords
- Refinement
- Information flow
- Security
- Probabilistic semantics
- Compositional reasoning
- Dalenius Desideratum
Cite this
}
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 journal › Article › Research › peer-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 -