| 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 |
| Pagination | 41–46 |
| Date or Month Published | June |
| Conference Location | San Diego, California, USA |
| 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. |
| Downloads | https://groups.csail.mit.edu/pag/pubs/infoflow-proof-plas2007.pdf PDF
|
| Citation Key | McCamantE2007 |
