Abstract

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.