A simulation-based proof technique for dynamic information flow
A simulation-based proof technique for dynamic information flow
复制标题
基于模拟的动态信息流证明技术
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Michael D. Ernst
中科院分区：
文献类型：
--
作者：
Stephen McCamant;Michael D. Ernst
信息流分析可以防止程序不正当地泄露秘密信息，动态方法可以使此类分析更实用，但验证此类分析是否合理的工作相对较少(考虑到给定执行中的所有流)。我们描述了一种新技术，用于证明端到端机密性等策略的动态信息流分析的可靠性。证明技术用一对程序副本来模拟被分析程序的行为：一个副本可以访问秘密信息，另一个负责输出。这两个副本通过有限带宽的通信通道连接，在该通道上传递的信息量限制了所披露的信息量，从而使其能够被量化。我们通过一个基于二进制工具的实用检查工具的模型来说明该技术，该工具以前没有被证明是可靠的
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