Bio
Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at UNSW (University of New South Wales) Sydney and Chief Research Scientist at CSIRO’s Data61. His research interest are in operating systems, real-time systems, security and safety.
He is the founder and past leader of Data61’s Trustworthy Systems group, which pioneered large-scale formal verification of systems code, specifically the design, implementation and formal verification of the seL4 microkernel; seL4 is now being designed into 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 more recently ships on the secure enclave of all iOS devices.
He presently serves as Chief Scientist, Software, of HENSOLDT Cyber, a Munich-based company providing a secure hardware-software stack for embedded and cyber-physical systems.
Gernot is a Fellow of the ACM, the IEEE and the Australian Academy of Technology and Engineering (ATSE) and an ACM Distinguished Lecturer.
The formally verified seL4 microkernel – present and future
Gernot Heiser
Scientia Professor and John Lions Chair of Operating Systems at UNSW Sydney
Chief Research Scientist at CSIRO’s Data61 – Australia
Keynote – Wednesday 19 February 2020 – 4:15 pm
Abstract
seL4 is the world’s first operating system (OS) kernel with a formal, machine-checked proof of implementation correctness, originally on Arm v6 processors. Since that initial work ten years ago, we have added proofs of security enforcement and timeliness properties and extended verification to x86 and RISC-V architectures. To this date, seL4 is not only the most comprehensively verified OS, but has a strong performance focus and evolves (with proofs) to address a widening class of real-world use cases.
This talk will provide a brief overview of the present state of seL4 and its verification story, including multicore support. I’ll focus on recent enhancements, in particular advanced mechanisms for supporting mixed-criticality real-time systems. I will also cover on-going work on time protection, a fundamental approach for preventing information leakage through timing channels.
SLIDES
VIDEO
Featured image: Gernot Heiser at the 2nd Multicore World (Auckland, 2014)
Copyright – Open Parallel Ltd
multicore.world 