With the spread of cyberphysical systems and the IoT, trustworthiness of these devices, i.e. security, safety and dependability, is becoming increasingly important. The course will investigate present operating system (OS) technology and why it fails to support trustworthiness. We will then discuss the requirements for operating systems for true trustworthiness.
We will then discuss security models for operating systems and OS mechanisms and structures to implement those. We will discuss security-oriented microkernels, and specifically the formally-verified seL4 microkernel as concrete representations.
The last part will examine the meaning of formal verification in general, and that of seL4 specifically, including a discussion of what it does and does not guarantee. We will finish with a discussion of on-going work on making systems trustworthy.
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 Data61s 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).