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 world runs on Unix and as a consequence, computer viruses, malware, spyware and ransomware are all common vocabulary terms. We traded this security away for nothing.
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.
> People like to snob Unix but the fact is: the world runs on Unix.
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.
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?
It’s fundamentally full of concepts incompatible with capability based security principles, which are provably secure. Access control lists are provably insecure. POSIX resource management is archaic. It’s not possible to define “ownership” clearly on a Unix system.
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.
"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.
You could build a POSIX system on seL4, but it won't take advantage of the capabilities that seL4 provides, because capabilities are absent from the POSIX APIs. Consider for example:
There's nothing in this function signature which specifies a capability to perform the open. Instead, there's an access control list somewhere else, where permission is looked up as to whether the file can be accessed by the current uid or whatever.
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).
Not arguing about the merits of capabilities and the open interface, but file handles are often cited as capability-like, and the ...at calls are in POSIX; but there's the global namespace. (Security in Plan 9 does say their capability system could be implemented for Unix, but I don't know if that's realistic and whether it provides proper capability security.)
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.
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.
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.
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).
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.
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.
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.
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.
41 comments
[ 2.8 ms ] story [ 43.7 ms ] threadProceedings 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 ; )
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.
[1] https://sel4.systems/
[2] https://barrelfish.org/
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.
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).
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.
https://en.wikipedia.org/wiki/Exokernel
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.