All mitigations to achieve microkernel like capabilities.
Xen is unfortunately large, and the full hypervisor runs privileged.
With seL4, VM exceptions are forwarded to VMM, which handles them.
From a security standpoint, a VM escape would only yield VMM privileges, which are no higher than that of the VM itself. This is much better than a compromise of Xen, which would compromise all VMs in the system.
Makatea[0] is an effort to build a Qubes-like system using seL4 and its virtualization support. It is currently funded by a NLNet grant.
Hypervisors, userspace drivers, containers, language runtime sandboxes, bytecode deployments, driver and kernel sandboxes (safe kernel / driver guard),container only distributions,...
If you can CI/CD in minutes a reduced kernel+app and reboot in 100ms your network-facing thing (be it nginx or haproxy) you might just take latest vanilla anyway...
How would we go about GPUs, NCs, and many kinds of drivers?
My desktop, on which I am the only person with an account, has 49 "users", of which 11 are actively running a process.
At work, every daemon we run has a dedicated user.
On android, every app runs as its own user.
It's like why it doesn't matter if you are running as root or not. The user account has access to whats important, like a database or keychain.
To elaborate, seL4 claims to be the fastest kernel around[0], a claim that remains unchallenged.
To put it into context, the difference in IPC speed is such that you'd need an order of magnitude more IPC for a multiserver system based on seL4 to actually be slower than Linux.
A multiserver design would imply increased IPC use, but not an order of magnitude.
From an observer on the sidelines: there was no namecalling.
He said you trolled, not that you ate a troll. The distinction is important.
Even the best of us troll, sometimes. (Not claiming you did btw, just that there was no name calling.)
[0]: https://trustworthy.systems/publications/full_text/Elphinsto...
Can I run Firefox or PostgreSQL on seL4? Or another real-world program of comparable complexity? And how does the performance of that compare to Linux or BSD?
That's really the only benchmark that matters; it's not hard to be fast if your kernel is simple, but simple is often also less useful. Terry Davis claimed TempleOS was faster than Linux, and in some ways he was right too. But TempleOS is also much more limited than Linux and, in the end, not all that useful – even Terry ran it inside a VM.
I've heard these sort of claims about seL4 before, and I've tried to look up some more detailed information about seL4 before, and I've never really found anything convincing on the topic beyond "TempleOS can do loads more context switched than Linux!" type stuff.
> seL4 is the world’s fastest operating system kernel designed for security and safety
Linux is arguably not designed for security and safety but it blows seL4 out of the water when it comes to performance. There’s a reason it only gets used in contexts where security is critical; I would have expected that you would be aware of this considering you were the one who is promoting it.
Citation needed.
And by that I mean actual benchmarks of Linux doing the few tasks seL4 does, such as IPC or context switching, faster than seL4.
The multiserver architecture does indeed imply an elevated use of IPC, but it does in no way outweigh the difference in IPC cost.
In this model, data sharing, and the implied locking, is minimized, which as a consequence helps SMP scaling.
Dragonfly, while not multiserver proper, took a different direction than Freebsd and Linux by optimizing IPC and not implementing fine-grained locks, and instead favoring concurrent lockless and lockfree servers.
As a consequence, Dragonfly scales much better than Freebsd, and in many benchmarks manages to outperform Linux.
This is despite the tiny development team, particularly so when considered relative to the amount of funding these two systems get.
I am sickened by the effort that's being wasted on a model that we know is bad and does not work. Linux will never be high assurance, secure or scale past a certain point.
Fortunately, no matter how long it'll take, the better technology will win; there's no "performance hack" that a bad system can pull to catch up with the better technology once it's there.
Just a matter of time.
Reminder the kernel has over a million LoCs, or megabytes of object code.
Perhaps we should start thinking about whether it is a good idea to run something this large in supervisor mode, with full privileges.
I wouldn't say it is sensible in a world where seL4 exists.