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

David Clark, Sebastian Hunt, Pasquale Malacaria

Research output: Contribution to journalArticlepeer-review

144 Citations (Scopus)

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 ℒ 1 inequality to provide reasonable bounds for conditional statements. While-loops are handled by integrating a qualitative flow-sensitive dependency analysis into the quantitative analysis.
Original languageEnglish
Pages (from-to)321-371
Number of pages51
JournalJournal of Computer Security
Volume15
Issue number3
Publication statusPublished - 2007

Fingerprint

Dive into the research topics of 'A static analysis for quantifying information flow in a simple imperative language'. Together they form a unique fingerprint.

Cite this