We cordially invite you to the upcoming CASA Distinguished Lecrute on Tuesday, May 13, 2025., 13. Mai 2025, ein.
When: 13.05.2025, 11:00 o´clock
Where: MB1 Seminar Room
Online-Participation: Zoom-Webinar (Meeting-ID: 680 8850 3529; Password: 364724)
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 a complete OS kernel. Over the following 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 no guarantee that a system built on top is secure in any real sense.
We had to realise that seL4 is too hard to use for people without a deep understanding of the kernel model and its philosophy, and that seL4 must be developed into a complete OS that provides the high-level services expected by developers, such as processes and I/O. We have therefore started to develop LionsOS, a highly modular design of an seL4-based OS for use in embedded/cyberphysical systems. We aim to achieve end-to-end proofs of security enforcement for LionsOS, including the provable confinement of untrusted code with a threat model that includes microarchitectural timing channels.
Our experience to date shows that a clean, lean and principled design not only makes it possible to develop an OS from scratch with the limited resources of a university group, but that such an OS can actually be highly performant – de-bunking some old (but apparently never-dying) myths about the performance of microkernel-based systems.
The talk will also touch on 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 serves as the founding Chairman of the seL4 Foundation. He 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.
General note: In case of using gender-assigning attributes we include all those who consider themselves in this gender regardless of their own biological sex.