[adamretter]

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.

[mike_hearn]

There was an seL4 summit last year:

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.

[vbezhenar]

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).

[bewo001]

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.

https://en.wikipedia.org/wiki/Exokernel

[bregma]

QNX 8.0 was just released. The version bump represents a rewritten microkernel.

[speed_spread]

Is QNX 8 seL4 based?

[panick21_]

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.

[wittystick]

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.

[gnufx]

I don't know how complete it is -- it doesn't list DeVault's Helios -- but various projects are listed at http://www.microkernel.info/

[riedel]

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.

[rurban]

OKL4 is the most widely used L4 spinoff, and Kernkonzept's L4Re based on Dresden's Fiasco comes much closer than seL4. https://l4re.org/

I don't consider seL4 current, more like academic research.

[lasiotus]

Motūrus OS (https://github.com/moturus/motor-os) has a newer microkernel.

[snvzz]

seL4 remains the state of the art.