  Researchers have proposed formal definitions of quantitative information flow
based on information theoretic notions such as the Shannon entropy, the min
entropy, the guessing entropy, belief, and channel capacity. This paper
investigates the hardness of precisely checking the quantitative information
flow of a program according to such definitions. More precisely, we study the
"bounding problem" of quantitative information flow, defined as follows: Given
a program M and a positive real number q, decide if the quantitative
information flow of M is less than or equal to q. We prove that the bounding
problem is not a k-safety property for any k (even when q is fixed, for the
Shannon-entropy-based definition with the uniform distribution), and therefore
is not amenable to the self-composition technique that has been successfully
applied to checking non-interference. We also prove complexity theoretic
hardness results for the case when the program is restricted to loop-free
boolean programs. Specifically, we show that the problem is PP-hard for all
definitions, showing a gap with non-interference which is coNP-complete for the
same class of programs. The paper also compares the results with the recently
proved results on the comparison problems of quantitative information flow.
