A Provably Secure Operating System.
Peter G. Neumann, Luke Robinson, Karl Levitt, R. S. Boyer, Amit Saxena · Defense Technical Information Center (DTIC) · 1975
This report summarizes work to date toward the development of a provable secure operating system. Discussed here are: (1) a methodology for the design, implementation, and proof of properties of large computing systems, (2) design of a secure operating system using this methodology, (3) the security properties to be proven about this system, (4) considerations for implementing such a system, and (5) an approach to monitoring security and performance.