Program

Abstract
A wide range of research areas – from natural language processing to computer vision and software engineering – have been (or are being) revolutionized by machine learning and artificial intelligence. Each of these areas went through an inflection point where they transitioned from ML as one of many approaches to ML becoming a predominant approach of the field. No example symbolizes this better than the AlexNet paper from 2012, which fundamentally transformed the field of computer vision.

Computer systems remain a notable exception. In this talk, I will discuss emerging trends in the ML for Systems domain, how systems differ from these other areas, and what an "AlexNet Moment" for systems might look like. Along the way, I will describe a framework for categorizing work in the field and discuss emerging research problems and opportunities.

Bio
Martin Maas is a research scientist at Google DeepMind, where he is working on new approaches to leverage artificial intelligence for solving computer systems problems. His research has been deployed in a range of Google systems and products, including Google Compute Engine, TCMalloc, Pixel phones and the TPU compiler. His work has received multiple recognitions, including an ASPLOS Best Paper Award, an IEEE Micro Top Pick, a SIGPLAN Research Highlight, and a CACM Research Highlight. He has been active in several leadership roles in the community, including as General Chair of ISMM 2025, WACI Chair and Vice Program Chair at ASPLOS 2025, Program Chair of ISMM 2020, and as one of the co-organizers of the ML for Systems workshop at NeurIPS. He also co-leads Google’s involvement in the free and open RISC-V instruction set architecture. Martin holds a Ph.D. from the University of California at Berkeley and a B.A. from the University of Cambridge, both in Computer Science.

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.