Kevin Elphinstone: Towards Trustworthy Systems - Formal Verification of the seL4 Operating System Kernel

Computer Science Colloquium

Speaker: Kevin Elphinstone, University of New South Wales & National ICT Australia

Abstract:

We increasingly put our trust in computing systems for many aspects of our lives, including medical, industrial control, and avionic systems. At the same time, computing systems are growing increasing complex and less trustworthy. One part of tackling this problem is to provide a trustworthy operating system (OS) to form the foundation upon which to construct trustworthy complex systems. The seL4 microkernel is formally verified to be correct in the Isabelle/HOL interactive theorem proving environment. The microkernel implementation will always strictly follow a high-level abstract specification of its behaviour. Practically, this implies many desirable properties, including never crashing, always terminating, and never performing unsafe operations. This talk will examine what we formally verified, under what assumptions, and our approach to achieving the proof. The research was a collaboration between OS and formal methods researchers. This talk is an OS researchers view of the project. I will also touch on current work and future directions of the Trustworthy Embedded Systems project at NICTA.

Biography:

Dr. Kevin Elphinstone is a Senior Researcher with National ICT Australia Ltd (NICTA), and a Senior Lecturer within the School of Computer Science and Engineering at the University of New South Wales, Sydney, Australia. Dr. Elphinstone's research and teaching interests lie in operating systems, with specific interests in security, microkernels, real-time systems, and trustworthy embedded systems. Dr. Elphinstone has a B.Sc. in Computer Science, a B.E. in Electrical Engineering, and was awarded a Ph.D. in Computer Science in 1999, all from the School of Computer Science and Engineering at UNSW. He has managed to escape from UNSW several times. He has been a Visiting Scientist at the IBM T.J. Watson Research Centre, NY, and a Research Associate at the University of Karlsruhe, Germany. He was an architect of microkernel-based operating systems in both positions.