Symbolic quantitative information flow

Quantitative Information Flow (QIF) is a powerful approach to quantify leaks of confidential information in a software system. Here we present a novel method that precisely quan-tifies information leaks. In order to mitigate the state-space explosion problem, we propose a symbolic representation of data, and a general SMT-based framework to explore sys-tematically the state space. Symbolic Execution fits well with our framework, so we implement a method of QIF anal-ysis employing Symbolic Execution. We develop our method as a prototype tool that can per-form QIF analysis for a software system developed in Java. The tool is built on top of Java Pathfinder, an open source model checking platform, and it is the first tool in the field to support information-theoretic QIF analysis