SRC Technical Note 1997-032
SRC Technical Note 1997-032A classic problem in security is the problem of determining whether a given program has secure information flow. Informally, this problem may be described as follows: Given a program operating on public and private variables, check whether observations of the public variables before and after execution reveal any information about the initial values of the private variables. Although the problem has been studied for several decades, most of the previous approaches have been syntactic in nature, often using type systems and compiler data flow analysis techniques to analyze program texts. This paper presents a considerably different approach to checking secure information flow, based on a semantic characterization of security. A semantic approach has several desirable features. Firstly, it gives a more precise characterization of security than that possible by conservative methods based on type systems. Secondly, it applies to any programming constructs whose semantics are definable; for instance, nondeterminism and exceptions pose no additional problems. Thirdly, it can be applied to reasoning about indirect leaking of information through variations in program behavior (e.g., whether or not the program terminates). The method is also useful in the context of automated verification, since it can be used to develop a mechanically-assisted technique for checking whether the flow of a given program is secure.
Back to the SRC Technical Notes main page.