Trustworthy Systems

Abstract hidden markov models: A monadic account of quantitative information flow


Carroll Morgan, Annabelle McIver and Tahiry Rabehaja


Macquarie University

UNSW Sydney


Hidden Markov Models, HMM's, are mathematical models of Markov processes with state that is hidden, but from which information can leak. They are typically represented as 3-way joint-probability distributions. We use HMM's as denotations of probabilistic hidden-state sequential programs: for that, we recast them as "abstract" HMM's, computations in the Giry monad $\Dist$, and equip we them with a partial order of increasing security. However to encode the monadic type with hiding over some state X we use DX->D^2X rather than the conventional X->DX that suffices for Markov models whose state is not hidden. We illustrate the DX->D^2X construction with a small Haskell prototype. We then present uncertainty measures as a generalisation of the extant diversity of probabilistic entropies, with characteristic analytic properties for them, and show how the new entropies interact with the order of increasing security. Furthermore, we give a "backwards" uncertainty-transformer semantics for HMM's that is dual to the "forwards" abstract HMM's --- it is an analogue of the duality between forwards, relational semantics and backwards, predicate-transformer semantics for imperative programs with demonic choice. Finally, we argue that, from this new denotational-semantic viewpoint, one can see that the Dalenius desideratum for statistical databases is actually an issue in compositionality. We propose a means for taking it into account.

BibTeX Entry

    author           = {Morgan, Carroll and McIver, Annabelle and Rabehaja, Tahiry},
    date             = {2019-3-31},
    issue            = {1},
    journal          = {Mathematical Structures in Computer Science},
    month            = mar,
    pages            = {36:1-36:50},
    paperurl         = {},
    publisher        = {Cambridge University Press},
    title            = {Abstract hidden Markov models: a monadic account of quantitative information flow},
    volume           = {15},
    year             = {2019}