The foundation for security enforcement is access control.Resources must be protected against access by unauthorized entities.Furthermore, authorized entities must be prevented from accessing resources in inappropriate ways.A major challenge to the developer of an access control policy is to provide users the flexibility to protect their resources as they see fit; system policies that am inconsistent with user needs are inadequate.In particular, systems that enforce a single, hard-coded policy cannot satisfy the needs of all users.As part of the Distributed Trusted Operating System (DTOS) program, we have developed and implemented a flexible security architecture using the Mach microkemel.In this architecture, the security rules enforced by the system are defined by a system component outside the microkemel.This reduces the problem of sup porting other security policies to redefining this system component; the same microkemel can be used to support a wide range of policies.Formal methods were used to provide a rigorous approach for the development of the policy.Recognizing that most people are uninterested in reading security requirements stated in formal specification languages, an approach was developed for representing and maintaining the policy in a tabular format.This paper describes the flexibility of the DTOS security architecture and the approach used in developing the access control policy for this flexible architecture.It also gives examples of how to detine a component that makes security decisions for the microkernel.''This work was suppxted in patt by the Maryland F'mcurement Office, contract MDA904-93C-4209 and was performed in cooperation with mscarchers at the Information Security Computer Science Rcseaxh Division of the Department of Jkfense.

Covert channels are a critical concern for multilevel secure (MLS) systems. Due to their subtlety, it is desirable to use formal methods to analyze MLS systems for the presence of covert channels. This paper describes an approach for using Abadi & Lamport's (1993) temporal logic of actions (TLA) to specify noninterference properties. In addition to providing a more intuitive definition of noninterference than previous attempts, this approach also supports the analysis of systems that do contain covert channels to demonstrate limitations on their exploitations. In relating the definition of noninterference given in this paper to prior definitions of noninterference, this paper discusses ways in which other definitions of noninterference can be formalized in TLA, too. Finally, this paper discusses how prior work on specification refinement and composition might be applied to the noninterference problem within the framework provided by TLA.

Distributed Trusted Mach (DTMach) is an operating system designed by Secure Computing Corporation. The goal of the project is to use the Mach 3.0 kernel as the base for a secure, distributed system. As a first step in developing the DTMach security policy, a categorization of general security concerns was constructed. Concerns that were not adequately addressed by the Mach 3.0 kernel indicated potential security vulnerabilities. The authors describe these general security concerns, the manner in which the Mach 3.0 kernel addresses each concern, and the manner in which DTMach addresses each concern. The focus is on the DTMach security policy and security mechanisms. It is first necessary to identify the general threats against which DTMach must protect. The next step is to identify control mechanisms that are sufficient to protect against each of the threats. The DTMach design makes extensive use of type enforcement in addressing the threats. The general threats and the countermeasures provided by DTMach are described, which provide more evidence of the usefulness of type enforcement in general and the high assurance provided by the DTMach type of enforcement policy.>

An algorithm that can be used to construct a definition of state equivalence that is meaningful in a security context is discussed. It the algorithm is followed, then at the completion of the algorithm, it has either been demonstrated that the system is secure in the sense that there can be no information flow from a higher level to a lower level, or an exploitation scenario for a covert channel has been demonstrated. The algorithm incrementally builds the definition of the equivalence relation in such a way that no effort is wasted. It allows for extensions to easily be made to the system without invalidating earlier work. Although it is generally thought that a noninterference analysis requires a verification environment, an informal analysis can still be performed without such an environment. This might result in slightly less confidence in the proofs, but it can save time. By doing this, one can analyze operations as they are being designed and errors can be corrected before they become entrenched in the system. When this point is reached, the security analysis will become a useful subtask of designing the system instead of an afterthought.>

The LOCK noninterference policy for analyzing security properties of systems is presented. An unwinding theorem is developed. Difficulties resulting from trying to apply an abstract noninterference policy to a real system are discussed. A comparison is made between the LOCK noninterference policy and other versions of noninterference.>