jpf-qif : Quantitative Information Flow Analysis for Java Bytecode


Computer systems in the real world are never 100% secure, so we need to measure how secure they are. As a simple example, suppose an attacker tries to guess a password: if his guess is correct, he can obtain all the information; otherwise he can still learn that the password is not the same as the previous try, so his search space is narrowed. In either the cases, the password checking program does leak some information. The aim of this project is to use JPF to quantify leakage of confidential information in Java programs.


student: Quoc-Sang Phan <quoc.phan AT>

mentor: Oksana Tkachuk

co-mentor: Corina Pasareanu


The sources for this project are available from a Mercurial repository at


Project documentation/wiki/blog are available at

Last modified 6 years ago Last modified on 06/01/2012 02:26:38 PM