TY - GEN
T1 - A simulation-based proof technique for dynamic information flow
AU - McCamant, Stephen
AU - Ernst, Michael D.
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
KW - Dynamic analysis
KW - Implicit flow
KW - Information-flow analysis
UR - http://www.scopus.com/inward/record.url?scp=36448929074&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=36448929074&partnerID=8YFLogxK
U2 - 10.1145/1255329.1255336
DO - 10.1145/1255329.1255336
M3 - Conference contribution
AN - SCOPUS:36448929074
SN - 1595937110
SN - 9781595937117
T3 - PLAS'07 - Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security
SP - 41
EP - 46
BT - PLAS'07 - Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security
T2 - PLAS'07 - 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security
Y2 - 14 June 2007 through 14 June 2007
ER -