Session chair: Haibo Chen

Title
Will we ever have truly secure operating systems?
Slides

Abstract
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 anOS 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 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 will explore some of the reasons behind this disappointing state of affairs, and what can be done about it. Specifically I will discuss our current work on LionsOS, a new seL4-based OS targeting the embedded/cyberphysical domain, and designed to be verifiable. I will also discuss more speculative, early-stage work towards a provably secure, general-purpose OS.

Bio
Gernot Heiser is Scientia (distinguished) Professor and John Lions Chair of Operating Systems at UNSW Sydney, where he leads the Trustworthy Systems research group. His research interest are in operating systems, real-time systems, security and safety. His research vision is to completely change the cybersecurity game, from playing catch-up with attackers, to making computer systems provably secure and safe. With his team he pioneered the large-scale formal verification of systems code, specifically the design, implementation and formal verification of the seL4 microkernel; this work was recognised with an ACM SIGOPS Hall of Fame Award and the ACM Software System Award.

Heiser's former company Open Kernel Labs, acquired by General Dynamics in 2012, marketed the OKL4 microkernel, which shipped on billions of mobile wireless chips and has been deployed on the secure enclave of iOS devices. He presently serves as Chief Scientist of Neutrality, and Chairman of the seL4 Foundation. Gernot is a Fellow of the ACM, the IEEE, Engineers Australia, the Australian Academy of Technology and Engineering (ATSE) and the Royal Society of New South Wales (RSN) and a Member of the German Academy of Sciences Leopoldina. He is also an ACM Distinguished Lecturer and an IEEE Distinguished Visitor.