Please join us for the next CSE seminar in the large conference room (2 MetroTech Center, 10th floor, room 10.099):
Speaker: Gernot Heiser, Scientia Professor and John Lions Chair of Operating Systems at UNSW Australia, Chief Research Scientist at Data61, CSIRO
I will give an introduction to the seL4 microkernel, and its formal verification. I’ll discuss what the verification means, what guarantees it does and does not provide. I will also explain what seL4 is as an operating-system kernel, its mechanisms and features, what user-level support exists, and what you need to know when considering building systems on top.
Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at UNSW Australia and Chief Research Scientist at Data61, CSIRO. He has a 20-year track record of building high-performance operating-system microkernels as a minimal basis for trustworthy systems. 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 verification of the seL4 microkernel. His 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 processor of all iOS devices. Heiser is a Fellow of the ACM, the IEEE and the Australian Academy of Technology and Engineering (ATSE).