5 ms·

I feel like this needs some reproducible datapoints and references to be anything more than an unsupported anecdote. In recent times it also requires studying

I feel like this needs some reproducible datapoints and references to be anything more than an unsupported anecdote. In recent times it also requires studying seL4's implementation of modern CPU vulnerability mitigations.

snvzz 3y ago
Note that not only does it have such mitigations, but seL4 has state-of-the-art[0] timing side channel prevention. 0. https://trustworthy.systems/projects/timeprotection/ https://trustworthy.systems/projects/timeprotection/
- arghwhat 3y ago
  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.
  - snvzz 3y ago
    >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? 0. https://github.com/au-ts/ipbench https://github.com/au-ts/ipbench
    - arghwhat 3y ago
      > 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 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.

snvzz 3y ago

Note that not only does it have such mitigations, but seL4 has state-of-the-art[0] timing side channel prevention. 0. https://trustworthy.systems/projects/timeprotection/ https://trustworthy.systems/projects/timeprotection/

arghwhat 3y ago
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.
- snvzz 3y ago
  >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? 0. https://github.com/au-ts/ipbench https://github.com/au-ts/ipbench
  - arghwhat 3y ago
    > 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 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.