The SeL4 Microkernel: An Introduction [pdf]

Being "formally proven" to be free of various flaws did not make seL4 immune to memory corruption flaws. Despite the formal proof, a memory corruption flaw was found a few years ago. The PRs for the commits fixing it and amending seL4's proof are public:

https://github.com/seL4/seL4/pull/243

https://github.com/seL4/l4v/pull/453

You will find a number of other memory related bugs in its issue tracker:

https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...

Interestingly, the PR fixing "register clobbering" in memory was not labelled bug, so it is not listed when you filter by "bug".

I used to think seL4 was immune to these issues given its proof allegedly saying it is, but upon seeing this, I have come to think that the proof is not as comprehensive as the wider community has been lead to believe. That said, seL4 is still a very impressive piece of software.

Finally, to answer your question. The specification that seL4 meets is published on github:

https://github.com/seL4/l4v

Has anyone added another formally proven layer or component? Yes, they're being added all the time. Recently added features:

- Support for a bunch of new architectures, including RISC-V. - Mixed criticality scheduling, which provides capability-based access to CPU time, mechanisms to limit the upper bound of execution of a thread, ensuring that high-criticality tasks have priority and access to necessary resources, and allowing "passive servers" which run on scheduling time donated by the caller. - Microkit, a new verified abstraction layer which made it much much easier to build actual systems using seL4. - Very recently, the Device Driver Framework, a device-driver template, control and data plane implementation, and tools for writing device drivers and providing device virtualisation for high-performance I/O on seL4.

Formal verification can guarantee that specific requirements hold in specific conditions. It's true that in general such requirements and conditions can be quite narrow. But seL4 itself has a whole lot of proofs about it, covering a wide range of properties that one would want in a kernel, and these guarantees hold under very weak assumptions. Even the correctness of the C compiler is not assumed, they have a separate tool which looks at the compiler output and proves that the compiled binary behaves correctly with respect to the required C semantics.

The requirements that seL4 meets include the following: the binary code of the seL4 kernel correctly implements the behaviour described in the abstract specification and nothing more. There are no buffer overflows, no memory leaks, no pointer errors or null pointer dereferences, no undefined behavior in the C code, no termination of the kernel apart from the explicit ways enumerated in the spec, etc. The specification and therefore the seL4 binary satisfy the security properties of integrity and confidentiality: the former means that there is absolutely no way for a process to change data that the process has no explicit permission to change, and the latter means that a process cannot, in any way, read data it has no explicit permission to read. It even shows that a process without permission cannot indirectly infer the data through certain side channels. Beyond security, the expected worst-case execution-time guarantees and scheduling properties are also met.

The developers of seL4 have been in funding hell for years. Most of their work was darpa research for remotely controlled drones. The US Military would very much like drones that can't be hacked.

Their current work is on LionsOS which is more towards greater adoptions: https://lionsos.org/

For example: No buffer overflows, null pointer exceptions, use-after-free, etc. On ARM and RISCV64 not even the C compiler has to be trusted, because functional correctness has been proven for the binary. And there are more proofs besides functional correctness. https://docs.sel4.systems/projects/sel4/frequently-asked-que...

https://github.com/auxoncorp/ferros

Lots of type-level programming for tracking resources, hardware access, and capabilities at compile-time and trying to bring some of the underlying kernel guarantees up to the compiler because finding out about and debugging issues at runtime was just the absolute worst.

The document was updated in January.

A lot has happened in the last few years, such as the founding of seL4 foundation, the maturation of mixed criticality scheduling, the celebration of multiple seL4 summits, and the deployment in practical use by multiple companies and countries, in several scenarios.

In high-assurance, formal methods were one of many used for the system. It was reduced complexity, precisely-specified behavior, likewise for security policy, proofs the design/code fulfilled it, exhaustive testing, leak analysis, pestering, and ability to recheck all this.

That's so hard it was mostly done for only kernels commercially. From there, your real-world use will involve user-level components, protocols with interactions, and so on. Add one thing to the proven TCB and maybe your proof disappears. So, every trusted component has to be rigorously designed. Then, all the interactions for a holistic argument.

Most don't do that. For example, seL4 hosting a web browser won't help you if it's a web application. IBOS and a WAF on seL4, all proven, might cover that. Harder argument. Most of these projects never go beyond the kernel or TLS stack or whatever.

You can do stuff with that. Look up Nizza Secure Systems Architecture for a paper with many examples. Yet, they usually don't cut it. They're not compatible with popular apps either. So, most people just harden Linux or BSD or Windows.

Sounds like your setup would make for an interesting read in longer form

Could you elaborate on how your servers use seL4? And are these production, commercial servers?

Are there notable uses of Genode?

The question is always "how big of a replacement are we talking?" Redox seems to be committed to interoperate well with POSIX, which naturally informs its design decisions. And there's a huge difference between having technical capabilities and succeeding. Although if Redox does succeed, it would already be a good step. seL4 is even more extreme in these qualities: its technical advantages are superb, but so far (and I think this will continue) it does not have what it takes, whatever that encompasses, to be the Next Big Thing. Ignoring political considerations, I think microkernels will be successful, and rightfully so.

>I would hesitate to consider it as a replacement for Linux

It would depend on the scenario. Of course, Linux is easier to work with but OTOH there are requirements which only seL4 can satisfy.

There's a lot required on top of seL4 for it to be actually useful. Fortunately, there has been a lot of Open Source work there as well. This is where seL4 is in a much better position than just a few years ago.

For static scenarios, there's LionsOS[0], quite usable already.

For dynamic scenarios, there's the Provably Secure, General-Purpose Operating System[1], which is still early stages.

Both can be found in the Projects page[2] at trustworthy systems, which is linked in the seL4 website.

0. https://trustworthy.systems/projects/LionsOS/

1. https://trustworthy.systems/projects/smos/

2. https://trustworthy.systems/projects/

No, that's the advantage is that the kernel/processes don't need to be trusted since your kernel guarantees the isolation. So you can have a Linux kernel running next to some high security process with the guarantee that they will be isolated (with the exception of allowed IPC)

No.

But there are limitations. DMA off, only formally verified drivers

It's also important to note that se4L multicore kernel is not yet verified.

In absolute terms, sure. At the practical level, you can find a partial answer in the section 7.2 of the paper.

The guarantees offered by the kernel cannot be subverted by unprivileged processes running on it.

Of course, the kernel is not very useful on its own, thus the design of drivers, filesystem servers and other services running on top of the kernel is still relevant.

Note that, unlike most other systems (including Linux) which are flawed at a fundamental level, seL4 actually enables the construction of a secure and reliable system.

I think there's a meaningful difference between "based on" and "inspired by", Helios being the latter.

https://en.wikipedia.org/wiki/L4_microkernel_family seems to describe it having been used all over the place, though mostly in embedded contexts.

> OKL4 shipments exceeded 1.5 billion in early 2012,[4] mostly on Qualcomm wireless modem chips. Other deployments include automotive infotainment systems.[13]

> Apple A series processors beginning with the A7 contain a Secure Enclave coprocessor running an L4 operating system[14] called sepOS (Secure Enclave Processor OS) based on the L4-embedded kernel developed at NICTA in 2006.[15] As a result, L4 ships on all modern Apple devices including Macs with Apple silicon.

Jochen Liedtke became a professor in 1999 in Karlsruhe, sadly he passed away only shortly after in 2001. I don't know if his successor Bellosa still does research on L4. There was the L4Ka project which appears to be completed. In the bachelor lecture on OS by him it's not part of the curriculum.

Rittinghaus, alumni of Bellosa, is involved with Unikraft [0], which was featured a couple of times on hn, and is using unikernel technology.

[0] https://unikraft.org/

Well, an L4 variant is used in iPhones: "The Secure Enclave Processor runs an Apple-customized version of the L4 microkernel." https://support.apple.com/de-at/guide/security/sec59b0b31ff/...

the L4Re derivative (open source) is running in every single id.X Volkswagen car in the central "icas1" ECU, carrying Linux and other guests.

https://www.kernkonzept.com/kk_events/elektrobit-advances-au...

afaics the L4Re kernel also is part of Elektrobit Safe Linux.

I love the work (and the direction) the Karlsruhe team did on L4Ka, especially with Pistachio - the design was clean, simple, easy to grasp.

I did a Pistachio-based OS for my diploma thesis (not at Karlsruhe). I always thought that if I'd been studying there, I'd probably go into OS research.

L4, L4Ka developed in Karlsruhe is not the same as seL4.

The utility of microkernels is orthogonal to hardware/software co-design.

From a practical engineering perspective, monolithic kernels were faster/easier/had more resources behind them and security is as robust as can be had with C (i.e. best effort and full of bugs). Lots of hardware has been introduced to try and mitigate that mess. But you theoretically wouldn't need a security co-processor with SeL4 because you have a very high degree of confidence that processes are isolated from each other and there are no root level exploits. So yes, hardware/software codesign is important!

That being said, the team behind SeL4 has had to spend a lot of engineering resources on eliminating side channels from the hardware. Hardware is also faulty as the real world doesn't care about your physics simulation.

The benefits of a microkernel here is that it is small enough for formal verification to be tractable. The proof itself is 10x the size of the kernel. Context switching on SeL4 is an order of magnitude faster than Linux, so the performance impact should be negligible. But if we magically could verify the millions of lines of a monolithic kernel, then it would still be faster to not do context switching. Indeed, the SeL4 team tried to move the scheduler to userspace but it cost too much in terms of performance. So it was kept in and added to the proof burden.

> It's like the difference between a 80286 and a 80386: The latter added the hardware support for true multitasking that the former lacked.

I'm not sure this is a good comparison. The 286 did support true multitasking in protected mode, and it was used in many non-DOS operating systems. What the 386 added (among other things) is the virtual 8086 mode which allowed it to multitask existing real mode DOS applications that accessed hardware directly.

That doesn't seem right. Even with strong hardware protections, how is Linux's TCB comparable to a microkernel? Unless it just recreates the exact same protection domains, there will be more vulnerability in Linux. Rather, the thing about hardware is primarily that it makes things more efficient. For example, microkernels nowadays are already quite robust because they make good use of certain hardware: the MMU. Then the small TCB of a microkernel gives the kernel credibiity, so the kernel and hardware together make for a solid infrastructure. So really it's a matter of how much "cheating" we're allowed to do with hardware, but microkernels overall utilize the protection better. Or see exokernels.

> Am I off base?

Yes. There is still plenty of work to be done in the OS research space. There has to be software interfaces and API's to all this new hardware.

I also think there is a lot to be learned from using micro/hybrid systems which are much more composable. e.g. Plan 9 is a great example of a hybrid system which makes use of a singular protocol, 9P, to serve all objects in the system to userspace. It is hybrid because some parts are in-kernel to avoid the overhead of system calls such as IP, and TLS. Another interesting design aspect is how the in-kernel drivers are minimal mostly acting as a 9P interface to the hardware logic. This way you A. turn a machine object like a pointer or record into a seekable file and B. secured that file using standard unix permissions and C. can easily distribute the components across machines via a network. Now you can securely push the driver logic into a userspace program. And 9p is network and architecture transparent meaning you can work across multiple machines running on Arm, x86, mips, etc. All this come out of the box.

When I go back to Linux/Unix or Windows from Plan 9 its a sad and frustrating time. They're about as flexible as igneous rock. All the features are ad-hoc bolted on in mutually incompatible ways using a myriad of protocols that all do the same thing - serve files/objects. Ugh.

In seL4's virtualization support, VM exceptions are turned into messages and handled by VMM, a task running in unprivileged mode.

VMM has no more capabilities than the VM itself, thus a VM escape would be, outside of academics, of no value.

Refer to pages 8 to 10 in the OP PDF.

I will caution that IPC microbenchmarks should not be taken as confirmation that the "academic microkernel" is viable: OS services all in userspace and with fine granularity as is appropriate. Often microkernel-like designs like VMMs/hypervisors and exokernels make use of unikernels/library OSes on top, which reduces the burden of fast IPC somewhat. Or developers intentionally lump protection domains to reduce IPC burden. Of particular note: even seL4 did not evict its scheduler to userspace. Since the scheduler is the basis behind time management, it's quite a blow to performance if the scheduler eats up time constantly. My own thoughts there are that, with care, a userspace scheduler can efficiently communicate with the kernel with a shared memory scheme, but that is not ideal. But for desktop and mobile, a microkernel design would be delightful and the performance impact is negligible. We need far more investment on QoS there.

Edit: That being said, we should be building microkernel-based OSes, and if for some cases performance really is a restricting factor, they will be exceptions. The security, robustness, flexibility, etc. of microkernels is not to be understated.

Drivers in userspace is not particularly microkernelly - most of the major monolithic kernels have supported this to some degree or another for years (it is easy in principle, just transmit I/O requests to userspace servers over some channel) while many historic microkernels (see e.g. Mach 3) did not do it. It hardly changes the architecture of the system at all.

It is moving the higher-level things into userland that is the harder problem, and the one that has been challenging for microkernels to do well.

seL4 having a proof of correctness does not mean all microkernels do. In fact, seL4 is the only microkernel that has a proof of correctness. If you build on top of it in the microkernel way, you quickly find that it is not performant. That is why NT and XNU both abandoned their microkernel origins in favor of becoming monolithic kernels.

To the best of my knowledge, seL4 is not AVX-512 aware. The AVX-512 state is not saved or restored on a context switch, which is clearly going to impact efficiency.

At present there's 16x64-bits of register state saved (128B), but if we were to have full support for the vectors, you need to potentially add 32x512-bits to the state (plus another 16 GP registers when APX arrives). Total state that needs moving from registers to memory/cache would jump to 2304B - a 1800% increase.

Give that memory is still the bottleneck, and cache is of limited size, a full context switch is going to have a big hit - and the main issue with microkernels is that a service you want to communicate with lives in another thread and address space. You have: app->kernel->service->kernel->app for a round-trip. If both app and service use the AVX-512 registers then you're going to have to save/restore more than half a page of CPU state up to 4 times, compared with up to 2 on the monolithic kernel which just does app->kernel->app.

The amount of CPU state only seems to be growing, and microkernels pay twice the cost.

I feel like containers and Kubernetes are microkernels revenge.

They are for all practical purposes fulfilling the same role.

I heard a joke somewhere that sel4 is even more successful than Linux because it is running below ring 0 in every Intel chip shipped in the past N decades, plus probably many others.

Yes and there's a very good reason: Linux is safe enough, more efficient, and more scalable.