Gernot Heiser is Scientia (distinguished) Professor and John Lions Chair of Operating Systems at UNSW Sydney. His research interests 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 systems that are provably secure. As leader of the Trustworthy Systems group, he pioneered large-scale formal verification of systems code, specifically the design, implementation and formal verification of the seL4 microkernel; seL4 is now being used in real-world security- and safety-critical systems. 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 is deployed on the secure enclave of all iOS devices. He presently serves as Chief Scientific Officer of Neutrality, and Chairman of the seL4 Foundation. Gernot is a Fellow of the ACM, the IEEE, the Australian Academy of Technology and Engineering (ATSE), the Royal Society of NSW (RSN) and an ACM Distinguished Lecturer.
gernot@unsw.edu.au
https://gernot-heiser.org/
https://microkerneldude.org
https://www.linkedin.com/in/gernotheiser/
DVP term expires December 2025
Presentations
From niche to prime time: How seL4 changed a research community
Operating system (OS) microkernels had been around since the 1970s, and were popular in the ’80, just to become highly unfashionable in the ’90s resulting from poor performance and deployment debacles. The early L4 microkernels of the mid-’90s demonstrated that good performance was possible with good design, but they remained a niche research topic (although commercially deployed in critical systems, especially avionics). Similarly, formal verification, i.e. correctness proofs, of program code looked promising in the early ’90s, but failed to deliver on more than toy problems. As a result, it made little impact, especially in the systems space, with virtually no verification results published in the top venues. This all changed when we provided a machine-checked proof of the correct implementation of the seL4 microkernel, the first ever OS kernel with such a proof. seL4 was specifically designed not to be a toy, but for real-world deployment, which required competitive performance. And it had to be written from scratch, to make verification feasible. The effect of the work was a dramatic change in attitude to formal methods first in the research community, and with some delay government and industry. The top systems conferences now regularly have multiple verification sessions, government organisations, such as DARPA, as well as corporations such as Apple, Amazon and Facebook, are massively re-investing in formal verification. And SIGOPS recognised the work and its impact with a Hall of Fame Award in 2019. In this talk I will discuss the story of seL4 in more detail, its real-world impact, and some of the follow-on research it triggered. I will also highlight some of the current research opportunities resulting from seL4.
Making Trusted Systems Trustworthy
We trust computer systems all the time: with our money, our sensitive private data, our critical infrastructure and, in the age of autonomous vehicles, increasingly with our lives. Yet contemporary computer systems really do not deserve such trust. We all got used to our PCs crashing, and all too frequently they get hacked by an attacker. While lack of computer reliability is often just a nuisance, increasingly it is well-resourced organised crime attacking individuals or organisations for financial gain. For critical infrastructure there is also the threat from state actors that might attack for political blackmail or to cause economic damage. Clearly we need to do better. And, while we are still years away from making complex, general-purpose computers, such as PCs and servers, trustworthy in any real sense, we now have the core ingredients for true trustworthiness, and are able to apply them in the more restricted scenarios of embedded and cyberphysical systems. Specifically, the seL4 microkernel is the first operating system (OS) kernel with a machine-checked proof of implementation correctness – bug-free in a very strong sense. The proof states that the kernel will always behave according to its formal specification, and applies to the actual binary code that runs on hardware. Additional proofs about the specification show that the kernel can enforce the classic security properties of confidentiality, integrity and availability. As such, seL4 is a bullet-proof base for building truly trustworthy systems, and it is already being deployed in national security, autonomous cars and critical infrastructure. However, seL4, being a microkernel, only provides the basic mechanisms for trustworthy systems; it is not a complete system, and further research and development is needed to make complete trustworthy systems a reality. These include trustworthy high-level services and abstractions, such as file systems and networking services, trustworthy application code that leverages the guarantees provided by the kernel, and system architectures that lend themselves to formal reasoning about security and safety. This will require further progress across operating systems, programming language design and implementation, formal methods as well as hardware verification. There is also on-going research on seL4 itself, especially on a principled prevention of information leakage through timing channels.
How to Write a Great Paper
Publication in prestigious venues is key to academic impact, and in computer science this mostly means the top-tier conferences. These venues receive large numbers of submissions, resulting in a very competitive paper selection process. In order to succeed, a prospective author must understand what is expected from a manuscript, what makes research significant enough to be considered for publication, and how presentation can help or hinder acceptance. Over more than a quarter century I have certainly experienced my fair share of rejections of what I thought were good papers, and, in hindsight, most of these rejections were justified (although it is obvious that there is a degree of good or bad luck involved as well). And from many years of serving on all of the top-tier program committees in my field, I have a good idea of what reviewers look for. In this talk, which is aimed at PhD students and early career researchers, I will discuss what makes a good research problem, how to perform a convincing evaluation that shows that you have made a significant contribution, and, importantly, how to present the work in a convincing paper that has a chance of getting accepted in a top-tier venue. While based on my experience in the core systems discipline (conferences like SOSP, OSDI, ASPLOS, EuroSys, Usenix ATC), it applies to “systems” research in general, including in programming languages, databases and security. My experience is less relevant for more theoretical research.
