> award winning

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.