SeL4 Device Driver Framework 0.4.0
lists.sel4.systems
lists.sel4.systems
>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.
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?
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 Linux to meet and beat the published sDDF performance with little effort. Despite that, I certainly welcome the experiments with novel approaches.
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?
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.
[1] https://opensource.googleblog.com/2022/10/announcing-kataos-...
> 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.
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.
But today, they have native modern webbrowser with native 3d acceleration and native audio.
Genode has gone very far.
However, there's a talk[0] from three years ago. I would imagine the architecture has changed since then.
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.