Professor Dr Gernot Heiser

Research Priorities: Computer science, operating systems, computer software, microkernels, covert channels, cyber security
Gernot Heiser is a German-Australian computer scientist. His research focus is on operating systems, especially microkernel-based systems and their application in embedded/cyber-physical systems. He is a pioneer of the use of mathematical proof techniques for ensuring the security and dependability of software systems. His innovations are used to ensure the security of medical devices, airplanes, critical infrastructure, and national security systems.
Gernot Heiser works on operating system security and more generally fundamental solutions to cyber-security threats. His focus is on improving the security and reliability of operating systems through the use of microkernel technology and formal verification. His team developed the seL4 microkernel, the first general-purpose operating system kernel with a proof of implementation correctness, considered a milestone in the application of formal methods to real-world software. Besides continuing to improve seL4, focuses on the development of practical high-assurance systems based on seL4.
A related area of interest are microarchitectural timing channels and their prevention. He demonstrated the first practical, cross-core attack on encryption keys through a shared cache. He subsequently developed a set of mechanisms, collectively called “time protection”, for the systematic prevention of information leakage through timing channels. Further research areas are energy/power management, virtualisation, and architectural support for operating systems.
His research outcomes are widely deployed. His earlier L4 microkernel shipped on billions of mobile communication chips and on the security processor of all iOS devices. seL4 was shown to be effective in protecting autonomous vehicles from cyber attacks, and is being designed into practical defence systems, critical infrastructure, autonomous cars and IoT devices.