This work was motivated by a desire to provide better security when using downloaded applications, by making fine-grained information flow control practical and efficient. This paper is a first step towards this goal.
A key limitation of most multilevel security models is that there is a single, centralized policy on how information can flow. This kind of policy does not match well with the decentralized model in which each user is independent. Our model provides each user the ability to define information flow policy at the level of individual data items. Each user has the power to declassify his own data, but declassification does not leak other users' data.
An important aspect of our label model is that labels identify the owners, or sources, of the data. Each owner listed in the label maintains its own separate annotation (the reader set) to control where its data may flow. When running on behalf of a particular principal P, a program is able to edit P's portion of the label without violating other principals' policies. Labels form a familiar security class lattice, but each principal has access to some non-lattice relabelings (by declassifying).
We have also shown how the labels we define can be used to annotate a simple programming language, which suggests that other programming languages and intermediate code formats can be similarly annotated. To ensure proper information flows, the labels in the resulting code can be statically checked by the compiler, in a manner similar to type checking. Also, as part of the label checking process, the compiler can construct a trace of its checking process. Some form of this trace can accompany the generated code, and can be used later to verify information flows in the code.
Labels are mostly checked statically, which has benefits in space and time. Compiled code does not need to perform checks, so the code is shorter and faster than with run-time checks. Storage locations that are statically typed require no extra space to store a label. However, we have also defined a mechanism for run-time label checking that allows the flexibility of run-time checks when they are truly needed. This mechanism guarantees that when the run-time checks fail, information is not leaked by their failure. The mechanism of implicit label polymorphism also extends the power of static analysis, by allowing the definition of code that is generic with respect to some or all of the labels on its arguments. We have presented a simple algorithm that, despite our extensions to the label system, is able to efficiently infer labels for basic blocks and local variables. Label inference makes the writing of label-safe code significantly less onerous.
We have provided some simple examples of code and software designs that cannot be adequately expressed using previous models of access control or information flow. These examples demonstrate that the new features of user declassification, label polymorphism, and run-time label checking add new power and expressiveness in capturing security policies.
Next: 9 Future Work Up: A Model for Decentralized Previous: 7 Related Work
Andrew C. Myers, Barbara Liskov
Copyright ©1997 by the Association for Computing Machinery