Next: 2 Motivating Examples Up: A Model for Decentralized Previous: A Model for Decentralized

1 Introduction

The common models for computer security are proving inadequate. Security models have two goals: preventing accidental or malicious destruction of information, and controlling the release and propagation of that information. Only the first of these goals is supported well at present, by security models based on access control lists or capabilities (i.e., discretionary access control, simply called ``access control'' from this point on). Access control mechanisms do not support the second goal well: they help to prevent information release but do not control information propagation. For example, if user A is allowed to read B's data, B cannot control how A distributes the information it has read. Control of information propagation is supported by existing information flow and compartmental models, but these models unduly restrict the computation that can be performed. The goal of this work is to make information flow control more useful by relaxing these restrictions.

Information flow control is vital for large or extensible systems. In a small system, preventing improper propagation of information is easy: you don't pass data to code whose implementation is not completely trusted. This simple rule breaks down in larger systems, because the trust requirement is transitive: any code the data might travel to must also be trusted, requiring complete understanding of the code. As the system grows larger and more complex, and incorporates distrusted code (e.g., web applications), complete trust becomes unattainable.

Systems that support the downloading of distrusted code are particularly in need of a better security model. For example, Java [GJS96] supports downloading of code from remote sites, which creates the possibility that the downloaded code will transfer private data to those sites. Java attempts to prevent these transfers by using a compartmental security model, but this approach largely prevents applications from sharing data. Also, different data manipulated by an application have different security requirements. A security model is needed that supports fine-grained information sharing between distrusted applications, while reducing the potential for information leaks.

This paper contains exploratory work towards a new model of decentralized information flow that is also inexpensive in both space and time. Our model allows users to control the flow of their information without imposing the rigid constraints of a traditional multilevel security system. The goal of this model is to provide security guarantees to users and to groups rather than to a monolithic organization. It differs from previous work on information flow control by allowing users to explicitly declassify (or downgrade) data that they own. When data is derived from several sources, all the sources must agree to release the data.

Like some existing information flow models [DD77, AR80], our model can largely be checked statically. We define user-supplied program annotations, called labels, that describe the allowed flow of information in a program. Annotated programs can be checked at compile time, in a manner similar to type checking, to ensure that they do not violate information flow rules. Compile-time checks have no run-time overhead in space or time, and unlike run-time checks, when they fail, they do not leak information about the data the program is using.

Our work extends existing models by allowing individuals to declassify data they own, rather than requiring a central authority to do it. In addition, we extend the static checking model in three ways. First, we introduce an implicit form of parametric polymorphism, called label polymorphism, to express procedures that are parametric with respect to the security labels of their arguments, and with respect to the principal on whose behalf the procedure executes. Label polymorphism extends the power of static analysis, and allows programmers to write generic code. Second, since purely static analysis would be too limiting for structures like file systems, where information flow cannot be verified statically, we define a new secure run-time escape hatch for these structures, with explicit run-time label checks. Uses of the run-time information flow mechanism are still partially verified statically, to ensure that they do not leak information. Third, we show that despite these features, the labels of local variables can be inferred automatically, easing the job of adding flow annotations to a program.

Our goal in exploring these techniques is to eventually support the following useful applications:

The annotations could be used to extend many conventional programming languages, intermediate code (such as JVM [LY96]), or machine code, where the labeling system defined here makes a good basis for security proofs [Nec97]. Labeled machine code and security proofs could work together: proof annotations for object code would be generated as a byproduct of compiling a program that contains information flow annotations.

The remainder of the paper describes the model and how checking is done. The model is intended to control covert and legitimate storage channels; it does not deal with timing channels, which are harder to control. The work assumes the existence of a reliable, efficient authentication mechanism, and of a trusted execution platform; for example, code may be executed by a trusted interpreter, or generated only by a trusted compiler. When the computational environment contains many trusted nodes connected by a network, the communication links beween the nodes must be trusted, which can be accomplished by encrypting communication between nodes.

The organization of the remainder of this paper is as follows. Section 2 briefly describes some systems that can benefit from decentralized information flow control, and which are not well supported by existing models. Section 3 introduces the fundamentals of the new information flow control model. Section 4 discusses issues that arise when code using the new model is statically checked for correctness. Section 5 shows how the model can be integrated into a simple programming language. Section 6 shows how to infer most labels in programs automatically, making the job of annotating a program much simpler. Section 7 describes related work in the areas of information flow models, access control, and static program analysis. We conclude in Section 8 and discuss future work in Section 9.

Next: 2 Motivating Examples Up: A Model for Decentralized Previous: A Model for Decentralized

Andrew C. Myers, Barbara Liskov

Copyright ©1997 by the Association for Computing Machinery