Trustworthy Systems

The seL4 microkernel

seL4 key logo

seL4, the secure embedded L4 microkernel, is a key element of our research program. We developed seL4 to provide a reliable, secure, fast and verified foundation for building trustworthy systems.

seL4 enforces security within componentised system architectures by ensuring isolation between trusted and untrusted system components, and by carefully controlling software access to hardware devices in the system.

As a microkernel, seL4 contains only about 12,000 lines of C code plus some assembly code. This minimises the trusted computing base, and has enabled us to verify seL4's functional correctness and security properties using rigorous mathematical proof.

Why seL4?

seL4 is the world’s fastest operating system kernel designed for security and safety, and has been deployed in several real-world projects. It runs on a variety of hardware platforms, including x86, x86-64, Arm and RISC-V. seL4 can also run virtual machines to support legacy software.

seL4-based systems have flown a helicopter and have handled classified military information. An earlier variant, OKL4, has been deployed in over two billion phones.

seL4 is also the foundation for most of our current research in operating systems, and the seL4 verification project hosts much of our research on formal methods for software verification. In turn, our advancements in real-time OS design, covert channel mitigation, hardware fault resiliency and other areas are eventually incorporated back into seL4 itself.

Developing on seL4

seL4 is open source and freely available on GitHub. It is now under the stewardship of the seL4 Foundation. Comprehensive libraries, documentation and tutorials are also available on its website, seL4.systems.

We continue to develop seL4 in close collaboration with our partners in the seL4 Foundation, including releases of verified new features to the user community. See our development roadmap.

We have complemented seL4 with an ecosystem of freely available tools for componentised software architectures, enabling the user community to build large scale software applications on top of the high-assurance environment that it provides.

Technical information

seL4 is a third-generation microkernel that builds on the strengths of the L4 microkernel design. Our documentation site has technical information about the design, implementation and interface of seL4 for software developers, and our publications below provide information for researchers.

We also have historical technical notes that explain seL4's initial design, implementation and verification.

RTOS

The seL4 kernel is targeted at hardware that supports memory protection, which enables strong isolation functionality. More constrained hardware, such as small micro-controllers without memory protection can still benefit from high-assurance real-time operating systems, for instance in the eChronos project.

People

Current

Past

  • Adrian Danis
  • Alexander Kroh
  • Amirreza Zarrabi
  • Anna Lyons
  • Bernard Blackham
  • Branden Robinson
  • Curtis Millar
  • David Cock
  • Dhammika Elkaduwe
  • Ed Pierzchalski
  • Gerwin Klein
  • Harvey Tuch
  • Hesham Almatary
  • Kent Mcleod
  • Kofi Doku Atuah
  • Matthew Fernandez
  • Michael von Tessin
  • Qian Ge
  • Shane Kadish
  • Simon Winwood
  • Thomas Sewell
  • Yanyan Shen

Publications

Abstract Slides Gernot Heiser
LionsOS: A highly dependable operating system for cyberphysical systems
Keynote at International Symposium on Parallel Computing and Distributed Systems, September, 2024
Abstract Slides Gernot Heiser
LionsOS: Towards a truly dependable operating system
Keynote at International Conference on Dependable Systems and Networks (DSN), June, 2024
Abstract PDF Gernot Heiser, Peter Chubb, Alex Brown, Courtney Darville and Lucy Parker
sDDF design: design, implementation and evaluation of the seL4 device driver framework
https://trustworthy.systems/publications/papers/Heiser_CBDP_24.pdf, 2024
Abstract Slides Gernot Heiser
The seL4 microkernel: Provable security for the real world
Keynote at the International Workshop on Advanced Industrial Science and Technology, September, 2023
Abstract Slides
Video
Lucy Parker
The seL4 device driver framework
Talk at the 5th seL4 Summit, September, 2023
Abstract Slides
Video
Ivan Velickovic
The seL4 Microkit
Talk at the 5th seL4 Summit, September, 2023
Abstract PDF Mathieu Paturel, Isitha Subasinghe and Gernot Heiser
First steps in verifying the seL4 Core Platform
Asia-Pacific Workshop on Systems (APSys), Seoul, KR, August, 2023
Abstract Slides Gernot Heiser
Intelligent vehicle security needs a verified operating system
Keynote at the International Workshop on Safety and Security of Intelligent Vehicles, June, 2023
Abstract Slides
Video
Gernot Heiser
seL4 update: Foundation and TS R&D news
Invited talk at the Trusted Computing Center of Excellence 2023 Summit, May, 2023
Abstract PDF Jason Belt, John Hatcliff, John Shackleton, Jim Carciofini, Todd Carpenter, Eric Mercer, Isaac Amundson, Junaid Babar, Darren Cofer, David Hardin, Karl Hoech, Konrad Slind, Ihor Kuz and Kent Mcleod
Model-driven development for the seL4 microkernel using the HAMR framework
Journal of Systems Architecture, Volume 134, pp. 102789, 2023
Abstract Slides
Video
Gernot Heiser
R&D update from Trustworthy Systems
Talk at the 5th seL4 Summit, 2023
Abstract Slides
Video
Gernot Heiser
State of seL4-related research
Keynote at the seL4 Summit, October, 2022
Abstract Slides
Video
Gernot Heiser
seL4 overview: Principles, abstractions, use
Invited talk at the seL4 Summit, October, 2022
Abstract Slides
Video
Lucy Parker
The seL4 device driver framework
Talk at the 4th seL4 Summit, October, 2022
Abstract PDF Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer and John Shackleton
Cyberassured systems engineering at scale
IEEE Security and Privacy, Volume 20, Number 3, pp. 52–64, March, 2022
Abstract Slides
Video
Gernot Heiser
The seL4 report: State of the seL4 ecosystem
Keynote at the Trusted Computing Center of Excellence 2022 Summit, February, 2022
Abstract Slides
Video
Gernot Heiser
The seL4 Foundation – growing through upheaval
On-line, January, 2022
Abstract Slides
Video
Gernot Heiser
The formally verified seL4 microkernel – a high-assurance foundation for MCS
Keynote at IEEE Conference on Embedded and Real-Time Computing and Applications, August, 2020
Abstract PDF Gernot Heiser, Toby Murray and Gerwin Klein
Towards provable timing-channel prevention
ACM Operating Systems Review, Volume 54, Issue 1, pp. 1-7, August, 2020
Abstract PDF
Presentation Video
Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Luca Benini and Gernot Heiser
Prevention of microarchitectural covert channels on an open-source 64-bit RISC-V core
Workshop on Computer Architecture Research with RISC-V (CARRV), Valencia, Spain, May, 2020
Abstract PDF Gernot Heiser, Gerwin Klein and June Andronick
seL4 in Australia: From research to real-world trustworthy systems
Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020
Abstract Slides
Video
Gernot Heiser
Verified seL4 on secure RISC-V processors
at linux.conf.au, Gold Coast, January, 2020
Abstract PDF Konrad Slind, David Hardin, Johannes Åman Pohjola and Michael Sproul
Synthesis of verified architectural components for autonomy hosted on a verified microkernel
Hawaii International Conference on System Sciences, pp. 6365-6374, Grand Wilea, Hawaii, January, 2020
Abstract PDF Yanyan Shen, Gernot Heiser and Kevin Elphinstone
Fault tolerance through redundant execution on COTS multicores: Exploring trade-offs
International Conference on Dependable Systems and Networks (DSN), pp. 188-200, Portland, Oregon, USA, June, 2019
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
Slides
PDF
Presentation Video
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser
Time protection: The missing OS abstraction
EuroSys Conference, Dresden, Germany, March, 2019
Best Paper Award
Abstract PDF Yanyan Shen
Microkernel mechanisms for improving the trustworthiness of commodity hardware
PhD Thesis, UNSW, Sydney, Australia, March, 2019
Abstract Slides Gernot Heiser
What's new in the world of seL4?
Talk at FOSDEM'19, Brussels, February, 2019
Abstract PDF Darren Cofer, Andrew Gacek, John Backes, Michael Whalen, Lee Pike, Adam Foltzer, Michael Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser and Douglas Stuart
A formal approach to constructing secure air vehicle software
IEEE Computer, Volume 51, Issue 11, pp. 14-23, November, 2018
Abstract PDF Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez
Formally verified software in the real world
Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018
Abstract
Slides
PDF Simon Biggs, Damon Lee and Gernot Heiser
The jury is in: Monolithic OS design is flawed
Asia-Pacific Workshop on Systems (APSys), Korea, August, 2018
Abstract
Slides
PDF Qian Ge, Yuval Yarom and Gernot Heiser
No security without time protection: we need a new hardware-software contract
Asia-Pacific Workshop on Systems (APSys), Korea, August, 2018
Best Paper Award Complete timing-channel data for evaluated x86 and Arm platforms.
Abstract PDF Anna Lyons
Mixed-criticality scheduling and resource sharing for high-assurance operating systems
PhD Thesis, UNSW, August, 2018
Abstract Slides Gernot Heiser
The quest for the perfect API
Invited "Fireside Talk" at VMware on occasion of the virtualisation pioneer's 20th anniversary, April, 2018
Abstract PDF Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser
Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time
EuroSys Conference, Porto, Portugal, April, 2018
Abstract PDF Gernot Heiser
For safety's sake: we need a new hardware-software contract!
IEEE Design and Test, Volume 35, Issue 2, pp. 27-30, March, 2018
Abstract Slides
Video
Gernot Heiser
Flying autonomous aircraft: Mixed-criticality support in seL4
at linux.conf.au, Sydney, January, 2018
Abstract PDF Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson
Secure mathematically-assured composition of control models
Technical Report, Data61, CSIRO, September, 2017
Abstract PDF Kevin Elphinstone, Amirreza Zarrabi, Kent Mcleod and Gernot Heiser
A performance evaluation of rump kernels as a multi-server OS building block on seL4
Asia-Pacific Workshop on Systems (APSys), India, September, 2017
Abstract PDF Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray and Liam O'Connor
Provably trustworthy systems
Philosophical Transactions of the Royal Society A, Volume 375, Issue 2104, pp. 1-23, September, 2017
Abstract PDF Thomas Sewell, Felix Kam and Gernot Heiser
High-assurance timing analysis for a high-assurance real-time OS
Real-Time Systems, Volume 53, Issue 5, pp. 812-853, September, 2017
Abstract PDF Thomas Sewell
Translation validation for verified, efficient and timely operating systems
PhD Thesis, UNSW, Sydney, Australia, July, 2017
Abstract PDF Matthew Fernandez
Formal verification of a component platform
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016
Abstract PDF Gernot Heiser and Kevin Elphinstone
L4 microkernels: The lessons from 20 years of research and deployment
ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016
Abstract PDF Thomas Sewell, Chi Kam and Gernot Heiser
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016
Outstanding Paper award
Abstract PDF Daniel Matichuk, Toby Murray and Makarius Wenzel
Eisbach: A proof method language for isabelle
Journal of Automated Reasoning, Volume 56, Number 3, pp. 261–282, March, 2016
Abstract PDF Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz
Automated verification of a component platform
Technical Report, NICTA and UNSW, August, 2015
Abstract
Slides
PDF Sean Peters, Adrian Danis, Kevin Elphinstone and Gernot Heiser
For a microkernel, a big lock is fine
Asia-Pacific Workshop on Systems (APSys), Tokyo, JP, July, 2015
Abstract Slides Gernot Heiser
seL4: Present and future
invited talk at FOSDEM'15, Brussels, BE, February, 2015
Abstract PDF Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein and Mark Staples
Empirical study towards a leading indicator for cost of formal software verification
International Conference on Software Engineering, pp. 11, Firenze, Italy, February, 2015
Abstract Slides
Video
Gernot Heiser
seL4 is free — what does this mean for you?
Abstract, LCA.
Abstract
Slides
PDF Anna Lyons and Gernot Heiser
Mixed-criticality support in a high-assurance, general-purpose microkernel
Workshop on Mixed Criticality Systems, pp. 9–14, Rome, Italy, December, 2014
Abstract PDF Andrew Boyton
Secure architectures on a verified microkernel
PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014
Abstract PDF David Cock, Qian Ge, Toby Murray and Gernot Heiser
The last mile: An empirical study of some timing channels on seL4
ACM Conference on Computer and Communications Security, pp. 570–581, Scottsdale, AZ, USA, November, 2014
Abstract PDF Matthias Daum, Nelson Billing and Gerwin Klein
Concerned with the unprivileged: User programs in kernel refinement
Formal Aspects of Computing, Volume 26, Number 6, pp. 1205–1229, October, 2014
Abstract PDF David Cock
Leakage in trustworthy systems
PhD Thesis, UNSW, Sydney, Australia, August, 2014
Abstract PDF Thomas Sewell
Formal replay of translation validation for highly optimised c: Work in progress
Verification and Program Transformation, Vienna, Austria, July, 2014
Abstract PDF Gerwin Klein and Tobias Nipkow
Applications of interactive proof to data flow analysis and security
Software Systems Safety, pp. 77–134, Volume 36 in NATO Science for Peace and Security Series , IOS Press BV, 2014
Abstract
Slides
PDF Bernard Blackham, Mark Liffiton and Gernot Heiser
Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 169–178, Berlin, Germany, April, 2014
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 PDF Michael von Tessin
The clustered multikernel: An approach to formal verification of multiprocessor operating-system kernels
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, December, 2013
Abstract
Slides
PDF
Presentation Video
Kevin Elphinstone and Gernot Heiser
From L3 to seL4 – what have we learnt in 20 years of L4 microkernels?
ACM Symposium on Operating Systems Principles, pp. 133–150, Farmington, PA, USA, November, 2013
Abstract PDF Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
PDF Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick
Towards a verified component platform
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013
Abstract PDF Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
Abstract PDF Bernard Blackham
Towards verified microkernels for real-time mixed-criticality systems
PhD Thesis, UNSW, Sydney, Australia, October, 2013
2013 ACM SIGBED Paul Caspi Memorial Dissertation Award and John Makepeace Bennett Award for Australasian Distinguished Doctoral Dissertation
Abstract
Slides
PDF Gernot Heiser
Can truly dependable systems be affordable?
Keynote at APSys'13, Singapore, July, 2013
Abstract PDF Kevin Elphinstone and Yanyan Shen
Improving the trustworthiness of commodity hardware with software
Workshop on Dependability of Clouds, Data Centers and Virtual Machine Technology (DCDV), pp. 6, Budapest, Hungary , June, 2013
Abstract
Slides
PDF Thomas Sewell, Magnus Myreen and Gerwin Klein
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013
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 Toby Murray and Thomas Sewell
Above and beyond: seL4 noninterference and binary verification
Abstract, 2013 High Confidence Software and Systems Conference, Annapolis, MD, May, 2013.
Abstract
Slides
PDF Bernard Blackham and Gernot Heiser
Sequoll: A framework for model checking binaries
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 97–106, Philadelphia, USA, April, 2013
Best Paper Award
Abstract
Slides
PDF Gernot Heiser, Etienne Le Sueur, Adrian Danis, Aleksander Budzynowski, Tudor-Ioan Salomie and Gustavo Alonso
RapiLog: reducing system complexity through verification
EuroSys Conference, pp. 323–336, Prague, Czech Republic, April, 2013
Abstract
Slides
PDF Gernot Heiser
Protecting e-government against attacks
EP Workshop on Security of e-Government, pp. 5, Brussels, Belgium, February, 2013
Abstract PDF Daniel Matichuk and Toby Murray
Extensible specifications for automatic re-use of specifications and proofs
10th International Conference on Software Engineering and Formal Methods, pp. 8, Thessaloniki, Greece, December, 2012
Abstract PDF Daniel Matichuk
Automatic function annotations for hoare logic
Systems Software Verification, pp. 10, Sydney, Australia, November, 2012
Abstract PDF June Andronick, Andrew Boyton and Gerwin Klein
Final report for AOARD grant #FA2386-11-1-4070, formal system verification — extension
Technical Report, NICTA, October, 2012
Abstract PDF June Andronick, Gerwin Klein and Toby Murray
Formal system verification for trustworthy embedded systems, final report for AOARD grant #FA2386-10-1-4105
Technical Report, NICTA, October, 2012
Abstract PDF June Andronick and Gerwin Klein
Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022
Technical Report, NICTA, August, 2012
Abstract
Slides
PDF Bernard Blackham and Gernot Heiser
Correct, fast, maintainable — choose any three!
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
Abstract
Slides
PDF Bernard Blackham, Vernon Tang and Gernot Heiser
To preempt or not to preempt, that is the question
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
Abstract PDF June Andronick, Gerwin Klein and Andrew Boyton
Formal system verification — extension, AOARD 114070
Technical Report, NICTA, May, 2012
Abstract
Slides
PDF Bernard Blackham, Yao Shi and Gernot Heiser
Improving interrupt response time in a verifiable protected microkernel
EuroSys Conference, pp. 323–336, Bern, Switzerland, April, 2012
Abstract PDF Matthew Fernandez, Gerwin Klein and Ihor Kuz
Microkernel verification down to assembly
Poster presented at EuroSys 2012, April, 2012
Abstract PDF Gerwin Klein
Interactive proof: Applications to semantics
Software Safety and Security: Tools for Analysis and Verification, pp. 85–125, IOS Press, 2012
Abstract
Slides
PDF Michael von Tessin
The clustered multikernel: An approach to formal verification of multiprocessor OS kernels
2nd Workshop on Systems for Future Multi-core Architectures, pp. 1–6, Bern, Switzerland, April, 2012
Abstract PDF Gernot Heiser, Toby Murray and Gerwin Klein
It's time for trustworthy systems
IEEE Symposium on Security and Privacy, Volume 10, Number 2, pp. 67–70, March, 2012
Abstract PDF June Andronick, Gerwin Klein and Toby Murray
Formal system verification for trustworthy embedded systems, final report option 1 — AOARD 104105
Technical Report, NICTA, November, 2011
Abstract PDF Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser
Timing analysis of a protected operating system kernel
IEEE Real-Time Systems Symposium, pp. 339–348, Vienna, Austria, November, 2011
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 Bernard Blackham, Yao Shi and Gernot Heiser
Protected hard real-time: The next frontier
Asia-Pacific Workshop on Systems (APSys), pp. 5, Shanghai, China, July, 2011
Abstract
Slides
PDF Gernot Heiser, Leonid Ryzhyk, Michael von Tessin and Aleksander Budzynowski
What if you could actually Trust your kernel?
Workshop on Hot Topics in Operating Systems (HotOS), pp. 1–5, Napa, CA, USA, May, 2011
Abstract PDF Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood
Provable security: How feasible is it?
Workshop on Hot Topics in Operating Systems (HotOS), pp. 5, Napa, USA, May, 2011
Abstract PDF June Andronick and Gerwin Klein
Formal system verification for trustworthy embedded systems, final report AOARD 094160
Technical Report, NICTA, April, 2011
Abstract PDF June Andronick
From a proven correct microkernel to trustworthy large systems
International Conference on Formal Verification of Object-Oriented Software, pp. 1–9, Paris, December, 2010
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 June Andronick, David Greenaway and Kevin Elphinstone
Towards proving security in the presence of large untrusted components
Systems Software Verification, pp. 9, Vancouver, CA, October, 2010
Abstract PDF Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk
The road to trustworthy systems
ACM Workshop on Scalable Trusted Computing (ACMSTC), pp. 3–10, Chicago, IL, USA, October, 2010
Abstract PDF Gerwin Klein
The l4.verified project – next steps
Verified Software: Theories, Tools and Experiments, pp. 86–96, Edinburgh, UK, August, 2010
Abstract PDF Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker
capDL: A language for describing capability-based systems
Asia-Pacific Workshop on Systems (APSys), pp. 31–35, New Delhi, India, August, 2010
Abstract PDF Gerwin Klein
A formally verified OS kernel. now what?
International Conference on Interactive Theorem Proving, pp. 1–7, Edinburgh, UK, July, 2010
Abstract
Slides
PDF Michael von Tessin
Towards high-assurance multiprocessor virtualisation
6th International Verification Workshop, pp. 110–125, Edinburgh, UK, July, 2010
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 PDF Dhammika Elkaduwe
A principled approach to kernel memory management
PhD Thesis, UNSW, Sydney, Australia, May, 2010
Abstract PDF Gerwin Klein, Thomas Sewell and Simon Winwood
Refinement in the formal verification of seL4
Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 323–339, Springer, 2010
Abstract PDF Gerwin Klein
Correct OS kernel? Proof? Done!
USENIX ;login:, Volume 34, Number 6, pp. 28–34, December, 2009
Abstract PDF Andrew Boyton
A verified shared capability model
Systems Software Verification, pp. 25–44, Aachen, Germany, October, 2009
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   Michael von Tessin
Towards a formally verifiable multiprocessor microkernel
Poster presented at the 2009USENIX Annual Technical Conference, June, 2009
Abstract PDF Gerwin Klein, Ralf Huuck and Bastian Schlich
Operating system verification
Journal of Automated Reasoning, Volume 42, Number 2-4, pp. 123–124, April, 2009
Abstract PDF Gerwin Klein
Operating system verification — an overview
Sadhana, Volume 34, Number 1, pp. 26–69, February, 2009
Invited paper. Journal homepage.
Abstract PDF Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Verified Software: Theories, Tools and Experiments, pp. 99–115, Toronto, Canada , October, 2008
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 David Cock
Bitfields and tagged unions in C — verification through automatic generation
International Verification Workshop, pp. 44–55, Sydney, August, 2008
Abstract PDF Rafal Kolanski
A logic for virtual memory
Systems Software Verification, pp. 61–77, Sydney, Australia, July, 2008
Abstract PDF Kevin Elphinstone, David Greenaway and Sergio Ruocco
Lazy queueing and direct process switch — merit or myths?
Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), pp. 69–77, Pisa, Italy, December, 2007
Abstract PDF Gernot Heiser
Your system is secure? Prove it!
USENIX ;login:, Volume 32(6), pp. 35—38, December, 2007
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 Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Technical Report NRL-1474, NICTA, October, 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 Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone
A memory allocation model for an embedded microkernel
International Workshop on Microkernels for Embedded Systems, pp. 28–34, Sydney, Australia, January, 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 Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone
Kernel data – first class citizens of the system
Workshop on Object Systems and Software Architectures , pp. 39–43, Victor Harbor, South Australia, Australia, January, 2006
Abstract PDF Gernot Heiser
Secure embedded systems need microkernels
USENIX ;login:, Volume 30, Number 6, pp. 9–13, December, 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