Basser Seminar Series

Towards Trustworthy Systems

Speaker: Scientia Professor Gernot Heiser
The University of New South Wales / NICTA

Time: Friday 9 September 2011, 4:00-5:00pm
Refreshments will be available from 3:30pm
Location: The University of Sydney, School of IT Building, Lecture Theatre (Room 123), Level 1

Add seminar to my diary


Computer systems are routinely deployed in life- and mission- critical situations, yet in most cases their security, safety or dependability cannot be assured to the degree warranted by the application. In other words, trusted computer systems are rarely trustworthy.

We believe that this is highly unsatisfactory, and have embarked on a research program aimed at bringing reality in line with expectations. This talk describes NICTA’s research agenda for achieving true trustworthiness in systems. The approach is based on establishing the trustworthiness of the lowest level of software, a small microkernel or hypervisor, and then using this platform to provide guarantees to complete systems built on top. A number of important steps in this direction have been achieved, specifically the formal proof of functional correctness of a complete OS microkernel, and subsequently the establishment of further properties, including timeliness and integrity enforcement. Work is progressing on making dependability guarantees for complete real-world systems, comprising millions of lines of code.

Speaker's biography

Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at the University of New South Wales (UNSW), and co-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.

In 2006, Gernot with a number of his students founded Open Kernel Labs, now the market leader in secure operating-systems and virtualization technology for mobile wireless devices. The company's OKL4 operating system, a descendent of L4 kernels developed by his group at UNSW and NICTA, is deployed in more than 1.2 billion mobile phones. 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.

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 and optimisation of high-performance silicon solar cells.