A Program Transformation Technique for Enforcement of Information Flow Properties ∗
msra(2004)
Abstract
With the ever-increasing presence of confidential data on the Internet, allowing such data to be processed while protecting it from leakage to unauthorized parties is a major concern. Mechanisms which can automatically track the flow of information in programs and prevent leaks have the potential for securing confidential data and have been a major focus of interest within the security community. Unfortunately, it is well known that policies restricting the flow of information during the execution of a program are not enforceable using traditional runtime enforcement mechanisms, which only consider the particular execution path taken by a program at runtime. This is because information flow depends not only on the execution path, but also on so-called implicit flows, some of which are generated by unexercised execution paths. As a result, recent research in the area of information flow policy enforcement has focused primarily on purely static techniques, which can consider all execution paths. The drawback of such approaches is that they can be overly conservative and thereby lose precision, resulting in rejection of legal programs. A natural way to improve precision is to augment static analysis with runtime checking. In this paper, we show that by using static analysis to gather information about potential implicit flows, and by combining this information with runtime checking techniques, more precise information flow tracking is possible. The approach is inherently more precise than purely static approaches, as it considers only the current execution path and its relation to the unexercised paths, whereas static approaches must consider all potential paths. A proof is given which establishes the soundness of the approach with respect to the noninterference property [7], which is the standard criteria for establishing the soundness of information flow policy enforcement techniques.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined