Speaker:   Prof. Gernot Heiser

                     University of New South Wales

Title:           Towards Principled Temporal Isolation in the Operating System

Date:          Monday, August 10, 2015

Time:          11:00 a.m.                        

Room:        E-Quad, Room B205

Host:          Prof. Ruby Lee

 

Abstract:  Spatial isolation, i.e. controlling memory access, forms the basis of protection in operating systems.  However, this is neither sufficient for ensuring safe operation of real-time systems, nor for ensuring confidentiality.  It must be complemented by temporal isolation, i.e. preventing a process from unduly influencing the execution speed of another process.  Most operating systems provide very poor temporal isolation if any.  Exceptions are systems designed to support a narrow class of applications (either hard real-time systems or separation kernels for security-critical uses), which also tend to have high overheads or force low system utilisation.

 

The formally-verified seL4 microkernel is a general-purpose high-assurance platform that is intended to support a wide range of uses, including highly performance-sensitive mobile systems, (safety) multi-criticality systems and (security-critical) cross-domain solutions.  We are therefore after mechanisms that provide strong temporal isolation where needed, but avoid overheads where not.  The talk will discuss present work in progress on simple kernel mechanisms that will allow us to achieve those goals.

 

 

Biography:  Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at UNSW, and leads the Software Systems Research Group at NICTA, Australia’s National Centre of Excellence for ICT Research.  He joined NICTA at its creation in 2002, and before that was a full-time member of academic staff at UNSW from 1991.  His past work included the Mungi single-address-space operating system (OS), several un-broken records in IPC performance, and the best-ever reported performance for user-level device drivers. More recently he led the team at NICTA which produced the world’s first formal proof of functional correctness of a protected general-purpose operating-system kernel, the first published sound worst-case execution time analysis of a protected OS kernel, and the synthesis of high-performance device drivers.

 

In 2006, Gernot with a number of his students founded Open Kernel Labs, to market secure virtualization technology for embedded systems. The company’s OKL4 operating system, a descendent of L4 kernels developed by his group at UNSW and NICTA, is deployed in billions of mobile devices, and now ships on the security processor of all iOS devices. Open Kernel Labs was sold to General Dynamics in August 2012.