London † Carnegie Mellon Silicon Valley,

In recent work we have proposed a software reliability analy-sis technique that uses symbolic execution and model count-ing to quantify the probability of reaching designated pro-gram states, e.g. assert violations, under uncertainty con-ditions in the environment. The technique has many ap-plications beyond reliability analysis, ranging from program understanding and debugging to analysis of cyber-physical systems. In this paper we report on a novel application of the technique, namely Quantitative Information Flow anal-ysis (QIF). The goal of QIF is to measure information leak-age of a program by using information-theoretic metrics such as Shannon entropy or Rényi entropy. We exploit the model counting engine of the reliability analyser over sym-bolic program paths, to compute an upper bound of the maximum leakage over all possible distributions of the con-fidential data. We have implemented our approach into a prototype tool, called QILURA, and explore its effectiveness on a number case studies. 1