Static Analysis of Information Release in Interactive Programs

by Adedayo O. Adetoye, Nikolaos Papanikolaou
Abstract:
In this paper we present a model for analysing information release (or leakage) in programs written in a simple imperative language. We present the semantics of the language, an attacker model, and the notion of an information release policy. Our key contribution is the use of static analysis 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 programs; our example is taken from a known ?aw in versions of OpenSSH distributed with various Unix, Linux, and OpenBSD operating systems.
Reference:
Static Analysis of Information Release in Interactive Programs (Adedayo O. Adetoye, Nikolaos Papanikolaou), In Electronic Communications of the EASST, volume 35, 2010.
Bibtex Entry:
@ARTICLE{Adetoye2010,
  author = {Adedayo O. Adetoye and Nikolaos Papanikolaou},
  title = {Static Analysis of Information Release in Interactive Programs},
  journal = {Electronic Communications of the EASST},
  year = {2010},
  volume = {35},
  __markedentry = {[Nick]},
  abstract = {In this paper we present a model for analysing information release
	(or leakage) in programs written in a simple imperative language.
	We present the semantics of the language, an attacker model, and
	the notion of an information release policy. Our key contribution
	is the use of static analysis 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 programs; our example is taken from a known ?aw in versions
	of OpenSSH distributed with various Unix, Linux, and OpenBSD operating
	systems.},
  doi = {ISSN 1863-2122},
  keywords = {secure information release, static analysis, program veri?cation},
  owner = {nikos},
  timestamp = {2011.11.18},
  url = {../files/staticanalysis.pdf}
}