Quantitative Information Flow - Verification Hardness and Possibilities

Date Added: May 2010
Format: PDF

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, and channel capacity. This paper investigates the hardness and possibilities of precisely checking and inferring quantitative information flow according to such definitions. The authors prove that, even for just comparing two programs on which has the larger flow, none of the definitions is a k safety property for any k, and therefore is not amenable to the self-composition technique that has been successfully applied to precisely checking non-interference.