4 ms·

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 "

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.

bregma 2y ago
QNX 8.0 was just released. The version bump represents a rewritten microkernel.
- speed_spread 2y ago
  Is QNX 8 seL4 based?
  - DoingIsLearning 2y ago
    QNX predates the first L4 release by at least 10 years. Unless they had a major rewrite I wouldn't assume so.
    - speed_spread 2y ago
      The comment I was replying to seemed to imply that QNX 8.0 is a full rewrite. I'm not sure how relevant that statement was here, unless the rewrite is seL4 based.
    - ahartmetz 2y ago
      Interestingly, QNX designers have learned and applied one of the same lessons as L4 designers: asynchronous messaging is messy regarding resource management and slower than well-executed synchronous messaging. QNX and L4 both use synchronous messaging for the vast majority of tasks.
      - vacuity 2y ago
        I find it unfortunate, since I think async should be the default model for communication. Similar to message passing with shared memory as an optimization, I wonder if async messaging with sync messaging as an optimization is feasible. Async in general does make reasoning about the program more difficult.
        ahartmetz 2y ago
        My intuition is similar to yours, but I trust people who have done the thing more than your or my intuition. Sync seems to require very responsive receivers, which is a desired property anyway, so maybe the downside isn't that great.
        rurban 2y ago
        Mach (with Hurd) went down this rabbithole and utterly failed. Mailboxes were the cause of the desaster.
panick21_ 2y ago
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 2y ago
  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.
riedel 2y ago
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/ https://www.redox-os.org/ . So sad that Liedke died so early, I really wonder what L5 would have looked like.
gnufx 2y ago
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/ http://www.microkernel.info/
lasiotus 2y ago
Motūrus OS (https://github.com/moturus/motor-os https://github.com/moturus/motor-os) has a newer microkernel.
snvzz 2y ago
seL4 remains the state of the art.
rurban 2y ago
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/ https://l4re.org/ I don't consider seL4 current, more like academic research.
mike_hearn 2y ago
There was an seL4 summit last year: https://www.youtube.com/@seL4/videos 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.
- bewo001 2y ago
  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 https://en.wikipedia.org/wiki/Exokernel
- vbezhenar 2y ago
  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).

bregma 2y ago

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

speed_spread 2y ago
Is QNX 8 seL4 based?
- DoingIsLearning 2y ago
  QNX predates the first L4 release by at least 10 years. Unless they had a major rewrite I wouldn't assume so.
  - speed_spread 2y ago
    The comment I was replying to seemed to imply that QNX 8.0 is a full rewrite. I'm not sure how relevant that statement was here, unless the rewrite is seL4 based.
  - ahartmetz 2y ago
    Interestingly, QNX designers have learned and applied one of the same lessons as L4 designers: asynchronous messaging is messy regarding resource management and slower than well-executed synchronous messaging. QNX and L4 both use synchronous messaging for the vast majority of tasks.
    - vacuity 2y ago
      I find it unfortunate, since I think async should be the default model for communication. Similar to message passing with shared memory as an optimization, I wonder if async messaging with sync messaging as an optimization is feasible. Async in general does make reasoning about the program more difficult.
      - ahartmetz 2y ago
        My intuition is similar to yours, but I trust people who have done the thing more than your or my intuition. Sync seems to require very responsive receivers, which is a desired property anyway, so maybe the downside isn't that great.
      - rurban 2y ago
        Mach (with Hurd) went down this rabbithole and utterly failed. Mailboxes were the cause of the desaster.

panick21_ 2y ago

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 2y ago
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.

riedel 2y ago

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/ https://www.redox-os.org/ . So sad that Liedke died so early, I really wonder what L5 would have looked like.

gnufx 2y ago

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/ http://www.microkernel.info/

lasiotus 2y ago

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

snvzz 2y ago

seL4 remains the state of the art.

rurban 2y ago

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/ https://l4re.org/ I don't consider seL4 current, more like academic research.

mike_hearn 2y ago

There was an seL4 summit last year: https://www.youtube.com/@seL4/videos 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.

bewo001 2y ago
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 https://en.wikipedia.org/wiki/Exokernel
vbezhenar 2y ago
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).