Towards Verified Real-World Systems

Abstract:

This talk presents an overview of the Trustworthy Systems project at NICTA, which aims to construct real-world systems with proven safety or security properties. Starting with the seL4 microkernel, for which we have established a complete proof chain from general safety and security properties (confidentiality and integrity) to binary code, we are developing a framework for building complete systems and proving their security. One case study is an autonomous aerial vehicle, which is developed under the DARPA HACMS program by a consortium conisting of NICTA, Rockwell Collins, Galois and Boeing.

Biography:

Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at the University of New South Wales (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 more than 2 billion mobile devices. This includes the Motorola Evoke, the first (and to date only) mobile phone running a high-level OS (Linux) and a modem stack on the same processor core. Open Kernel Labs was sold to General Dynamics in August 2012.

In a former life, Gernot developed semiconductor device simulators and models of device physics for such simulators, and pioneered the use of three-dimensional device simulation for the characterisation an optimisation of high-performance silicon solar cells.