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 quantifies 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 systematically the state space. Symbolic Execution fits well with our framework, so we implement a method of QIF analysis employing Symbolic Execution. We develop our method as a prototype tool that can perform 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.
This is joint work with Pasquale Malacaria, Oksana Tkachuk and Corina S. Pasareanu.