DTOS Program Summary

Overall DTOS Objectives

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.

• To develop a prototype of the lowest level software components in the Synergy architecture, the microkernel and the security server, improving upon the initial prototype of these components by the NSA.
• To provide assurance documentation and evidence that these components meet their security requirements, and more generally, to perform research addressing how to best provide evidence for the overall security of a system conforming with the Synergy architecture.

Prototype Objectives and Approach

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:

• Policy Flexibility The DTOS kernel should be capable of supporting a range of security policies, including mandatory access control policies such as a DoD multilevel security policy. To increase the ability to change between policies, system changes required by a change in policy should be localized within a single system component, the security server.
• Mach Compatibility The DTOS kernel should be capable of supporting all existing Mach applications, subject only to the restrictions of the security policy being enforced. In particular, if the security policy permits all operations, then existing Mach applications should run without change.
• Performance The performance of the DTOS kernel should be similar to that of the Mach kernel from which it is derived.

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

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:

• Requirements tracing
• Engineering process documentation
• Use of cleared personnel
• Code reviews
• Code assertions
• Type-safe programming languages
• Testing
• Formal mathematical proofs

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

• The DTOS prototype was successful as a proof of concept. While performance measurements are incomplete, the three design goals of the prototype were met sufficiently to demonstrate that, at the microkernel level, policy flexible security mechanisms need not be incompatible with other desired features.

• While the prototype was successful as a proof of concept, it also became clear during the program that the code base from which the DTOS prototype was developed is not a suitable code base for a secure, assured microkernel. The code is simply too complex and poorly structured to provide any meaningful assurance that it satisfies all of the required security properties.

• The DTOS program provided for distribution of the DTOS prototype and a NSA-developed secure operating system environment to several sites performing research under the Synergy program. These sites were able to use the operating system as a platform for developing other prototype elements of a flexible secure system.

• A demo was created to demonstrate an application satisfying a security policy specific to the application. The application relies upon a combination of security controls in the application and the security controls and services of the underlying platform.

• The results of the DTOS program have directly or indirectly influenced several other programs being conducted at Secure Computing. While none of these programs are specifically part of the Synergy program, they all have goals which will contribute to the overall success of the Synergy program.

• Because of the goal of policy flexibility in the prototype, it is important that security properties of the prototype be stated independent of any particular security policy. This allows any assurance evidence for the properties to be reused in distinct policy environments. The DTOS Formal Security Policy Model (FSPM) was written so that the basic security requirements on the DTOS prototype microkernel were stated in terms of security decisions retrieved from the security server, rather than in terms of specific security attributes of microkernel entities.

• The Synergy architecture emphasizes the use of multiple, interchangeable components. Therefore to provide assurance for a system constructed in this way, it is very desirable to be able to analyze the components individually and then easily combine the analysis to provide assurance evidence for the entire system. Using prior work by others as a base, a framework for composing assurance evidence of different system components was developed on the program. Worked examples of such an analysis were also conducted.

• One of the design goals of the prototype was policy flexibility. To consider the extent to which this goal was met, a framework was developed for evaluating the flexibility of a system with distinct policy decision making and enforcement components. This framework is general enough to apply to any system with an architecture providing a distinction between a policy decider and policy enforcers. It was applied specifically to the DTOS prototype to determine the range of policies supportable by DTOS. Results from this analysis were provided to the prototype effort to suggest ways to increase the range of supportable policies.

• The goal of policy flexibility similarly affects the covert channel analysis of the system. Ideally, covert channel properties can be stated independent of any security policy. Another important issue in covert channel analysis for a system built with the Synergy architecture is the ability to analyze the various servers independently.

  The DTOS program conducted several areas of research into theories and techniques for performing a covert channel analysis independent of a policy and within a multiserver architecture such as Synergy. A technique for performing analysis of a single server independent of a security policy was developed and demonstrated with a simple example. Properties of this technique and of traditional techniques were considered and some weaknesses common to each have been identified. Many open issues remain in this area.

• While the basic DTOS design was developed earlier on the DTMach program and had been subjected to considerable review, there are still other possible ways to meet the three basic design goals within a secure system implementing the Synergy architecture. A study was performed during the program to compare the security mechanisms and models provided by four other microkernel based secure systems. This study validated the approach taken by DTOS as providing the greatest policy flexibility and assurability, but also suggests some ways in which other mechanisms could potentially be incorporated into DTOS to provide further enhanced security.

• In any program such as Synergy which implements a long term strategy, it is important to record the results of each stage of the program to limit the tendency to repeatedly address the same issues. This Lessons Learned Report provides a comprehensive discussion of the various efforts undertaken on the program, including the significant contributions, methodology and lessons learned by each effort. This is expected to be valuable input to future elements of the Synergy program as they are undertaken.

• The long term goals of Synergy require involvement and interest within the research and commercial vendor communities. One vehicle for generating this interest is the presentation of papers at conferences. As part of the DTOS program, several papers were contributed to security and operating systems conferences, and four of these papers were accepted and presented.