Trustworthy Systems

The seL4 verification project

Mobile phones that can be hacked by SMS.

Cars that have more software problems than mechanical ones.

Medical implants that allow hackers to kill their hosts.

Computer viruses spreading through critical control systems and defense systems.

But it does not have to be that way.

A proved-correct operating system kernel

In the seL4 verification project, we prove that our seL4 OS kernel implements its specifications correctly.

Building on state-of-the-art formal methods, our proofs provide mathematically sound, computer-checked evidence that seL4's code works correctly as described.

This makes seL4 the foundation of choice for building software systems with unprecedented security, safety, reliability and efficiency.

What we have proved

Functional correctness (L4.verified)
The source code of seL4 implements its specification, which is a precise description of seL4's system call interface. This was the original L4.verified milestone and was completed in 2009.
Integrity and information flow security
seL4 correctly enforces the basic security properties of data integrity and information flow security for program threads. This is the world's first source-level proof of information flow security for a general-purpose OS kernel.
Compilation correctness
On ARMv7 and RISC-V (64-bit), the C source code of seL4 is correctly compiled to executable code. This means that the proofs about seL4 also apply to the code that actually runs on the hardware.
Verified worst-case execution time
We have verified upper bounds on the execution time of seL4 operations. This applies directly to the seL4 machine code running on an ARM11 processor, and is the first ever published complete timing analysis of a protected multitasking kernel.

A detailed overview of these proof projects can be found in our journal article: Comprehensive formal verification of an OS microkernel.

We also have information on verification status for different hardware platforms.

Upcoming features

As seL4 is continuously evolving to support new features and platforms (see the roadmap), our proofs also evolve with it.

Hardware platforms
Our proofs initially targeted only the ARM architecture. We have now proved functional correctness, security properties and compilation correctness for the 64-bit RISC-V architecture, and the functional correctness of seL4 for ARM hypervisor extensions and the x86-64 architecture.
Real-time and mixed-criticality scheduling
seL4 now provides novel mechanisms for implementing real-time mixed-criticality systems. We are specifying and verifying the correctness of the new kernel scheduler and system call interfaces.
Concurrency
We are verifying a multi-core port of seL4. This will involve not only writing the proof itself, but also developing a concurrency proof framework that can be applied at the size and complexity of seL4's code base.
Time protection
We have evaluated mechanisms for seL4 to enforce the prevention of timing channels between security domains. Work is currently underway on formalising the correctness of these mechanisms, so as to make them amenable to verification.

We also work on strengthening some of the assumptions made in our proofs, especially assumptions involving hardware behaviour.

TLB formal model
Operating systems such as seL4 must manage a complicated translation lookaside buffer (TLB), provided by modern processors. We are investigating how to extend specifications and proofs to take this translation system into account, a hitherto-unsolved problem.

From a verified kernel to trustworthy systems

The long-term goal of our formal methods research is to formally verify programs and entire systems running on seL4, as in our trustworthy components projects. We are extending the seL4 proofs to support these projects, which are listed below.

Cogent

Our Cogent language aims to simplify the verification of the device drivers and services that are needed in a modern operating system. Cogent has a formally verified toolchain, covering the entire compilation process from type-checking to low-level code output.

CakeML

CakeML is a verified compiler for a high-level functional language, suitable for application-level software.

CakeML is a collaborative project by researchers at multiple institutions. Here at Trustworthy Systems, our work focuses on applying CakeML to systems programming, and verifying the behaviour of CakeML programs in the context of larger systems.

Trustworthy component framework

It is not enough to prove the correctness of individual components in a software system; the overall system configuration and connections also need to be correct. We are implementing automatic verification tools for our CAmkES component framework.

System initialisation

This is a project to verify the error-prone process of initially setting up the components of a system on seL4.

Tools and engineering

Proof engineering

Our seL4 proofs contain nearly 1 million lines of proof steps, and continue to be expanded. To manage this complexity, we are developing a new systematic discipline of proof engineering.

As software engineering is for software, proof engineering systematically treats large-scale formal proofs, including their development, maintenance, deployment, and project management aspects.

Our work has also led to a number of additional verification tools and frameworks, mainly for the Isabelle proof assistant:

Eisbach
Eisbach is a proof method language that enables Isabelle end users to write automated proof procedures.
C parser
Our C parser translates (a subset of) C code into a formal representation in Isabelle/HOL. The C parser is used to describe the behaviour of seL4's code in our proofs.
AutoCorres
Our AutoCorres tool automatically abstracts and simplifies programs that have been translated by the C parser.

See our software page for a full list.

Our past projects

Publications

Abstract PDF Gernot Heiser, Gerwin Klein and Toby Murray
Can we prove time protection?
Workshop on Hot Topics in Operating Systems (HotOS), pp. 23-29, Bertinoro, Italy, May, 2019
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013
Abstract PDF Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325–340, Nijmegen, The Netherlands, August, 2011
Abstract PDF Rafal Kolanski
Verification of programs in virtual memory using separation logic
PhD Thesis, UNSW, Sydney, Australia, July, 2011
Abstract PDF Gerwin Klein
From a verified kernel towards verified systems
Asian Symposium on Programming Languages and Systems (APLAS), pp. 21–33, Shanghai, China, November, 2010
Invited extended abstract.
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an operating-system kernel
Communications of the ACM, Volume 53, Number 6, pp. 107–115, June, 2010
Research Highlights paper
Abstract
Slides
PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009
Best Paper Award
Hall of Fame Award
Abstract PDF
Presentation Video
Gerwin Klein, Philip Derrin and Kevin Elphinstone
Experience report: seL4 — formally verifying a high-performance microkernel
International Conference on Functional Programming, pp. 91–96, Edinburgh, UK, August, 2009
Abstract PDF Rafal Kolanski and Gerwin Klein
Types, maps and separation logic
International Conference on Theorem Proving in Higher Order Logics, pp. 276–292, Munich, Germany, August, 2009
Abstract PDF Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish
Mind the gap: A verification framework for low-level C
International Conference on Theorem Proving in Higher Order Logics, pp. 500–515, Munich, Germany, August, 2009
Abstract PDF Rafal Kolanski and Gerwin Klein
Mapped separation logic
Verified Software: Theories, Tools and Experiments, pp. 15–29, Toronto, Canada, October, 2008
Abstract PDF Harvey Tuch
Formal memory models for verifying C systems code
PhD Thesis, UNSW, Sydney, Australia, August, 2008
Abstract PDF Rafal Kolanski
A logic for virtual memory
Systems Software Verification, pp. 61–77, Sydney, Australia, July, 2008
Abstract PDF Gernot Heiser
Trusted ⇐ trustworthy ⇐ proof – Position paper
Conference on Future of Trust in Computing, pp. 55–59, Berlin, DE, May, 2008
Abstract PDF Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007
Abstract PDF Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser
Towards a practical, verified kernel
Workshop on Hot Topics in Operating Systems (HotOS), pp. 6, San Diego, CA, USA, May, 2007
Abstract PDF Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser
Verifying a high-performance micro-kernel
Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007
Abstract PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97–108, Nice, France, January, 2007
Abstract PDF Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M. T. Chakravarty
Running the manual: An approach to high-assurance microkernel development
Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA, September, 2006
Abstract PDF Kevin Elphinstone, Gerwin Klein and Rafal Kolanski
Formalising a high-performance microkernel
Verified Software: Theories, Tools and Experiments, pp. 1-7, Seattle, USA, August, 2006
Abstract PDF Gerwin Klein and Rafal Kolanski
Formalising the L4 microkernel API
Computing: The Australasian Theory Symposium (CATS), pp. 53–68, Hobart, Australia, January, 2006
Abstract PDF Harvey Tuch and Gerwin Klein
A unified memory model for pointers
International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 474–488, Montego Bay, Jamaica, December, 2005
Abstract PDF Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco
L4cars
Embedded Security in Cars Conference (escar), Cologne, DE, November, 2005
Abstract PDF Harvey Tuch, Gerwin Klein and Gernot Heiser
OS verification — now!
Workshop on Hot Topics in Operating Systems (HotOS), pp. 7–12, Santa Fe, NM, USA, June, 2005
Abstract PDF Rafal Kolanski
A formal model of the L4 micro-kernel API using the B method
Technical Report Technical Report 05-00029-1, NICTA, 2005
Abstract PDF Kevin Elphinstone
Future directions in the evolution of the L4 microkernel
Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004
Abstract PDF Harvey Tuch and Gerwin Klein
Verifying the L4 virtual memory subsystem
Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, pp. 73–97, Sydney, Australia, October, 2004
Abstract PDF Gerwin Klein and Harvey Tuch
Towards verified virtual memory in L4
TPHOLs Emerging Trends '04, pp. 16 pages, Park City, Utah, USA, September, 2004