Source-level reasoning for quantitative information flow

TL;DR

This paper introduces a formal system for reasoning about and proving quantitative information leakage in programs using gain-functions and source-level annotations, enabling precise security analysis.

Contribution

It presents a novel formal framework that models information leakage as a noisy channel and allows source-level reasoning with gain-expressions for complex adversarial scenarios.

Findings

Effective in analyzing small, intricate programs

Enables formal proofs of information flow properties

Supports general adversarial models through gain-expressions

Abstract

We present a novel formal system for proving quantitative-leakage properties of programs. Based on a theory of Quantitative Information Flow (QIF) that models information leakage as a noisy communication channel, it uses "gain-functions" for the description and measurement of expected leaks. We use a small imperative programming language, augmented with leakage features, and with it express adversaries' activities in the style of, but more generally than, the Hoare triples or expectation transformers that traditionally express deterministic or probabilistic correctness but without information flow. The programs are annotated with "gain-expressions" that capture simple adversarial settings such as "Guess the secret in one try." but also much more general ones; and our formal syntax and logic -based framework enables us to transform such gain-expressions that apply after a program has finished to ones that equivalently apply before the program has begun. In that way we enable a formal proof-based reasoning system for QIF at the source level. We apply it to the %programming language we have chosen, and demonstrate its effectiveness in a number of small but sometimes intricate situations.