An abstract of “Secure Minicomputer Operating System (KSOS): Executive Summary Phase I: Design”
The long-term goal of the KSOS effort is to develop a commercially viable computer operating system for the DEC PDP-11/70 that
- is compatible with the Bell Telephone Laboratories’ UNIX*tm,
- is capable of efficiency comparable to standard UNIX*tm,
- enforces multilevel security and integrity, and
- is demonstrably secure.
In order to achieve this goal, the Phase I effort described here has designed a trusted Security Kernel and associated trusted Non-Kernel Security-Related Software, such that the trusted software:
- provides a suitable basis for KSOS;
- intrinsically supports multilevel security/integrity,
- can be used by itself to support non-UNIX*tm-based applications, and
- is able to run efficiently on a DEC PDP-11/70.
The security of the overall KSOS system must be convincingly demonstrated. This will be accomplished by formal verification of the security properties of the design (i.e., the formal specifications) and selected proofs of correspondence between the delivered code and the design. In addition, KSOS will be rigorously tested to lend added confidence in the in the system.
Although the Security Kernel is intended initially to support an Emulator providing a UNIX*tm-like user environment, the Kernel has been designed to be used by itself, or with an Emulator providing a different user environment. Typical uses of the Kernel by itself would be dedicated secure systems such as military message processing systems, or secure network front ends.
