>Measured performance shows a vast improvement over the CAmkES-based framework, as well as significantly better performance than Linux, despite the higher number of system calls and context-switches required. In particular we find that a highly componentised sDDF system easily distributes across cores, while each individual component being strictly sequential, reducing its complexity.
>The framework, running on the Microkit, clearly over-achieves our goal of “performance comparable to Linux”, outperforming Linux by a significant margin under all configurations evaluated. Performance is vastly better than that of the CAmkES system adapted to our transport layer (which is already a significant improvement over the performance of the previous CAmkES-based driver framework). The performance comparison to Linux is especially encouraging, given that the Linux IP stack is supposedly well optimised (especially for multicore use), while we are using the simple lwip [Dunkels, 2001]. We find that even on multicore (the scenario most favourable to Linux) our per-packet costs are significantly lower.
1. The document you link states that seL4 requires a specific CPU design that is work-in-progress by Integrated Systems Lab (a RISC-V CPU of course) to provide the claimed guarantees. This makes no sense in the context of testing performance of mitigations, which are fixes to silicon or microcode bugs fixed in later CPUs or microcode updates. If seL4 can require a hypothetical CPU to be secure, I can also just respond with a hypothetical CPU and microcode where all known bugs are fixed so no mitigations are needed.
In either case, you cannot have made benchmark on a hypothetical CPU, so the question becomes: does seL4 have appropriate mitigations for current buggy CPUs or does its security model just fall apart on those?
2. The document you link make it appear as if their focus is purely in the form of explicitly classified security partitions, and does not provide protections within the partition. This requires trust between all processes in a security partition, and I suspect in turn means that their performance between security domains is significantly worse.
This makes me suspicious of performance tests that artificially boost results in ways that are not representative of real-world performance, by comparing an seL4 system with a few security domains that only apply mitigations occasionally, with a Linux systems that assign a "security domain" to every process and apply mitigations constantly. Design benefits aside, and ignoring the actual mitigation effectiveness, these would be very different security and trust profiles.
This is why all benchmarks and performance claims need to include detailed test procedures to have any value whatsoever.
>The document you link states that seL4 requires a specific CPU design that is work-in-progress by Integrated Systems Lab (a RISC-V CPU of course) to provide the claimed guarantees.
I did not link a single document, but an index of relevant documents. The specific award winning paper from 2021 you quote, however, is quite interesting, and elaborates on the hardware requirement, which is spearheaded by seL4, but not specific to seL4 in any way.
RISC-V was inevitably chosen for this research; RISC-V has high suitability for research due to its openness/licensing.
As for the mitigations you are interested on, they were implemented in a timely manner ages ago. Older documents cover that. You need to scroll way down to ~2018 for the relevant papers.
>The document you link make it appear as if their focus is purely in the form of explicitly classified security partitions, and does not provide protections within the partition. This requires trust between all processes in a security partition, and I suspect in turn means that their performance between security domains is significantly worse.
Refer to 10.2.2 in the same document.
>This is why all benchmarks and performance claims need to include detailed test procedures to have any value whatsoever.
Is it not just ipbench[0], which they published alongside the paper?
While I know it wasn't meant bad I thought I'd note that others like might see such remarks in negative light, detracting from your point. Let the paper talk for itself, rather than claim it has value because others gave it an award.
> RISC-V was inevitably chosen for this research; RISC-V has high suitability for research due to its openness/licensing.
Nothing wrong with RISC-V, but my point is that protections that require a non-existent CPU has no practical value right now, nor do protections for that CPU matter if you run, say, x86_64 or ARM as is the norm.
With that in mind, any claims that require features of this CPU, while academically interesting, is purely a distraction when it comes to evaluating current security and performance, in particular whether performance is representative or a result of a higher or lower security guarantee.
> As for the mitigations you are interested on, they were implemented in a timely manner ages ago. Older documents cover that. You need to scroll way down to ~2018 for the relevant papers.
2018? Either that is non-representative of their mitigations, or their work is 6 years out of date with new CPUs, microcode updates, vulnerabilities and mitigations having been implemented since then. The last CPU vulnerability I heard of was just last month, affecting Intel Atom.
seL4 mitigations could be better, and could be better performing, but comparisons are only valid if they cover the same vulnerabilities. If these are not matched, a better option is to disable all mitigations at compile-time in both OS's. These mitigations massively affect context switch overhead, and lack of a particular mitigation can give an unfair benefit in either direction.
> Is it not just ipbench[0], which they published alongside the paper?
(It is found by going to the linked release page, then clicking on the git tag, then clicking on the link to trustworthy.systems, scrolling down to the Documentation section and then clicking on the sDDF design doc.)
Things I find lacking:
1. The paper tests several seL4 kernels, starting with SMP compiled out entirely, then gradually adding barriers and finally running full SMP. Only one Linux kernel with no information about its configuration is tested. It does note that "distributions had significant effect", and that they compiled mainline. There are numerous relevant compile-options to test on the Linux side as well.
2. The paper clarifies that they clearly tuned CPU affinity on seL4, data locality, presumably also buffers sizes and what not, while no such effort appears done on Linux. A test was run that limited scheduler choices to two cores, but that seems to be it.
3. It appears that no consideration of io_uring was done, meaning that the test did not try to achieve the best possible results on Linux even in the stock configuration. That does not invalidate the data, but that Linux can do better than the posted numbers as-is is something to consider.
4. The paper mentions that sDDF-like drivers can be implemented on linux through UIO, but seems to not mention that user-space drivers have been used for ages for super high-performance networkign in the form of DPDK which could fairly easily have been tested at the time of writing.
5. Generally speaking, I feel that the description of the setups were only cursory to give a high-level overview, but severely lacking from the sense of allowing the results to be replicated or analyzed by others. This is especially sad when we are primarily dealing with software configuration which can be trivially documented to perfect replication.
With all that in mind, I find the data somewhat lacking, and suspect that tuning, and in particular use of modern APIs, would allow Li...
is SeL4 anywhere near usability by regular humans? is that even it's design purpose? Are we going to see the equivalent of Arch Sel4 that I can install, run wayland to get a gui, and replace my linux stuff?
It is not. The closest thing you'll get to it that has the features you mention, is Qubes OS [0].
When it comes to the L4 family, Google's adoption of seL4 [1] might be interesting to you, and possibly L4Re [2] [3], which is open source (not their tooling, though) with commercial support.
Edit: there's a bunch more open source activity in this field, but I'm not familiar with it.
> Sparrow is a project to build a low-power secure embeded platform for Ambient ML applications. The target platform leverages RISC-V and OpenTitan. The Sparrow software includes a home-grown operating system named CantripOS, that runs on top of seL4 and (ignoring the seL4 kernel) is written almost entirely in Rust.
Just to add an interesting information, the famous GNU Hurd project had the goal of making a system like L4 usable by regular humans. (Later on, they changed it to work literally with L4.)
That doesn't mean any project to do that will have the fate of Hurd. But it is a huge and complicated task.
This is interesting. GNU inherits a lot from ITS, DDT and Emacs openness, where they had no security at all and you could edit the files from the whole system and import processes locally and over the network.The security there was to behave like a lady/gentelman and help/get helped.
Also, crackers weren't interested as everyone could see everything users where doing at any moment. Data security? Restoring from tapes.
By setting up an open system on top of a permissions bound system (Unix) having limitations as an user looks really weird and with full of rough edges everywhere, with limited permissions even to mount a hard disk image.
Namespaces in Hurd (+ maybe guix) solve that by giving the user lots of freedom to install and share whatever it wants without breaking a system.
That would explain why it never seemed to move forward.
TBF, that makes it quite explicit that the problem of Hurd never getting ready was due to the project governance (as in "this is not a goal"). A project that uses Mach could never get big.
Kind of actually, just depends how much you mean by "regular human"--it's not super popular but the Sculpt OS[1] release of Genode is a pretty solid system runnable on top of SeL4 that supports emulation for the features it's otherwise missing (a la wifibox). Have not personally used it yet but I believe the developers dogfood it on some decently modern hardware (think Framework). It has a very specific design ethos and aesthetic[2] that I find super compelling.
Very interesting. I couldn't find a high-level overview of how they're approaching this though. It seems like they might be re-implementing some Linux APIs, but I have the impression that it runs all those APIs in a single process, like hosting a UNIX or Linux kernel as a guest OS, which would be a fairly large TCB. Is there a reference document that describes the system architecture in more detail? Their handbook is a little thin on details.
It's interesting that they have some kind of subsystem to run code in kernel space too, very against typical microkernel thinking for isolation/safety reasons.
Nowhere near the usability of Linux, let alone something like MacOS.
I'd be really happy if I could easily deploy small self-contained embedded applications using general purpose ARMv8 processors. Like one would do with an infotainment system for a car, which is currently done primarily with QNX.
> Nowhere near the usability of Linux, let alone something like MacOS.
Like if there was a clear order of usability between Linux and MacOS :) it's more a matter of habits and preferences (and religion maybe for some ^^) than anything else.
MacOS seemed downright rough the few times I've had to use it. It's not intuitive and stuff often seems buggy until you get that dreaded spinning pinwheel...
"Intuitive" is not an objective property, it's too polluted by habits you've learned from other systems.
But we can say this: there's nothing intuitive about Windows' incomplete transition to the new settings app that still sometimes requires you to jump to the old control panel system; there's nothing intuitive about Linux' 50 desktop environments, each with their own incomplete configuration systems. In any kind of match up, MacOS will win on simplicity and intuitiveness hands down simply because every other option is just much worse.
> "Intuitive" is not an objective property, it's too polluted by habits you've learned from other systems.
To an extent, but then the test is seeing how people who have never used any system interact. I maintain the MacOS paradigm is objectively less intuitive than alternatives.
> But we can say this: there's nothing intuitive about Windows' incomplete transition to the new settings app that still sometimes requires you to jump to the old control panel system; there's nothing intuitive about Linux' 50 desktop environments, each with their own incomplete configuration systems
Sure, that's clumsy. Not really relevant though.
> In any kind of match up, MacOS will win on simplicity and intuitiveness hands down simply because every other option is just much worse.
Strongly disagree. MacOS comes in behind Windows for certain, and likely behind a couple of FOSS DEs as well. Windows has issues, but usability isn't one of them.
An easier-to-use driver framework seems like a step in the right direction. It also seems like the list of drivers is still extremely small.
I understand that use as a general purpose OS by non-technical people is a long ways away, but is there a general/mature guide to porting applications from other OSes? How far away are we from being able to easily deploy things like robotics applications on platforms like RPi? For example:
* GStreamer
* ROS
* OpenCV
* custom-built applications in languages like Rust or Java
Java is super easy to use in robotics, although probably not as free beer, that is a kind of market that keeps commercial Java vendors like PTC, Aicas and microEJ in business.
I know it’s easy to use in robotics, my problem is more that in order to use it, you have to use Linux or Windows or bypass the benefits of an OS altogether. Java on SeL4 would be great to have.
Using shared rings of buffers is almost but not quite what io_uring provides? It looks like it takes an io_uring style approach and natively so unless I’m misreading?
Have the performance numbers somewhere been validated?
38 comments
[ 1.7 ms ] story [ 88.7 ms ] thread>Measured performance shows a vast improvement over the CAmkES-based framework, as well as significantly better performance than Linux, despite the higher number of system calls and context-switches required. In particular we find that a highly componentised sDDF system easily distributes across cores, while each individual component being strictly sequential, reducing its complexity.
>The framework, running on the Microkit, clearly over-achieves our goal of “performance comparable to Linux”, outperforming Linux by a significant margin under all configurations evaluated. Performance is vastly better than that of the CAmkES system adapted to our transport layer (which is already a significant improvement over the performance of the previous CAmkES-based driver framework). The performance comparison to Linux is especially encouraging, given that the Linux IP stack is supposedly well optimised (especially for multicore use), while we are using the simple lwip [Dunkels, 2001]. We find that even on multicore (the scenario most favourable to Linux) our per-packet costs are significantly lower.
In recent times it also requires studying seL4's implementation of modern CPU vulnerability mitigations.
0. https://trustworthy.systems/projects/timeprotection/
In either case, you cannot have made benchmark on a hypothetical CPU, so the question becomes: does seL4 have appropriate mitigations for current buggy CPUs or does its security model just fall apart on those?
2. The document you link make it appear as if their focus is purely in the form of explicitly classified security partitions, and does not provide protections within the partition. This requires trust between all processes in a security partition, and I suspect in turn means that their performance between security domains is significantly worse.
This makes me suspicious of performance tests that artificially boost results in ways that are not representative of real-world performance, by comparing an seL4 system with a few security domains that only apply mitigations occasionally, with a Linux systems that assign a "security domain" to every process and apply mitigations constantly. Design benefits aside, and ignoring the actual mitigation effectiveness, these would be very different security and trust profiles.
This is why all benchmarks and performance claims need to include detailed test procedures to have any value whatsoever.
I did not link a single document, but an index of relevant documents. The specific award winning paper from 2021 you quote, however, is quite interesting, and elaborates on the hardware requirement, which is spearheaded by seL4, but not specific to seL4 in any way.
RISC-V was inevitably chosen for this research; RISC-V has high suitability for research due to its openness/licensing.
As for the mitigations you are interested on, they were implemented in a timely manner ages ago. Older documents cover that. You need to scroll way down to ~2018 for the relevant papers.
>The document you link make it appear as if their focus is purely in the form of explicitly classified security partitions, and does not provide protections within the partition. This requires trust between all processes in a security partition, and I suspect in turn means that their performance between security domains is significantly worse.
Refer to 10.2.2 in the same document.
>This is why all benchmarks and performance claims need to include detailed test procedures to have any value whatsoever.
Is it not just ipbench[0], which they published alongside the paper?
0. https://github.com/au-ts/ipbench
While I know it wasn't meant bad I thought I'd note that others like might see such remarks in negative light, detracting from your point. Let the paper talk for itself, rather than claim it has value because others gave it an award.
> RISC-V was inevitably chosen for this research; RISC-V has high suitability for research due to its openness/licensing.
Nothing wrong with RISC-V, but my point is that protections that require a non-existent CPU has no practical value right now, nor do protections for that CPU matter if you run, say, x86_64 or ARM as is the norm.
With that in mind, any claims that require features of this CPU, while academically interesting, is purely a distraction when it comes to evaluating current security and performance, in particular whether performance is representative or a result of a higher or lower security guarantee.
> As for the mitigations you are interested on, they were implemented in a timely manner ages ago. Older documents cover that. You need to scroll way down to ~2018 for the relevant papers.
2018? Either that is non-representative of their mitigations, or their work is 6 years out of date with new CPUs, microcode updates, vulnerabilities and mitigations having been implemented since then. The last CPU vulnerability I heard of was just last month, affecting Intel Atom.
seL4 mitigations could be better, and could be better performing, but comparisons are only valid if they cover the same vulnerabilities. If these are not matched, a better option is to disable all mitigations at compile-time in both OS's. These mitigations massively affect context switch overhead, and lack of a particular mitigation can give an unfair benefit in either direction.
> Is it not just ipbench[0], which they published alongside the paper?
For others, the paper you talk about but didn't link to is here: https://trustworthy.systems/projects/drivers/sddf-design.pdf
(It is found by going to the linked release page, then clicking on the git tag, then clicking on the link to trustworthy.systems, scrolling down to the Documentation section and then clicking on the sDDF design doc.)
Things I find lacking:
1. The paper tests several seL4 kernels, starting with SMP compiled out entirely, then gradually adding barriers and finally running full SMP. Only one Linux kernel with no information about its configuration is tested. It does note that "distributions had significant effect", and that they compiled mainline. There are numerous relevant compile-options to test on the Linux side as well.
2. The paper clarifies that they clearly tuned CPU affinity on seL4, data locality, presumably also buffers sizes and what not, while no such effort appears done on Linux. A test was run that limited scheduler choices to two cores, but that seems to be it.
3. It appears that no consideration of io_uring was done, meaning that the test did not try to achieve the best possible results on Linux even in the stock configuration. That does not invalidate the data, but that Linux can do better than the posted numbers as-is is something to consider.
4. The paper mentions that sDDF-like drivers can be implemented on linux through UIO, but seems to not mention that user-space drivers have been used for ages for super high-performance networkign in the form of DPDK which could fairly easily have been tested at the time of writing.
5. Generally speaking, I feel that the description of the setups were only cursory to give a high-level overview, but severely lacking from the sense of allowing the results to be replicated or analyzed by others. This is especially sad when we are primarily dealing with software configuration which can be trivially documented to perfect replication.
With all that in mind, I find the data somewhat lacking, and suspect that tuning, and in particular use of modern APIs, would allow Li...
It is not. The closest thing you'll get to it that has the features you mention, is Qubes OS [0].
When it comes to the L4 family, Google's adoption of seL4 [1] might be interesting to you, and possibly L4Re [2] [3], which is open source (not their tooling, though) with commercial support.
Edit: there's a bunch more open source activity in this field, but I'm not familiar with it.
[0] https://www.qubes-os.org/
[1] https://opensource.googleblog.com/2022/10/announcing-kataos-...
[2] https://l4re.org/
[3] https://www.youtube.com/watch?v=x8jxINR-q40
https://github.com/kernkonzept/manifest/wiki#tutorials
https://l4re.org/rpi.html
https://l4re.org/doc/
https://www.youtube.com/watch?v=oqm6GOniQ_k
https://www.youtube.com/watch?v=WGjAxsEAWRI
https://www.youtube.com/watch?v=6s5FDX5PkZI
> Sparrow is a project to build a low-power secure embeded platform for Ambient ML applications. The target platform leverages RISC-V and OpenTitan. The Sparrow software includes a home-grown operating system named CantripOS, that runs on top of seL4 and (ignoring the seL4 kernel) is written almost entirely in Rust.
> Archived on Jan 4 2024
Look into Makatea[0], a seL4-based QubesOS-like system.
0. https://trustworthy.systems/projects/makatea/
That doesn't mean any project to do that will have the fate of Hurd. But it is a huge and complicated task.
By setting up an open system on top of a permissions bound system (Unix) having limitations as an user looks really weird and with full of rough edges everywhere, with limited permissions even to mount a hard disk image. Namespaces in Hurd (+ maybe guix) solve that by giving the user lots of freedom to install and share whatever it wants without breaking a system.
TBF, that makes it quite explicit that the problem of Hurd never getting ready was due to the project governance (as in "this is not a goal"). A project that uses Mach could never get big.
[1] https://genode.org/download/sculpt
[2] https://genode.org/about/2020-09-16-sculpt.png
But today, they have native modern webbrowser with native 3d acceleration and native audio.
Genode has gone very far.
0. https://managarm.org/
However, there's a talk[0] from three years ago. I would imagine the architecture has changed since then.
0. https://www.youtube.com/watch?v=BzwpdOpNFpQ
So as I suspected, posix-subsystem is a single process that provides the POSIX support for all other process, so it's a single point of failure: https://docs.managarm.org/handbook/sys-arch/posix/index.html
It's interesting that they have some kind of subsystem to run code in kernel space too, very against typical microkernel thinking for isolation/safety reasons.
thor seems to be an actual "bottleneck".
I'd be really happy if I could easily deploy small self-contained embedded applications using general purpose ARMv8 processors. Like one would do with an infotainment system for a car, which is currently done primarily with QNX.
Like if there was a clear order of usability between Linux and MacOS :) it's more a matter of habits and preferences (and religion maybe for some ^^) than anything else.
But we can say this: there's nothing intuitive about Windows' incomplete transition to the new settings app that still sometimes requires you to jump to the old control panel system; there's nothing intuitive about Linux' 50 desktop environments, each with their own incomplete configuration systems. In any kind of match up, MacOS will win on simplicity and intuitiveness hands down simply because every other option is just much worse.
To an extent, but then the test is seeing how people who have never used any system interact. I maintain the MacOS paradigm is objectively less intuitive than alternatives.
> But we can say this: there's nothing intuitive about Windows' incomplete transition to the new settings app that still sometimes requires you to jump to the old control panel system; there's nothing intuitive about Linux' 50 desktop environments, each with their own incomplete configuration systems
Sure, that's clumsy. Not really relevant though.
> In any kind of match up, MacOS will win on simplicity and intuitiveness hands down simply because every other option is just much worse.
Strongly disagree. MacOS comes in behind Windows for certain, and likely behind a couple of FOSS DEs as well. Windows has issues, but usability isn't one of them.
I understand that use as a general purpose OS by non-technical people is a long ways away, but is there a general/mature guide to porting applications from other OSes? How far away are we from being able to easily deploy things like robotics applications on platforms like RPi? For example:
* GStreamer
* ROS
* OpenCV
* custom-built applications in languages like Rust or Java
Have the performance numbers somewhere been validated?