DTOS Technical Reports

Final Report

• DTOS Lessons Learned Report [ Postscript ] [ PDF ]
  This report includes the final report for the DTOS program and provides an overview of all of the technical efforts on the program. It describes significant accomplishments and obstacles encountered during these efforts and lessons learned while carrying out the program. Finally, it provides suggestions for future efforts which build upon the successes of the program or address deficiencies.

Prototype Documentation

• DTOS Kernel Interface Document [ Postscript ] [ PDF ]
  This document defines the interfaces to the prototype kernel and security server. It is based upon the OSF KID for the OSF MK14 version of the kernel. In addition to defining the data structures visible at the interface, the KID defines the privileges required to be held by users of each interface.
• DTOS Users Manual [ Postscript ] [ PDF ]
  This document is the user's manual for the DTOS prototype system. It provides background concepts, procedures, and reference information needed for installing and using the DTOS prototype. It should be consulted by anyone who plans to use the DTOS system.

Assurance-Formal Specifications of DTOS

• DTOS Formal Security Policy Model (FSPM) [ Postscript ] [ PDF ]
  This document defines the security policy enforced by the DTOS prototype kernel. The policy is defined formally using the Z specification language. The FSPM begins with a brief description of the Mach kernel data structures and then describes new kernel data structures required by the DTOS design; these data structures are used to identify the services provided by the DTOS kernel. Security requirements are stated governing when each service may be provided, in terms of permissions granted by the security server.
• English-only Version of the FSPM [ Postscript ] [ PDF ]
  This document is a version of the FSPM which does not include any formal specification, just english descriptions.
• DTOS Formal Top-Level Specification [ Postscript ] [ PDF ]
  This document provides a partial formal specification of the DTOS microkernel. It describes the system behavior both in English and in the Z specification language.

Assurance-Research Tasks

• DTOS Generalized Security Policy Specification [ Postscript ] [ PDF ]
  This document analyzes the policy flexibility of the DTOS architecture and records insights into the effect that the goal of policy flexibility has on the design of an object manager and its interface with the rest of the system. The report first surveys a variety of security policies from the computer security literature. It then gives a general framework for modeling a system in which security enforcement is separated from the making of security decisions. The DTOS kernel and security servers for several example policies are specified within this framework and the resulting systems analyzed. The report also identifies a list of policy characteristics and classifies a variety of policies with respect to these characteristics.
• DTOS Composability Study [ Postscript ] [ PDF ]
  This document studies existing composability techniques and applies them to analyzing DTOS. The goal is to assess these techniques for specifying and verifying modular systems by composing specifications and proofs for the individual system components and to develop new techniques as necessary. The report includes a framework for composition and an example of the composition of several components.
  The framework and examples in this report were written using PVS . The source files are available as a pvsdump , though a few of the proofs may not be compatible with current versions of PVS.
  A newer version of the framework, which supports refinement in addition to composition, should be available soon through the Composability for Secure Systems program.

Study of Operating System Security Mechanisms

• DTOS General System Security and Assurability Assessment Report [ Postscript ] [ PDF ]
  This document contains the results of the DTOS Essential Requirements Study. It presents criteria for assessing microkernel based systems in their ability to be configured to meet a range of security policies and the feasibility of assuring that a system meets the security requirements of the policies. Five systems are then assessed against these criteria. The goal of this report is to provide guidance for future secure system development by providing the design criteria and examples of designs which meet and do not meet those criteria.