Protecting information has become very important due to the safety-critical nature of many computer-based applications. The information flow analysis plays a very important role in quantifying information-related properties under external attacks. Traditionally, information flow analysis is performed using paper-and-pencil based proofs or computer simulations but due to their inherent nature, these meth- ods are prone to errors and thus cannot guarantee accurate analysis. As an accurate alternative, we propose to conduct the information flow analysis within the sound core of a higher-order-logic theorem prover. For this purpose, some of the most commonly used information flow measures, including Shanon entropy, mutual information, min-entropy, belief min-entropy, have been formalized. We use the Shannon entropy and mutual information formalizations to formally verify the Data Processing and Jensen’s inequalities. Moreover, we formalize the gain min-entropy for the case of the partial guess scenario. These formalizations allow us to to reason about information flow of a wide range of systems within a theorem prover. For illustration purposes, we performed a formal comparison between the min-entropy leakage and the gain leakage.
Keywords: Information Flow, Entropy, Gain Function, g-Leakage, Theorem Proving, Higher-order Logic.

HOL Scripts

Foundational Formalization

• min-belief-gainTheo.sml (This file contains formalization of Min-Entropy, Belief Min-Entropy and Gain Min-Entropy theories) (Ghassen Helali)
• DPI_Jensen.sml (This file contains formalization of the Data Processing and the Jensen's inequalities properties) (Cvetan Dunchev)

Applications

• gainCascChann.sml (This file contains the formal verification of the two proposed applications: Comparing Min-Entropy Leakage and Gain Leakage + information leakage of a Cascade of Channels) (Ghassen Helali)