Will We Ever have Truly Secure Operating Systems?

Half a century after PSOS, the first attempts to prove an operating system (OS) secure, OS faults remain a major threat to computer systems security. A major step forward was the verification of the seL4 microkernel, the first proof of implementation correctness of an OS kernel. Over the next 4 years this proof was extended to the binary code, proofs of security enforcement, and sound and complete worst-case execution-time analysis. The proofs now cover 4 ISAs.Yet, 15 years later, there is still no provably secure OS. While seL4 has been successfully deployed in defence and civilian security- and safety-critical systems, it is a microkernel that mostly guarantees process isolation without providing the application-oriented services expected from an OS. This not only makes seL4 difficult to deploy, but also means that there is limited assurance that a system built on top is secure in any real sense.Why has seL4 not been leveraged into a secure OS? In this talk I explore some of the reasons behind this disappointing state of affairs, and what can be done about it. Specifically, I discuss our current work on LionsOS, a new seL4-based OS targeting the embedded/cyberphysical domain, which is easy to use and designed to be verifiable. We aim to achieve our goals by a principled design driven by simplicity, modularity, strict separation of concerns, and highly use-case specific policies, rather than the standard approach of trying to generalise policies.I also discuss more speculative, early-stage work towards a provably secure, general-purpose OS