A Quantitative Analyser for Programs in a Core Imperative Language
This paper presents a tool for analyzing Quantified Information Flow (QIF) for programs written in a core imperative language. The intended application is measuring leakage of secrets. The tool can provide either exact leakage or an upper bound depending on the trade off chosen by the user between exactitude or computation speed. Approximations are created via abstractions derived from partitions on the initial store. The authors outline the workings of the tool and summarise results derived from running the tool on a range of example programs with either concrete or abstract initial stores.