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
- 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 |