Precise Quantitative Information Flow Analysis Using Symbolic Model Counting
Vladimir Klebanov · 2012
Abstract. Quantitative information flow analyses (QIF) are a class of techniques for measuring the amount of confidential information leaked by a program to its public outputs. QIF analyses can be approximative or precise, offering different trade-offs. In this paper, we lift a particular limitation of precise QIF. We show how symbolic model counting replaces explicit leak enumeration with symbolic computation, thus eliminating the associated bottleneck. 1