Brussels / 1 & 2 February 2020


Gernot Heiser

Photo of Gernot Heiser

I'm a distinguished professor (Scientia Professor) at UNSW Sydney where for 25 years I have been researching microkernels as the basis for secure and safe systems, with a track record of open-sourcing kernels and related software since 1997. I have also been active in transferring research outcomes into real-world deployments, and my kernels have been deployed in billions of devices. I'm also a researcher at CSIRO's Data61, an Australian government research organisation. I'm a Fellow of the ACM, the IEEE and the Australian Academy of Technology and Engineering (ATSE).

Past achievements include: * first 64-bit L4 microkernel (MIPS R4000), open-sourced in 1997 * open-source L4-embedded microkernel, derived from Karlsruhe's Pistachio kernel, deployed on billions of Qualcomm modem chips * an adapted version of the above is deployed on the secure enclave of all iOS devices * seL4: first ever OS kernel with a formal, machine-checked proof of implementation correctness, verified in 2009, open-sourced in 2014 * ACM SIGOPS Hall of Fame Award for seL4 (2019) * first complete and sound worst-case execution-time analysis of an OS kernel (seL4 in 2011) * first capabilities for time suitable for hard real-time systems (seL4 in 2018) * pioneered the new concept of time protection (temporal equivalent of memory protection) for principled and systematic prevention of timing channels



Title Day Room Track Start End
seL4 Microkernel Status Update Sunday K.4.601 Microkernels and Component-based OS 09:00 09:50