A Tool: Quantitative Analyser for Programs

This paper presents a tool for analysing 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 and computation speed. Approximations are created via abstractions derived from partitions on the initial store. We 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.