In both secure and safety-critical systems it is desirable to have a very clear relationship between the system's mandatory security policy and its proven operational semantics. This relationship is made clearer if the system architecture provides strong separation between the enforcement mechanisms and the policy decisions, and if the policy decision software is clearly identifiable in the system's architecture.
This paper describes a prototype Unix system based on Mach which provides mandatory control over all kernel-supported operations. The prototype work modified the Mach kernel by extending its limited control mechanisms based on the Mach port right. The control extensions allow a mandatory control policy to specify control over not only access to an object via a port right, but over the individual services supported by the object. The mandatory security policy is implemented in an external Security Server which provides very strong separation between policy enforcement and policy decision software. This makes it possible to support a wide range of security policies with no change to the kernel or applications.
Full paper available as a postscript file (170K), or as a pdf file (120K).
The foundation for security enforcement is {\em 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 are 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 microkernel. In this architecture, the security rules enforced by the system are defined by a system component outside the microkernel. This reduces the problem of supporting other security policies to redefining this system component; the same microkernel 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 define a component that makes security decisions for the microkernel.
Full paper available as a postscript file (120K), or as a pdf file (131K).
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 Lamport's TLA to specify noninterference properties. In addition to providing a more intuitive definition of noninterference than previous attempts, this approach also supports analysis of systems that do contain covert channels to demonstrate limitations on their exploitations. In relating the definition of noninterference given here 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.
Full paper available as a postscript file (110K), or as a pdf file (125K).
Analysis of complex systems requires the use of a ``divide-and-conquer'' approach to specification and verification. Existing theories for specification composition provide a starting point for a framework for such an approach. This paper describes a new framework that is a hybrid of two existing frameworks, explains the advantages of the new framework, and illustrates its use through a simple example.
Full paper available as a postscript file (130K), or as a pdf file (157K).