BT

Secure Microkernel seL4 Reaches Version 7

| by Kevin Neaton Follow 2 Followers on Oct 31, 2017. Estimated reading time: 3 minutes |

Version 7.0.0 of the seL4 microkernel has been released, bringing with it an alternate CMake-based build system with support for out-of-source builds and interactive configuration. Support for standalone ia32 builds and aarch64 specific documentation are also included in this release.

seL4 is a high-assurance open-source microkernel with strong isolation guarantees backed up by an end-to-end proof. In practice, this means that the seL4 codebase is bug-free in that it will behave as specified given that the proof assumptions are met. As such, it has been used to isolate critical trusted components from untrusted components running on the same processor.

The seL4 microkernel has been developed, maintained and formally verified by NICTA (now the Trustworthy Systems Group at Data61) and is owned by General Dynamics C4 Systems (GDC4S). NICTA and GDC4S decided to open-source seL4 in 2014 "in the hope that this will help everyone to build more dependable (safe, secure, reliable) computer systems."

The initial proof of functional correctness was completed in 2009 via the L4.verified project, showing that the code correctly implements the formal kernel specification. Subsequent work resulted in a comprehensive formal verification of the kernel by proving both that the specification satisfies desirable high-level security properties such as “availability, authority confinement, integrity, and confidentiality” and that those properties survive translation to the code and binary levels. The combined result is the first end-to-end proof of a general-purpose operating system kernel. Notably, the proof has continued to grow and evolve alongside the kernel for over a decade, making it the first proof at this scale to do so.

By design, the seL4 kernel has retained a high degree of performance despite the massive verification effort, which has actually aided the implementation of performance optimizations. Properties and invariants provided by the existing proof were used to inform the worst case execution time (WCET) analysis of the kernel resulting in improvements to the kernel implementation and further reductions in the WCET. Similarly, a fastpath was added to automatically speed up inter-process communication (IPC) when possible. The proof was then extended to verify that the kernel behavior conforms to the specification, whether the fastpath is used or not. The result of this effort is a provably fast, secure, and reliable kernel with application areas including defense, automotive, avionics, medical devices, and industrial automation.

In the US, over $2.3 million has been awarded through the SBIR (Small Business Innovation Research) program to fund defense projects related to seL4. In one such project, the SMACCM team used seL4 to build "highly hack-resilient" unmanned aerial vehicles (UAVs). The team used seL4 to isolate a virtualized Linux instance running non-critical code from critical code running on the same “mission board”. The Blue Team was able to operate the seL4-based system effectively while the Red Team attempted to hack it. The system was developed using a normal quadcopter and later transferred to the Unmanned Little Bird (ULB) autonomous helicopter developed by Boeing. But seL4 is not just for defense contractors. With support for the Raspberry Pi 3, the development of safe, secure, and reliable seL4-based systems is within the reach of students as well.

Although seL4 represents the state-of the art in secure operating systems development, it is minimal by definition and does not include all of the things that make using a fully featured operating system like Linux convenient, such as support for a wide range of devices and easy inter-process communication.

The status of ongoing development and verification efforts is provided by the development and verification roadmap which is updated frequently. Answers to common questions can be found on the project's FAQ page.

Rate this Article

Adoption Stage
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread
Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Discuss

Login to InfoQ to interact with what matters most to you.


Recover your password...

Follow

Follow your favorite topics and editors

Quick overview of most important highlights in the industry and on the site.

Like

More signal, less noise

Build your own feed by choosing topics you want to read about and editors you want to hear from.

Notifications

Stay up-to-date

Set up your notifications and don't miss out on content that matters to you

BT