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
Links
Events
| Title | Day | Room | Track | Start | End |
|---|---|---|---|---|---|
| seL4 Microkernel Status Update | Sunday | K.4.601 | Microkernels and Component-based OS | 09:00 | 09:50 |