That video is from 2013. Is anyone aware of an update for the last ten years which covers 2013 to 2023? I would like to understand if seL4 is still considered "current" or there have been newer developments since then that are worth considering. I have searched around a bit, and apart from Google's Fuscia Zircon, or Unikernel's like UniKraft, other L4 spin-offs and XNU I am not finding too much about newer modern microkernels.
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.
I don't see this trend with Linux. FUSE is very old and does not seem to get much traction. User space schedulers: where are they used? eBPF is like the other way around: people want to run more stuff inside kernel.
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).
For high-speed networking, exokernel concepts are now being used in the form of DPDK (user space) and eBPF/XDP (user code dynamically verified and loaded into kernel space). Exokernels aimed to move kernel functionalities not into a bunch of separate processes like microkernels, but into libraries. In the late 1990s, I worked on such a system which unfortunately fell victim to the dotcom crash.
seL4 is still being worked on. There are recent changes to the wat time is tracked. I would say in terms of research seL4 is still up there. The current trend is very much on verification of user space and also verification chains down to RISC-V.
Probably the biggest development in seL4 since this is the MCS (mixed criticality systems) addition, which provides capabilities for budgeting CPU usage to give guarantees for components that need higher priority. There's some videos by Gernot Heiser on YouTube covering it.
I just thought if L4 pistachio was a thing in the days (C++ rewrite, the new thing when I did my masters in Karlsruhe), someone must have written a microkernel OS in Rust by now and here it is: https://www.redox-os.org/ . So sad that Liedke died so early, I really wonder what L5 would have looked like.
Not Unix but Lions OS[1]. Also, why would you want to build Unix on top of seL4? I think we can have better ideas than that in today's state of the art.
>Also, why would you want to build Unix on top of 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.
> I think we can have better ideas than that in today's state of the art.
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 ; )
The problem with Unix is the abstractions it provides, not its implementation. Basing Unix off seL4 changes nothing of what makes Unix inadequate in 2024.
The problem with Unix is that the abstractions don't match today's adversarial computing environment. If seL4 can provide kernel-level process (tree) isolation, which part of Unix is inadequate for 2024?
"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.
I think one problem is that SEL4 lacks proper multi-core support. According to the FAQ it has not been formally verified, and it relies on a big lock for everything. This is fine when powering a security chip like T2, but not so fine if you are trying to replace UNIX.
Readit News
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).
https://en.wikipedia.org/wiki/Exokernel
I don't consider seL4 current, more like academic research.
Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles November 2013
https://dl.acm.org/doi/10.1145/2517349.2522720
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
[1] https://trustworthy.systems/projects/LionsOS/
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 ; )
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.
Deleted Comment