A simulation-based proof technique for dynamic information flow

Stephen McCamant, Michael D. Ernst

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationPLAS'07 - Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security
Pages41-46
Number of pages6
DOIs
StatePublished - Nov 30 2007
EventPLAS'07 - 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security - San Diego, CA, United States
Duration: Jun 14 2007Jun 14 2007

Publication series

NamePLAS'07 - Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security

Other

OtherPLAS'07 - 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security
CountryUnited States
CitySan Diego, CA
Period6/14/076/14/07

Keywords

  • Dynamic analysis
  • Implicit flow
  • Information-flow analysis

Fingerprint Dive into the research topics of 'A simulation-based proof technique for dynamic information flow'. Together they form a unique fingerprint.

  • Cite this

    McCamant, S., & Ernst, M. D. (2007). A simulation-based proof technique for dynamic information flow. In PLAS'07 - Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (pp. 41-46). (PLAS'07 - Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security). https://doi.org/10.1145/1255329.1255336