Dynamic Security Labels and Noninterference

Abstract

This paper explores information flow control in systems in which the security classes of data can vary dynamically. Information flow policies provide the means to express strong security requirements for data confidentiality and integrity. Recent work on security-typed programming languages has shown that information flow can be analyzed statically, ensuring that programs will respect the restrictions placed on data. However, real computing systems have security policies that vary dynamically and that cannot be determined at the time of program analysis. For example, a file has associated access permissions that cannot be known with certainty until it is opened. Although one security-typed programming language has included support for dynamic security labels, there has been no examination of whether such a mechanism can securely control information flow. In this paper, we present an expressive languagebased mechanism for securely manipulating dynamic security labels. The mechanism is presented both in the context of a Java-like programming language and, more formally, in a core language based on the typed lambda calculus. This core language is expressive enough to encode previous dynamic label mechanisms; as importantly, any well-typed program is provably secure because it satisfies noninterference. 1