From L3 to seL4: 20 years of L4 microkernels (2013) [video]
youtube.com
youtube.com
https://www.youtube.com/@seL4/videos
Anyway the trend has been that regular mainstream kernels steadily adopt more microkernel-like features when it can be shown to not harm performance too much. MacOS/iOS aren't technically microkernels, but they incorporate Mach into the core and a typical system will have thousands of possible servers that can be reached via Mach. Those servers are all sandboxed pretty heavily too, so you get the security benefits. The core filesystem and networking stack do still run in kernel mode because there aren't many benefits there (moving them to user space doesn't remove them from the TCB and) but over time more and more stuff has been kicked out to user space. The same can be seen in Windows where over time more subsystems get extracted to user space servers.
Linux has a less well defined architecture than Apple's platforms and there are way fewer services reachable via DBUS than on macOS, but the same trends can be seen there too with support for direct user space access to devices, FUSE, user space schedulers, eBPF and so on.
So there isn't I think much interest in pure microkernels now. Linux has got flexible enough that you can make it as micro-kernelly as you want, but the current balance seems about right for nearly all use cases. The stuff that remains in-kernel generally isn't a big source of vulnerabilities, moving stuff to userspace wouldn't help anyway but would reduce performance a lot.
Honestly I feel that Linux server users are performance freaks and will kill for 0.1% performance. So it's very unlikely that they'll trade anything for it. They don't need stability, they'll just recreate server if necessary. They need absolute minimum of security (otherwise they would use VMs instead of containers).
Sync seems to require very responsive receivers, which is a desired property anyway, so maybe the downside isn't that great.
I don't consider seL4 current, more like academic research.
Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles November 2013
Are there any projects trying to make a universal UNIX operating system with sel4?
I know of Genode, but is there anything more simple/traditional?
PS: Helios is also there but not based directly on seL4
Thank you very much for the link, and yes you are absolutely right. I should have wrote unix'i or plan9'i or better just a universal operating-system, i meant with that not just a hypervisor but a "real/full" os on top of seL4.
And yet Unix is powering all the supercomputers, six of the seven magnificent seven, the AI revolution, nearly every single computer in all the datacenters around the world, billions of "small" devices, etc.
Can we really do that much better or is it just hubris?
At what point another approach, like the one Windows used, would be considered a failure? Once it's only powering the corporate world and not much else?
And at what point another approach would be considered a success? Once it has replaced Unix on all the supercomputers and in all the datacenters?
People like to snob Unix but the fact is: the world runs on Unix.
P.S: I wrote "Unix" with an 'i' and not a star because I have no clue how to write a star in HN's powerful text editor ; )
Linus Torvalds would have told you its system call performance, but Linux is also forced to solve these problems with things like futexes and io_uring, which carry over just as easily to microkernels.
Nowadays the excuse is side-channel attacks make any attempts at security pointless anyways so the kernel has exploded in size and complexity. This is insane logic, not least of all because side-channel attacks are read-only and can’t embed themselves into your system permanently through a bug in a browser JIT.
Linux is used purely because of all of its drivers and familiarity. Not on technical merits.
Can be prevented[0][1][2].
0. https://trustworthy.systems/publications/
1. https://trustworthy.systems/publications/papers/Sison_BMKH_2...
2. https://trustworthy.systems/publications/papers/Buckley_SWMM...
The world you are aware of runs on it.
> Can we really do that much better or is it just hubris?
Yes. Have a look at seL4[1] and Barrelfish too[2], even though that's no longer active. seL4 in particular is powering a lot of highly secure computing systems. There is a surprisingly large sphere outside of Unix/POSIX.
You could certainly write a Unix abstraction layer on top of seL4, or more commonly treat seL4 as a hypervisor, but you would not be able simply use a Unix interface to interact with seL4 and get all of it’s benefits.
Capability based systems don’t magically carry their desired properties up the abstraction ladder, they have to be maintained and the designer has to be vigilant to avoid introducing ambient authority by using capability based design themselves.
Genode is an example of a layer over seL4 that follows these principles.
If it's not too late to ask, where can we read about that? I've only ever seen ACL v. capability discussed in terms of trades-off as far as I remember.
Also, why it's inadequate?
"Unix 2.0" which is basically plan9/9front, uses namespaces, cpu, auth and so on 'servers' to authenticate users and even shared devices over the network.
FILE *fopen(const char *filename, const char *mode)
Rule #1 of capabilities is: Don't separate designation from authority. Rather than a filename, a capability based API for opening files should take a capability argument instead of a filename, which both designates which file to open and provides the authority to open it, without attempting to look up that authority elsewhere. And notably, this capability cannot be forged - it can't be generated from a string containing the name of the file.
So the first step to making a POSIX on seL4 is to get rid of the POSIX API and replace it with a better API based on capabilities. Then of course, it is no longer POSIX.
The reason to use capabilities rather than ACLs is that ACLs are vulnerable to confused deputy attacks. Linux namespaces have numerous security vulnerabilities that could be avoided with capabilities. Also note that POSIX "capabilities" are not proper capabilities in the sense they're used in capability based security (as in seL4).