A static analysis for quantifying information flow in a simple imperative language

Hunt, S., Clark, D. & Malacaria, P. (2007). A static analysis for quantifying information flow in a simple imperative language. Journal of Computer Security, 15(3), pp. 321-371.

Download (537kB) | Preview


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 L1 inequalities to provide reasonable bounds for conditional statements. While-loops are handled by integrating a qualitative flow-sensitive dependency analysis into the quantitative analysis.

Item Type: Article
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Divisions: School of Informatics > Department of Computing
School of Informatics > Centre for Software Reliability
URI: http://openaccess.city.ac.uk/id/eprint/195

Actions (login required)

View Item View Item


Downloads per month over past year

View more statistics