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.

(About this image)

What we have proved
Upcoming features
From a verified kernel to trustworthy systems
Tools and engineering
Our past projects
Publications

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

Multiprocessor-kernel verification — verification of an early version of the multiprocessor seL4 kernel
Proof measurement and estimation — metrics and estimation methods, to help planning and management of large-scale verification projects
Verification-enhanced compiler optimisation — optimising code based on formally proved properties
Whole-system assurance — an experiment in verifying user-level system properties over a low-level ARM model

Publications

		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
		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
		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
		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
		Rafal Kolanski Verification of programs in virtual memory using separation logic PhD Thesis, UNSW, Sydney, Australia, July, 2011
		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.
		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
		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
		Gerwin Klein, Philip Derrin and Kevin Elphinstone Experience report: seL4 — formally verifying a high-performance microkernel Proceedings of the 14th International Conference on Functional Programming, pp. 91–96, Edinburgh, UK, August, 2009
		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
		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
		Rafal Kolanski and Gerwin Klein Mapped separation logic Verified Software: Theories, Tools and Experiments, pp. 15–29, Toronto, Canada, October, 2008
		Harvey Tuch Formal memory models for verifying C systems code PhD Thesis, UNSW, Sydney, Australia, August, 2008
		Rafal Kolanski A logic for virtual memory Systems Software Verification, pp. 61–77, Sydney, Australia, July, 2008
		Gernot Heiser Trusted ⇐ trustworthy ⇐ proof – Position paper Proceedings of the 2nd Conference on Future of Trust in Computing, pp. 55–59, Berlin, DE, May, 2008
		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
		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
		Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser Verifying a high-performance micro-kernel 7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007
		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
		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
		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
		Gerwin Klein and Rafal Kolanski Formalising the L4 microkernel API Computing: The Australasian Theory Symposium (CATS), pp. 53–68, Hobart, Australia, January, 2006
		Harvey Tuch and Gerwin Klein A unified memory model for pointers Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 474–488, Montego Bay, Jamaica, December, 2005
		Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco L4cars 3rd Embedded Security in Cars Conference (escar), Cologne, DE, November, 2005
		Harvey Tuch, Gerwin Klein and Gernot Heiser OS verification — now! Proceedings of the 10th Workshop on Hot Topics in Operating Systems (HotOS), pp. 7–12, Santa Fe, NM, USA, June, 2005
		Rafal Kolanski A formal model of the L4 micro-kernel API using the B method Technical Report Technical Report 05-00029-1, NICTA, 2005
		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
		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
		Gerwin Klein and Harvey Tuch Towards verified virtual memory in L4 TPHOLs Emerging Trends '04, pp. 16 pages, Park City, Utah, USA, September, 2004