Source-level reasoning for quantifying information leaks

Information-leak analysis for programs designates certain variables as “high security”, i.e. that should not be directly readable by an adversary; the aim then is to show that execution of the program does not allow their values even to be inferable, that is even if they are not read directly. For probabilistic programs in particular, “information entropies” measure the adversary’s uncertainty about high-security variables. A decrease in entropy, as the program executes, indicates that information has leaked—so revealing a possible (undesired) inference. 

This paper addresses the challenge of formal probabilistic information-flow analysis in the style above, “formal” in the sense that the reasoning is carried out entirely at the source level: both of the program text and in the description of the possible information flows. 

We present that analysis via a novel extension to an extant expectation-based logic for probabilistic programs. The extension can express many entropy-like functions, and we show how backwards reasoning –in the familiar post-to-pre style– when applied to entropies can produce sophisticated predictions of how damaging any unwanted leaks can be.