A semantic approach to secure information flow

A classic problem in security is that of checking that a program has secure information flow. informally, this problem is described as follows: Given a program with variables partitioned into mio disjoint sets of "high-securi ty" and "low-security" variables, check whether observations of the low-sec urity variables reveal any information about the initial values of the high -security variables. Although the problem has been studied for serveral dec ades, most previous approaches have been syntactic in nature, often using t ype systems and compiler data flow analysis techniques to analyze program t exts. This paper presents a considerably different approach to check secure information flow, based on a semantic characterization. A semantic approac h has several desirable features. Firstly, it gives a more precise characte rization of security than that provided by most previous approaches. Second ly, it applies to any programming constructs whose semantics are definable; for instance, the introduction of nondeterminism and exceptions poses no a dditional problems. Thirdly, it can be used for reasoning about indirect le aking of information through variations in program behavior (e.g., whether or not the program terminates). Finally, it can be extended to the case whe re the high- and low-security variables are defined abstractly, as function s of actual program variables. The paper illustrates the use of the charact erization with several examples and discusses how it can be applied in prac tice. (C) 2000 Elsevier Science B.V. All rights reserved.