6 ms·

Does the OS that lies on top of this kernel need to be formally verified as well for the security guarantees to hold?

Koshkin 1y ago
In absolute terms, sure. At the practical level, you can find a partial answer in the section 7.2 of the paper.
snvzz 1y 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 1y ago
  Well, 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 1y ago
    An 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
rubenbe 1y ago
No, that's the advantage is that the kernel/processes don't need to be trusted since your kernel guarantees the isolation. So you can have a Linux kernel running next to some high security process with the guarantee that they will be isolated (with the exception of allowed IPC)
nabla9 1y ago
No. But there are limitations. DMA off, only formally verified drivers It's also important to note that se4L multicore kernel is not yet verified.
- snvzz 1y ago
  An IOMMU can help significantly with the driver problem, preventing a properly initialized driver from misbehaving and compromising the system.
  - vacuity 1y ago
    I want the magical IOMMUs that are maturely secure like MMUs are now. For now, I think various efforts in verifying/restricting/generating drivers are far better, although they fall particularly flat for proprietary drivers.
    - snvzz 1y ago
      >I want the magical IOMMUs that are maturely secure like MMUs are now. There's nothing magical about IOMMUs. They weren't invented last week either. Driver and hardware talk to each other using virtual memory instead of physical memory, preventing the scenario where a bug causes DMA to shit all over somebody else's memory. What holds is that systems that run drivers in supervisor mode have not been able to leverage an iommu to its full extent.
      - vacuity 1y ago
        My (admittedly limited) understanding is that IOMMUs still have practical roadblocks to being a solidly established part of the security of the computer. Of course they aren't bad in principle. Perhaps it's just that we aren't willing to eat the performance cost of making them more robust, but then performance is a tortured debate.
        surajrmal 1y ago
        The primary roadblock is cost and complexity. The technology itself is sound and doesn't have major performance problems.

In absolute terms, sure. At the practical level, you can find a partial answer in the section 7.2 of the paper.

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 1y ago
Well, 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 1y ago
  An 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

rubenbe 1y ago

No, that's the advantage is that the kernel/processes don't need to be trusted since your kernel guarantees the isolation. So you can have a Linux kernel running next to some high security process with the guarantee that they will be isolated (with the exception of allowed IPC)

nabla9 1y ago

No. But there are limitations. DMA off, only formally verified drivers It's also important to note that se4L multicore kernel is not yet verified.

snvzz 1y ago
An IOMMU can help significantly with the driver problem, preventing a properly initialized driver from misbehaving and compromising the system.
- vacuity 1y ago
  I want the magical IOMMUs that are maturely secure like MMUs are now. For now, I think various efforts in verifying/restricting/generating drivers are far better, although they fall particularly flat for proprietary drivers.
  - snvzz 1y ago
    >I want the magical IOMMUs that are maturely secure like MMUs are now. There's nothing magical about IOMMUs. They weren't invented last week either. Driver and hardware talk to each other using virtual memory instead of physical memory, preventing the scenario where a bug causes DMA to shit all over somebody else's memory. What holds is that systems that run drivers in supervisor mode have not been able to leverage an iommu to its full extent.
    - vacuity 1y ago
      My (admittedly limited) understanding is that IOMMUs still have practical roadblocks to being a solidly established part of the security of the computer. Of course they aren't bad in principle. Perhaps it's just that we aren't willing to eat the performance cost of making them more robust, but then performance is a tortured debate.
      - surajrmal 1y ago
        The primary roadblock is cost and complexity. The technology itself is sound and doesn't have major performance problems.