The seL4 microkernel

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

Publications

		Gernot Heiser LionsOS: A highly dependable operating system for cyberphysical systems Keynote at International Symposium on Parallel Computing and Distributed Systems, September, 2024
		Gernot Heiser LionsOS: Towards a truly dependable operating system Keynote at International Conference on Dependable Systems and Networks (DSN), June, 2024
		Gernot Heiser, Peter Chubb, Alex Brown, Courtney Darville and Lucy Parker sDDF design: design, implementation and evaluation of the seL4 device driver framework 2024
		Gernot Heiser The seL4 microkernel: Provable security for the real world Keynote at the International Workshop on Advanced Industrial Science and Technology, September, 2023
		Lucy Parker The seL4 device driver framework Talk at the 5th seL4 Summit, September, 2023
		Ivan Velickovic The seL4 Microkit Talk at the 5th seL4 Summit, September, 2023
		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
		Gernot Heiser Intelligent vehicle security needs a verified operating system Keynote at the International Workshop on Safety and Security of Intelligent Vehicles, June, 2023
		Gernot Heiser seL4 update: Foundation and TS R&D news Invited talk at the Trusted Computing Center of Excellence 2023 Summit, May, 2023
		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
		Gernot Heiser R&D update from Trustworthy Systems Talk at the 5th seL4 Summit, 2023
		Gernot Heiser State of seL4-related research Keynote at the seL4 Summit, October, 2022
		Gernot Heiser seL4 overview: Principles, abstractions, use Invited talk at the seL4 Summit, October, 2022
		Lucy Parker The seL4 device driver framework Talk at the 4th seL4 Summit, October, 2022
		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
		Gernot Heiser The seL4 report: State of the seL4 ecosystem Keynote at the Trusted Computing Center of Excellence 2022 Summit, February, 2022
		Gernot Heiser The seL4 Foundation – growing through upheaval On-line, January, 2022
		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
		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
		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
		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
		Gernot Heiser Verified seL4 on secure RISC-V processors at linux.conf.au, Gold Coast, January, 2020
		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
		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
		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
		Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser Time protection: The missing OS abstraction EuroSys Conference, Dresden, Germany, March, 2019 Best Paper Award
		Yanyan Shen Microkernel mechanisms for improving the trustworthiness of commodity hardware PhD Thesis, UNSW, Sydney, Australia, March, 2019
		Gernot Heiser What's new in the world of seL4? Talk at FOSDEM'19, Brussels, February, 2019
		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
		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
		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
		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.
		Anna Lyons Mixed-criticality scheduling and resource sharing for high-assurance operating systems PhD Thesis, UNSW, August, 2018
		Gernot Heiser The quest for the perfect API Invited "Fireside Talk" at VMware on occasion of the virtualisation pioneer's 20th anniversary, April, 2018
		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
		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
		Gernot Heiser Flying autonomous aircraft: Mixed-criticality support in seL4 at linux.conf.au, Sydney, January, 2018
		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
		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
		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
		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
		Thomas Sewell Translation validation for verified, efficient and timely operating systems PhD Thesis, UNSW, Sydney, Australia, July, 2017
		Matthew Fernandez Formal verification of a component platform PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016
		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
		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
		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
		Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz Automated verification of a component platform Technical Report, NICTA and UNSW, August, 2015
		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
		Gernot Heiser seL4: Present and future invited talk at FOSDEM'15, Brussels, BE, February, 2015
		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
		Gernot Heiser seL4 is free — what does this mean for you? Abstract, LCA.
		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
		Andrew Boyton Secure architectures on a verified microkernel PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014
		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
		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
		David Cock Leakage in trustworthy systems PhD Thesis, UNSW, Sydney, Australia, August, 2014
		Thomas Sewell Formal replay of translation validation for highly optimised c: Work in progress Verification and Program Transformation, Vienna, Austria, July, 2014
		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
		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
		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
		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
		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
		Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz CAmkES glue code semantics Technical Report, NICTA and UNSW, November, 2013
		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
		Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray CAmkES formalisation of a component platform Technical Report, NICTA and UNSW, November, 2013
		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
		Gernot Heiser Can truly dependable systems be affordable? Keynote at APSys'13, Singapore, July, 2013
		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
		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
		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
		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.
		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
		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
		Gernot Heiser Protecting e-government against attacks EP Workshop on Security of e-Government, pp. 5, Brussels, Belgium, February, 2013
		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
		Daniel Matichuk Automatic function annotations for hoare logic Systems Software Verification, pp. 10, Sydney, Australia, November, 2012
		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
		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
		June Andronick and Gerwin Klein Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022 Technical Report, NICTA, August, 2012
		Bernard Blackham and Gernot Heiser Correct, fast, maintainable — choose any three! Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
		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
		June Andronick, Gerwin Klein and Andrew Boyton Formal system verification — extension, AOARD 114070 Technical Report, NICTA, May, 2012
		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
		Matthew Fernandez, Gerwin Klein and Ihor Kuz Microkernel verification down to assembly Poster presented at EuroSys 2012, April, 2012
		Gerwin Klein Interactive proof: Applications to semantics Software Safety and Security: Tools for Analysis and Verification, pp. 85–125, IOS Press, 2012
		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
		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
		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
		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
		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
		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
		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
		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
		June Andronick and Gerwin Klein Formal system verification for trustworthy embedded systems, final report AOARD 094160 Technical Report, NICTA, April, 2011
		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
		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.
		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
		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
		Gerwin Klein The l4.verified project – next steps Verified Software: Theories, Tools and Experiments, pp. 86–96, Edinburgh, UK, August, 2010
		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
		Gerwin Klein A formally verified OS kernel. now what? International Conference on Interactive Theorem Proving, pp. 1–7, Edinburgh, UK, July, 2010
		Michael von Tessin Towards high-assurance multiprocessor virtualisation 6th International Verification Workshop, pp. 110–125, Edinburgh, UK, July, 2010
		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
		Dhammika Elkaduwe A principled approach to kernel memory management PhD Thesis, UNSW, Sydney, Australia, May, 2010
		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
		Gerwin Klein Correct OS kernel? Proof? Done! USENIX ;login:, Volume 34, Number 6, pp. 28–34, December, 2009
		Andrew Boyton A verified shared capability model Systems Software Verification, pp. 25–44, Aachen, Germany, October, 2009
		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 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
		Michael von Tessin Towards a formally verifiable multiprocessor microkernel Poster presented at the 2009USENIX Annual Technical Conference, June, 2009
		Gerwin Klein, Ralf Huuck and Bastian Schlich Operating system verification Journal of Automated Reasoning, Volume 42, Number 2-4, pp. 123–124, April, 2009
		Gerwin Klein Operating system verification — an overview Sadhana, Volume 34, Number 1, pp. 26–69, February, 2009 Invited paper. Journal homepage.
		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
		Rafal Kolanski and Gerwin Klein Mapped separation logic Verified Software: Theories, Tools and Experiments, pp. 15–29, Toronto, Canada, October, 2008
		David Cock Bitfields and tagged unions in C — verification through automatic generation International Verification Workshop, pp. 44–55, Sydney, August, 2008
		Rafal Kolanski A logic for virtual memory Systems Software Verification, pp. 61–77, Sydney, Australia, July, 2008
		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
		Gernot Heiser Your system is secure? Prove it! USENIX ;login:, Volume 32(6), pp. 35—38, December, 2007
		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
		Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Technical Report NRL-1474, NICTA, October, 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 Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007
		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
		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
		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
		Gernot Heiser Secure embedded systems need microkernels USENIX ;login:, Volume 30, Number 6, pp. 9–13, December, 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