A simulation-based proof technique for dynamic information flow

Download: PDF, PostScript.

“A simulation-based proof technique for dynamic information flow” by Stephen McCamant and Michael D. Ernst. In PLAS 2007: ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, (San Diego, California, USA), June 14, 2007, pp. 41-46.

Abstract

Information-flow analysis can prevent programs from improperly revealing secret information, and a dynamic approach can make such analysis more practical, but there has been relatively little work verifying that such analyses are sound (account for all flows in a given execution). We describe a new technique for proving the soundness of dynamic information-flow analyses for policies such as end-to-end confidentiality. The proof technique simulates the behavior of the analyzed program with a pair of copies of the program: one has access to the secret information, and the other is responsible for output. The two copies are connected by a limited-bandwidth communication channel, and the amount of information passed on the channel bounds the amount of information disclosed, allowing it to be quantified. We illustrate the technique by application to a model of a practical checking tool based on binary instrumentation, which had not previously been shown to be sound.

Download: PDF, PostScript.

BibTeX entry:

@inproceedings{McCamantE2007,
   author = {Stephen McCamant and Michael D. Ernst},
   title = {A simulation-based proof technique for dynamic information flow},
   booktitle = {PLAS 2007: ACM SIGPLAN Workshop on Programming Languages
	and Analysis for Security},
   pages = {41--46},
   address = {San Diego, California, USA},
   month = {June~14,},
   year = {2007}
}

(This webpage was created with bibtex2web.)

Back to Program Analysis Group publications.