12 - Quantitative Information Flow with Monads in Haskell

Summary

Monads are a popular feature of the programming language Haskell because they can model many different notions of computation in a uniform and purely functional way. Our particular interest here is the probability monad, which can be -- and has been -- used to synthesise models for probabilistic programming. Quantitative Information Flow, or QIF, arises when security is combined with probability, and concerns the measurement of the amount of information that 'leaks' from a probabilistic program's state to a (usually) hostile observer: that is, not 'whether' leaks occur but rather 'how much?' Recently it has been shown that QIF can be seen monadically, a 'lifting' of the probability monad so that programs become functions from distributions to distributions of distributions: the codomain is 'hyper distributions'. Haskell's support for monads therefore suggests a synthesis of an executable model for QIF. Here, we provide the first systematic and thorough account of doing that: using distributions of distributions to synthesise a model for Quantitative Information Flow in terms of monads in Haskell.