3 ms·
The guarantees offered by the kernel cannot be subverted by unprivileged processes running on it. Of course, the kernel is not very useful on its own, thus the
by snvzz 2y ago
The guarantees offered by the kernel cannot be subverted by unprivileged processes running on it.
Of course, the kernel is not very useful on its own, thus the design of drivers, filesystem servers and other services running on top of the kernel is still relevant.
Note that, unlike most other systems (including Linux) which are flawed at a fundamental level, seL4 actually enables the construction of a secure and reliable system.
- marcosdumay 2y agoWell, as long as the hardware underneath it also enables the construction of a secure system. I don't think we have any such option right now.
- snvzz 2y agoAn example of this is timing side channels. Originating in an effort within seL4[0], there's ongoing work[1] in RISC-V to resolve this. 0. https://sel4.systems//Foundation/Summit/2022/slides/d1_11_fence.t_hardware_support_for_preventing_microarchitectural_timing_channels_Nils_Wistoff.pdf https://sel4.systems//Foundation/Summit/2022/slides/d1_11_fe... 1. https://lf-riscv.atlassian.net/browse/RVS-3569 https://lf-riscv.atlassian.net/browse/RVS-3569