Skip to content

seL4 is finally free! Can you afford not to use it?

2014/08/17

The world’s most highly assured operating system (OS) kernel

… the only one with a formal proof of implementation correctness (freedom from bugs), the only one with a proof of security that extends all the way to the executable code, the only protected-mode OS with sound worst-case execution time (WCET) bounds, is finally free. It is available under the same license as the Linux kernel, the GPL v2. Everyone can use it, and everyone should. And, as I’ll explain, they may, one day, be considered negligent for not using seL4, and such liability could reasonably start with any system that is designed from now on.

Critical systems

Let’s expand on this a little. Let’s assume you, or our company, is building a device/system whatever which has safety or security requirement. There are lots of these, where failure could lead to death or injury, loss of privacy, or loss of money. Many systems that are part of everyday life fall into that category, not only national-security type of systems (but those obviously do too).

Medical implants

Medical implants could kill a patient or fail to keep them alive if they fail. Such systems may fail because their critical functionality (that keeps the patient alive) is compromised by a “non-critical” part that misbehaves (either by a bug triggered during normal operation, or a vulnerability exploited by an attacker). Most implants have such “non-critical” code, in fact, it tends to be the vast majority of the software on the device. Most devices these days have some wireless communication capability, used for monitoring the patient, the state of the device, and maybe even to allow the physician to adjust its operation. On systems not built on seL4, there can be no guarantee that this “non-critical” software is free from dangerous faults, nor can there be a guarantee that its failure cannot cause the critical bits to fail.

Cars

Complex software in a car could misbehave and compromise critical components like engine control, breaks, air bags. Attacks on cars are well documented. The CAN networks in cars are fundamentally vulnerable, so many of the devices on the bus can be the starting point of an attack. Furthermore, functionalities that used to run on separate ECUs (microprocessors) are increasingly consolidated onto shared processors, creating more potential vulnerabilities. Car hacks clearly have the potential to kill people.

Industrial automation

Industrial automation systems are in many ways – other than scale 😉 – similar to medical implants: Some critical functionality (which may or may not be small but is likely to be highly assured) runs beside large, complex software stacks that supports monitoring, control, reprogramming etc, and is far too complex for high assurance to be feasible. If such a system misbehaves it may cause millions of dollars worth of damage, or even endanger lives.

Others

There are many other systems where failure is expensive or dangerous. They include systems performing financial transactions (eg point-of-sale systems or ATMs), voting machines, systems holding or providing access to personal data (cards with medical history, etc).

There are many more examples.

Limitations

Of course, seL4 cannot give a complete guarantee of no failure either. The hardware could fail, the system could be ill-designed or wrongly configured, or few other things could go wrong. But it definitely (for a well-designed and -configured system) makes it impossible for a compromised “non-critical” subsystem to interfere, through a software fault, with the critical part. This is by far the most likely source of error, and seL4 gives you the highest degree of certainty achievable to date that this won’t happen.

So, why would you not want to use seL4 in your next design?

Let’s examine the reasons people usually give.

License

seL4 is published under the GPLv2. This means that any improvements will have to be open-sourced as well, which is a concern to some people.

I claim this is mostly a misconception. Nothing you build on top of seL4 will be affected by the kernel’s license (just as you can build closed-source stuff on Linux). seL4 contains the GPL to the kernel, and our license files have explicit wording (taken from Linux) confirming that.

How about changes to seL4 itself? Reality is that you aren’t likely to make significant changes to seL4. For one, any change will invalidate the proofs. Ok, maybe you don’t care too much about this, as even if it’s not 100% verified, even a slightly modified seL4 system will be massively more dependable than anything else. So maybe you want to do some “improvements” and then keep them to yourself?

As long as those are actual “improvements”, I suspect that you won’t be able to outrun the momentum that’s behind seL4 at present. No-one knows better than us how to improve seL4 even more (despite it already being much better than any comparable system), and we keep doing this. And if you have a real use case that requires some improvements, you’re better off talking to us than to try on your own.

Or maybe your improvements are really adaptations to proprietary hardware. In most cases that will be a non-issue, as seL4 contains no device drivers (other than a timer and the interrupt-controller driver), so any proprietary stuff isn’t likely to be visible to the kernel. But if you really have to modify the kernel in a way that exposes sensitive IP, then you can always get access under a different license (for a fee). If this is your situation then talk to us.

Processor architecture

Maybe you want to run seL4 on a processor that isn’t presently supported. As long as it’s a supported CPU architecture (ARM and x86) then that isn’t a big deal, and we can help you porting. If you need it on a different architecture (say Power) then that would involve a fair bit more work. Still, you should talk to us about a port, the cost is likely to be a small fraction of your overall project cost, and will be tiny compared to the potential cost of not using seL4 (more on that below).

Performance

I thought our work in the past 20 years was enough to debunk the “microkernels are slow” or even “protection is too expensive” nonsense. Ok, some microkernels are slow, and, in fact, almost all commercial ones are, especially the so-called high-assurance ones (OKL4 is an exception). But seL4 isn’t. It runs loops around all the crap out there! And OKL4, shipped in billions of power-sensitive mobile devices, has shown that a fast microkernel doesn’t cause a performance problem. Performance is definitely one of the more stupid excuses for not using seL4!

Resource usage

Unless you have an extremely constrained system, then seL4 is small (compared to just about everything else). If you’re running on a low-end microcontroller (with not only serious resource constrains but also no memory protection) you should look at our eChronos system instead.

Legacy

Your design has to re-use a lot of legacy software that is dependent on your old OS environment. Whether that’s a real argument probably depends a lot on how well your legacy software is written. If it is essentially unstructured homebrew that doesn’t abstract common functionality into libraries, then you may have a real problem. In the sense of having a real problem, which is going to bite you hard sooner or later, whether you’re migrating to seL4 or not. If that isn’t the case, then there is likely to be a sensible migration path, the cost of which is likely to be dwarfed by the potential cost of not using seL4 (see below).

Environment and support

seL4 is a young system, with a limited support environment in terms of libraries and tools. That is true, but it’s also changing rapidly. We’ll see userland developing quickly. And don’t you think that just because it’s open source there isn’t good support. Between NICTA and GD and our partners, we can certainly provide highly professional support for your seL4-based development. Just talk to us.

So, what’s the trade-off?

Well, ask yourself: You’re developing some critical system. Critical in the sense that failure will be very costly, in terms of lost business, lost privacy, loss of life or limb. Imagine you’re developing this based on yesterday’s technology, the sort of stuff others are trying to sell you, and what you may have been using believing (at the time at least) that it was state of the art. Now it ain’t.

So, imagine you are developing this critical system and decide not to use seL4. And, sooner or late, it fails, with the above costly consequences. You may find yourself in court, being sued for many millions, trying to explain why you developed your critical system using yesterday’s technology, rather than the state of the art. I wouldn’t want to be in your shoes. In fact, I might serve as an expert witness to the other side, which argues that you should have known, and that doing what you did was reckless.

Do you want to run that risk? For what benefit?

Think carefully.

Advertisements
3 Comments
  1. sara permalink

    Ugh. GPL is not truly free software. I wish it were public domain or MIT license. The GPL is only FSF free, not copyfree.

  2. It actually is, under the original definition of “free software”: https://en.wikipedia.org/wiki/Free_software#Definition

    Gernot

  3. macrokernel-dude permalink

    > formal proof of implementation correctness (freedom from bugs),
    Gernot, you should read your FAQ. http://sel4.systems/FAQ/#zerobugs. It might be you oversimplified a bit in that statement. But of course it is always easier to redefine bugs as “unexpected features”, right 😉

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: