A simulation-based proof technique for dynamic information flow
Submitted by mernst on Wed, 2011-11-30 14:35
| Title | A simulation-based proof technique for dynamic information flow |
| Publication Type | Conference Paper |
| Year of Publication | 2007 |
| Authors | McCamant S, Ernst MD |
| Conference Name | PLAS 2007: ACM SIGPLAN Workshop on Programming Languages and Analysis for Security |
| Date or Month Published | June 14 |
| Conference Location | San Diego, California, USA |
| Abstract | <p>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.</p> |
| Downloads | PDF PostScript |
| Citation Key | McCamantE2007 |
Last changed Mon, 2013-06-03 10:27

cs.