The goal of the Department of Defense Kernelized Secure Operation System (KSOS) project is to design, implement and prove a secure operating system. Specifically, it is desired that KSOS be designed and proven to enforce a security model, derived from the security practices of the Department of Defense, referred to as "multilevel security."
The proof required for KSOS is rigorous proof in the mathematical sense. The necessity of preparing for proof of a program so large and complex as an operating system has led to the adaptation and , where necessary, development of design and implementation methodologies for KSOS which are departures from the usual methods of system programming. Specifically, KSOS has required formal specification of operating system design, automatic theorem generation, automatic theorem proof, selection and use of a verifiable programming language, and verification of operating system programs. KSOS represents the first industrial application of many of these techniques, and is breaking new ground in the construction and proof of large scale computer systems. This paper describes what methods were chosen for KSOS and how they were applied.
This paper is not (yet) available online.