DTOS Program Summary

Overall DTOS Objectives
Prototype Objectives and Approach
Assurance Objectives and Approach
Significant Results and Accomplishments

Overall DTOS Objectives

The DTOS program was part of a broad operating systems research program by the NSA known as Synergy, the objective of which was to develop a flexible, microkernel-based architecture for secure distributed systems. The Synergy efforts were part of a long term strategy to encourage operating system vendors to include strong security mechanisms in the next generation of commercially available operating systems.

An initial element of this strategy was to develop a prototype which could be used to demonstrate the feasibility of including strong security mechanisms without sacrificing other desirable features. The prototype was also intended to be used as a platform for further research into other components of the Synergy architecture.

Under the DTOS program, Secure Computing Corporation was tasked with addressing two of the basic needs of the Synergy program.

Each of these is discussed in a separate section below.

Prototype Objectives and Approach

DTOS is a successor to the DTMach program, which produced a high-level design for a secure distributed operating system and an initial NSA-developed prototype of the microkernel security enhancements and a separate security server. The DTOS prototype effort by Secure Computing Corporation was almost exclusively limited to two components in this design, the microkernel and the security server. The NSA developed security enhancements to the Lites Unix server to provide a secure operating system environment.

The microkernel was designed as a collection of enhancements to the existing Mach~3.0 design. One purpose of starting from an existing microkernel was to demonstrate that security need not be incompatible with other desired features. The Mach microkernel itself was chosen for a variety of reasons, including its acceptance within the research and commercial operating systems communities and because source code to a Mach implementation was available, from Carnegie Mellon University (CMU), without restrictive licensing agreements.

The security server embodies the system's security policy. Its main function is to provide security decisions which are enforced by other service-providing components such as the microkernel. These policy enforcing servers query the security server for decisions during processing at certain well-defined control points.

The separation of policy decision making, performed in the security server, from policy enforcement, performed in other object servers, is a fundamental property of the Synergy architecture. It encourages flexibility so that those other servers can be reused in many different policy environments.

The design goals of the prototype effort were the following:

Comparing these to the goals of the Synergy program, the first goal emphasizes one instance of the flexibility which is important to Synergy, while the second and third goals aim to demonstrate that security mechanisms need not be incompatible with other features of a commercial operating system.

In addition to these three design goals, the other important goal for the DTOS prototype was that it be made available to any interested researcher, in particular, researchers involved in other Synergy related projects.

Assurance Objectives and Approach

It is not enough that a system is declared to be ``secure''. An individual responsible for evaluating a system for a particular use requires evidence that the system will actually meet the security needs of the users. We use the term assurance to refer to this evidence and the process of developing the evidence. Assurance evidence consists of two elements; a statement of the security properties that a system is claimed to satisfy, and some kind of argument that the system actually does satisfy those properties.

The statement of a system's security properties is generally done at a high level, so that they are relevant to users of the system. For instance, a security property of an operating system used for classified information might be that the system prevents a user from accessing data for which the user is not cleared.

On the other hand, the assurance argument often involves specification of the system at multiple levels of abstraction between the high level statement of the security properties and the actual implementation. Verification evidence is presented to justify that the specification at each level meets the requirements of the next highest level. Common forms of verification evidence include the following:

For the DTOS program, the primary goal of the assurance efforts is to perform research for assurance of systems constructed following the Synergy architecture. The particular aspects of this architecture with which the efforts are most concerned are security policy independence, decider/enforcer separation and modularity of the multiserver architecture. This research considered techniques for developing assurance evidence and for documenting and presenting the evidence. In most cases, the research was performed independent of the DTOS prototype, however, the prototype was often used to demonstrate the effectiveness (or ineffectiveness) of assurance techniques.

The DTOS research was strongly influenced by the use of formal mathematical methods. Formal mathematical theories were used as a basis for verification evidence and formal mathematical languages are used throughout the documentation. The only significant task which did not rely on formal methods was the Specification to Code analysis task, which is essentially a highly structured code review.

One drawback of this reliance on formal methods is that formal languages are often a barrier to the use of assurance documentation. To avoid this, an emphasis was placed on minimizing the reliance upon formal languages to only those situations when the corresponding English statements contained possible ambiguities. In particular, formal languages are considered as an enhancement to the English language rather than a replacement for it.

The emphasis on formal methods on DTOS is not an indication that the other forms of verification evidence are perceived to have no value. On the contrary, all of the listed techniques are valuable components of an overall assurance argument. Formal methods do however provide the strongest guarantee of completeness in an assurance argument. Completeness is especially important when verifying security properties, when even a single failure can have potentially devastating consequences. This is reflected in the TCSEC, where the only distinction between the highest rating (A1) and the second highest rating (B3) is the extent to which formal methods are used for system verification.

Significant Results and Accomplishments

DTOS Home Page
This page is currently being maintained by: Stephen Smalley.
Last Modified: 20 Dec 2000