What does seL4’s license imply?

This question comes up again and again, and from talking to people, I realise that there are a lot of misconceptions about seL4 licensing and what it implies, in particular in terms of the infectiveness of the GPL. I tried to address this at my talk at the recent seL4 Summit, and will repeat and expand on what I said there.

Spoiler: The GPL license of seL4 has even less impact on you than the license of Linux would. It is not forcing any licensing conditions of anything that is of any value to you, and most likely not on anything you should be touching at all.

Licenses

The seL4 kernel is licensed under GPLv2,  version 2 of the Gnu General Public License – exactly the same license that is used for the Linux kernel. The core implication is the same as for Linux: Work derived from the kernel (be it additions, modifications or other enhancements) become automatically GPLed, but anything running on top of the kernel (i.e. in usermode) is unaffected and can be under any license.

We specifically license any usermode code we developed from scratch (libraries and components such as drivers and file systems) under the permissive 2-clause BSD license, to allow people to build arbitrary systems on top of seL4 and license them as they see fit. We do license some generally useful tools under GPL to maximise the benefit to the community, but no-one who uses seL4 is forced to use those tools.

A similar story holds for proofs: Our proofs about the kernel itself are under GPLv2, while proofs about user-level code are a mixture of GPLv2 and BSD licenses.

Implications

So, while in an abstract sense, things are exactly as in Linux, in practice there is a huge difference: GPL infectiveness in seL4 is only limited to code you should most likely not touch at all. This is a result of seL4 being a microkernel: the kernel only contains code that must run in the privileged mode of the hardware, everything else is left to user mode. This means that everything that does anything “useful”, such as file systems, device drivers, network protocol stack, resource management, definition of security policies, etc, is left in user mode, and can therefore be under any license. The kernel (after booting) is just a fast context-switching engine that happens to enforce isolation with the strength of mathematical proof.

This is in stark contrast to Linux, where all of the things listed above are inside the kernel (and thus subject to the GPL). As the figure shows, with seL4 all the “interesting” code, in particular anything that could be valuable IP of the adopter of seL4, is at user level, and can be under any license. This specifically includes device drivers, which might reveal valuable hardware IP – with seL4 these can be kept closed. With Linux, you’d be forced to open-source them. Similarly, if you add a new file system or improve an existing one, provide improved network protocols, etc, you can do this without open-sourcing with seL4, but not with Linux.

In short, with seL4, any IP of real value can be licensed under conditions chosen by the owner, while in Linux, much IP would have to be open-sourced. This includes everything in the “your system services” box in the diagram, as well as the driver part of the platform-port box below. Compared to the size of the seL4 kernel (order of 10kLOC), this is huge (typically 100s of kLOC), much bigger than it might appear from the simple diagram.

In fact, you shouldn’t ever modify any of the GPLed kernel code, unless you’re doing a new platform port. The reason is simple: if you modify seL4, you invalidate verification. And the verification is the real value of seL4 (besides minor details such as seL4 being the fastest of its kind, and also the most advanced 😉) so why would you want to throw it away? With broken verification, it’s no longer seL4!

What actually must be open-sourced with seL4 is some minimal platform support. But this is simple and pretty boring boilerplate stuff:

• You’ll need a simple timer driver (so the kernel can perform time-slice preemption). A typical example consists of less than 20 LOC (split between header and implementation body). This is if your platform has a timer device that’s different from any existing supported platform, and there’s a good chance there is one already. Typically you’d lift that code out of Linux anyway.
• You’ll need a serial port driver (used for kernel debugging, but not in the production kernel). A typical example is less than 10 LOC! Again, it may already exist or you borrow it form Linux. No valuable IP anywhere near.
• Then there’s an interrupt controller. That’s another 500 LOC or so spread over multiple files. Much of it is addresses, more addresses and register layouts, and some generic code that probably exists already.
• You may also need some code for handling the System MMU (SMMU) and cache management functions, but those are becoming increasingly standardised.

As I said, none of this is IP of any value, and chances are that most of it exists already and you won’t have to do much more than defining the memory layout of your platform. A concrete example is the patch needed for supporting the i.MX8: about 20 lines of definitions in total. Scared of “giving it away”? Why would you?

[Thanks Kent McLeod for digging out the code examples.]

Why are we doing it this way?

People sometimes suggest we should just change the license to BSD. This would be a really bad idea! To demonstrate what I mean here I asked the Summit participants who had done a project involving Linux before. Unsurprisingly, almost everyone put their hand up. I then asked who had done a project with BSD Unix. Two academics raised their hand.

This says a lot about the power of licensing. Experts generally agree that BSD Unix was technically superior to Linux. Yet Linux dominates the world, and BSD Unix exists in academia and some niche applications, the only significant usage is its descendant Darwin, which forms the core of macOS and iOS (but not many know this).

Why did this happen? The reason is that, lacking strong leadership and using a permissive license, BSD forked into oblivion.

We will not allow the same to happen to seL4. We want seL4 to grow and become the one and only choice of OS for security- and safety-critical systems. The GPL is part of that strategy (and the forthcoming seL4 Foundation is the other).