Leakage of confidential information represents a serious security risk.
Despite a number of novel, theoretical advances, it has been unclear if and how
quantitative approaches to measuring leakage of confidential information could
be applied to substantial, real-world programs. This is mostly due to the high
complexity of computing precise leakage quantities. In this paper, we introduce
a technique which makes it possible to decide if a program conforms to a
quantitative policy which scales to large state-spaces with the help of bounded
model checking.