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.
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.
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.
As seL4 is continuously evolving to support new features and platforms (see the roadmap), our proofs also evolve with it.
We also work on strengthening some of the assumptions made in our proofs, especially assumptions involving hardware behaviour.
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.
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 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.
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.
This is a project to verify the error-prone process of initially setting up the components of a system on seL4.
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:
See our software page for a full list.
|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
Verification of programs in virtual memory using separation logic
PhD Thesis, UNSW, Sydney, Australia, July, 2011
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
Formal memory models for verifying C systems code
PhD Thesis, UNSW, Sydney, Australia, August, 2008
A logic for virtual memory
Systems Software Verification, pp. 61–77, Sydney, Australia, July, 2008
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|
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
A formal model of the L4 micro-kernel API using the B method
Technical Report Technical Report 05-00029-1, NICTA, 2005
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