Gernot Heiser was born in 1957. He is a computer scientist from Germany and Australia. He holds the title of Scientia Professor and serves as the John Lions Chair for operating systems at UNSW Sydney. At this university, he leads the Trustworthy Systems group (TS).

Life

Heiser earned his high school diploma in 1976 at the Markgräfler Gymnasium Müllheim in Müllheim im Markgräflerland.

In 1991, Heiser joined the School of Computer Science and Engineering at UNSW Sydney, originally as a lecturer. He reached the rank of full professor in 2002, a position he continues to hold.

Also in 2002, he joined the newly created research organization NICTA as one of its initial Program Leaders, responsible for the Embedded, Real-Time and Operating Systems (ERTOS) program. After a reorganization in 2011, ERTOS became the Software Systems Research Group (SSRG), which he led. When NICTA was absorbed into CSIRO in 2016, Heiser stepped back from managing the group, which was then called Trustworthy Systems (TS). In 2021, CSIRO closed TS, and at that time, Heiser took the group back to UNSW and resumed its leadership.

Since April 2020, Heiser has served as the Founding Chairman of the seL4 Foundation.

Research

Heiser's research is about microkernels, systems based on microkernels, and virtual machines. He focuses on making these systems perform well and be reliable.

His group created Mungi, an operating system that runs on groups of 64-bit computers. They also developed versions of the L4 microkernel with very fast communication between different parts of the system. His Gelato@UNSW team helped start the Gelato Federation. They studied how to make Linux work better and scale more on Itanium computers. They also found the limits of how quickly messages can be sent between parts of a system on Itanium hardware.

When Heiser joined NICTA in 2002, his research shifted to focus on embedded systems instead of high-end computers. He aimed to improve security, safety, and reliability by using microkernel technology. This work led to the creation of a new microkernel called seL4. He proved that seL4 works correctly, which was the first complete proof of a general-purpose operating system kernel.

His work on virtualization was to create full operating system environments on his microkernels. The Wombat project used methods similar to the L4Linux project but ran on x86, ARM, and MIPS hardware. The Wombat project later became the basis for the OKL4 hypervisor from his company, Open Kernel Labs. He also developed a method to reduce the effort needed for paravirtualization, called automated paravirtualization. His work on vNUMA showed how a hypervisor could make a distributed system look like a shared-memory multiprocessor, useful for chips with many processor cores.

Device drivers are another area of his work. He demonstrated user-mode drivers with less than 10% performance loss. This method reduces driver errors. He also created drivers from test equipment and showed that drivers can be automatically made from formal specifications. He studied how operating systems manage energy use.

After leaving Open Kernel Labs in 2010, he focused on seL4 and systems built on seL4. He analyzed how long seL4 takes to run in the worst case, which was the first such analysis for a protected-mode operating system kernel. He also added support for mixed-criticality systems to seL4, making time a key part of its security features.

He studied microarchitectural timing channels and showed the first practical cross-core timing attack in 2015. This led to methods to stop timing-channel leaks, called time protection.

Earlier, he worked on simulating semiconductor devices and used multi-dimensional modeling to improve silicon-based solar cells.

Awards and honours

• Member of the German National Academy of Sciences Leopoldina (2023)
• Fellow of The Royal Society of New South Wales (RSN) (2022)
• Distinguished Speaker of the Association for Computing Machinery (ACM) (2021)
• ACM SIGOPS Hall of Fame Award (2019) for the paper "seL4: Formal Verification of an OS Kernel" (He was the third author on the paper with co-authors)
• Fellow of the Australian Academy of Technology and Engineering (ATSE) (2016)
• Fellow of the Institute of Electrical and Electronics Engineers (IEEE) (2016) "For contributions to security and safety of operating systems"
• Australian Computer Society (ACS) ICT Researcher of the Year (2015)
• Fellow of the Association for Computing Machinery (ACM) (2014) "For contributions demonstrating that provably correct operating systems are feasible and suitable for real-world use"
• Scientia Professor at the University of New South Wales
• 2010 Innovation Hero at The Warren Centre for Advanced Engineering, University of Sydney
• NSW Scientist of the Year 2009 in the category of Engineering, Mathematics, and Computer Sciences
• Best Paper at the 22nd ACM SIGOPS Symposium on Operating Systems Principles (2009)
• Best Paper at the 13th IEEE Asia-Pacific Computer Systems Architecture Conference (2008)
• Best Student Paper at the 2005 USENIX Annual Technical Conference