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.
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:
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.
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:
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.
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.