An abstract of “A Provably Secure Operating System”
This report summarizes work to date toward the development of a provably secure operating system. Discussed here are
- a methodology for the design, implementation, and proof of properties of large computing systems,
- the design of a secure operating system using this methodology,
- the security properties to be proven about this system,
- considerations for implementing such a system, and
- an approach to monitoring security and performance.