Static Analysis of Information Release in Interactive Programs

In this paper we present a model for analysing information release (or leakage) in programs written in a simple imperative language. We present the se- mantics of the language, an attacker model, and the notion of an information release policy. Our key contribution is the static analysis technique to compute information release of programs and to verify it against a policy. We demonstrate our approach by analysing information released to an attacker by faulty password checking pro- grams; our example is inspired by a known flaw in versions of OpenSSH distributed with various Unix, Linux, and OpenBSD operating systems.