Quantitative Information Flow in Boolean Programs.

The <italic>quantitative information flow bounding problem</italic> asks, given a program <italic>P</italic> and threshold <italic>q</italic>, whether the information leaked by <italic>P</italic> is bounded by <italic>q</italic>. When the amount of information is measured using mutual information, the problem is known to be PSPACE-hard and decidable in EXPTIME. We show that the problem is in fact decidable in PSPACE, thus establishing the exact complexity of the quantitative information flow bounding problem. Thus, the complexity of bounding quantitative information flow in programs has the same complexity as safety verification of programs. We also show that the same bounds apply when comparing information leaked by two programs. [ABSTRACT FROM AUTHOR]