SeL4 Whitepaper [pdf]

SeL4 Whitepaper [pdf]
sel4.systems

> seL4 is also a hypervisor. seL4 supports virtual machines that can run a fully fledged guest OS such as Linux

> seL4 is the world’s fastest microkernel

current users aren't very loud about it. RTI is implementing DDS for sel4. productionization is still early days. DARPA is pushing for it. you might look at the speakers, sponsors, and attendees of the sel4 conferences and workshops :)

(here they talk about seL4 capabilities which are different to )

> The confused deputy problem is the “killer app” for capabilities, as the problem is un-solvable with ACLs. Hence, next time someone is trying to sell you a “secure” OS, not only ask whether they have a correctness proof for the OS, but also whether it uses capability-based access control. If the answer to either questions is “no”, then you’re being offered snake oil

bit before that there is also a "shout-out" to SELinux:

> While in some ways more secure than standard Linux, seLinux suffers from the same problem as standard Linux: a huge TCB, and correspondingly huge attack surface. In other words, seLinux is an add-on to a fundamentally insecure operating system and thus remains fundamentally insecure. In contrast, seL4 provides bullet-proof isolation from the ground up.In short, seLinux is not suitable for truly security-critical uses, while seL4 is designed for them.

and containers:

> A typical scenario is that a user wants to run an untrusted program (downloaded from the internet) to process a particular file but wants to prevent the program from accessing any other files the user has access. This is called a confinement scenario, and there is no clean way to do this in Linux, which is the reason people came up with heavyweight workarounds (I like to call them hacks)such as “chroot jails”, containers etc

some of it I think is justified if they see themselves competing for the hypervisor and hard RTOS markets. Also they seem to distance themselves from Genode, which IMO serves a very different purpose (composability):

> Genode is in many ways a more powerful and general framework, that supports multiple microkernels and already comes with a wealth of services and device drivers, especially for x86 platforms. It is arguably more convenient to work with than CAmkES, and is certainly the way to get a complex system up quickly. However, Genode has drawbacks: 1. As it supports multiple microkernels, not all as powerful as seL4, Genode is based on the least common denominator. In particular, it cannot use all of seL4’s security and safety features. 2. It has no assurance story.

here a whole post by Norman Freske's in praise of seL4 back in 2016 (he is maintainer of Genode and did some talks that year at FosDem):

https://www.osnews.com/story/29377/genode-1608-brings-intera...

==

As much as I want seL4 succeed I wonder if they will reach critical adoption levels. One of the challenge in Linux is managing complexity of all these policies. SELinux done right is a continuous effort (and of course it's huge because user-space is huge). seL4 not even manages the memory for you, it's all in user-space (e.g. a Linux Guest OS). It's therefore a bit of a privileged statement and unfair comparison.

The "seL4 capabilities" and Linux (capabilities.h) are apples and oranges. User-land Linux is a constantly moving target, you don't have that on a unique network or industrial appliance. Imagine the tears (from users and maintainers) if Linux distributions started to enforce firejail policies and that every systemd.service file came with a correct list of "allowed system calls". No distribution would do that because the work involved would be massive and continuous and all but those who care about endpoint security would leave (what % would that be idk but I think it is massive).