Affiliations: [a] Department of Computer Science, Kings College, London, UK. E-mail: david@dcs.kcl.ac.uk | [b] Department of Computing, City University, London, UK. E-mail: seb@soi.city.ac.uk | [c] Department of Computer Science, Queen Mary, London, UK. E-mail: pm@dcs.qmul.ac.uk
Abstract: We propose an approach to quantify interference in a simple imperative language that includes a looping construct. In this paper we focus on a particular case of this definition of interference: leakage of information from private variables to public ones via a Trojan Horse attack. We quantify leakage in terms of Shannon’s information theory and we motivate our definition by proving a result relating this definition of leakage and the classical notion of programming language interference. The major contribution of the paper is a quantitative static analysis based on this definition for such a language. The analysis uses some non-trivial information theory results like Fano’s inequality and the L1 inequality to provide reasonable bounds for conditional statements. While-loops are handled by integrating a qualitative flow-sensitive dependency analysis into the quantitative analysis.
Keywords: Security, program analysis, static analysis, confidentiality, information flow, measurement, information theory, quantify interference, while language, leakage
