4 ms·

> I have a lot of hope for SeL4, but progress there seems to be slow mostly because the security model has poor ergonomics. seL4 has its place, but that place

> I have a lot of hope for SeL4, but progress there seems to be slow mostly because the security model has poor ergonomics. seL4 has its place, but that place is not as a Linux replacement. Modern general purpose computers (both their hardware, and their userspace ecosystems) have too much unverifiable complexity for a formally verified microkernel to be really worthwhile.

darksaints 2y ago
I agree that SeL4 won't replace Linux anytime soon, but I beg to differ on the benefits of a microkernel, formally verified or not. Any ordinary well-designed microkernel gives you a huge benefit: process isolation of core services and drivers. That means that even in the case of an insecure and unverified driver, you still have reasonable expectations of security. There was an analysis of Linux CVE's a while back and the vast majority of critical Linux CVEs to that date would either be eliminated or mitigated below critical level just by using a basic microkernel architecture (not even a verified microkernel). Only 4% would have remained critical. https://microkerneldude.org/2018/08/23/microkernels-really-do-improve-security/ https://microkerneldude.org/2018/08/23/microkernels-really-d... The benefit of a verified microkernel like SeL4 is merely an incremental one over a basic microkernel like L4, capable of capturing that last 4% and further mitigating others. You get more reliable guarantees regarding process isolation, but architecturally it's not much different from L4. There's a little bit of clunkiness for writing userpace drivers for SeL4 that you wouldn't have for L4. That's what the LionsOS project is aiming to fix.
- zozbot234 2y ago
  Process isolation of drivers is just not very useful when the driver is interfacing with a device that has full access to system memory. Which is the case for many devices today unless you use IOMMU to prevent this.
  - darksaints 2y ago
    The SeL4 microkernel specification assumes the use of a memory management unit, and is required by default. https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que...
    - comex 2y ago
      IOMMU, not regular (CPU) MMU. The FAQ _does_ address this, but it's under "What about DMA?". In short: drivers have to be trusted for now, except that there's experimental support for x86 VT-d (which is a type of IOMMU).
      - vacuity 2y ago
        I've been developing a notion that, in modern times, a microkernel is not the sole root of trust. It is just the most privileged component that glues other essential components. Without it, things fall apart, but we still need quality in the "business logic" components (everything else, from this view). So a user should deploy a trusted microkernel with trusted means of download and whatever opsec, and similarly for other crucial components like drivers. This is all essential trust anyways. The leaps and bounds we've achieved through hardware engineering have the burden that they aren't credible for security. You can use IOMMU, but perhaps I won't. Integrated co-development of hardware and software is ideal, but generally there is an adversarial relationship, and we must reflect that in the software. Trust and security are not yes/no questions. We have to keep pushing boundaries. seL4 is a good start; let's make more from it.
      - darksaints 2y ago
        Ah yes, thanks for the correction.
    - nine_k 2y ago
      Not memory management unit (MMU), but I/O memory access management unit (IOMMU). That is, can a device start a DMA transfer from/to anywhere in the physical RAM? Does this access have to pass through virtual address translation? For stuff like GPUs and even NICs the performance implications can be noticeable.
- vacuity 2y ago
  Your view is not espoused enough. Thank you for this comment. I'm not suggesting we just go and use seL4 myself, but it's a strong foundation that shows we don't have to be so cynical about the potential of microkernels.
yencabulator 2y ago
Oh don't worry, seL4 isn't formally proven on any multicore computer anyway. And the seL4 core architecture is fundamentally "one single big lock" and won't scale at all to modern machines. The intended design is that each core runs its own kernel with no coordination (multikernel a la Barrelfish) -- none of which is implemented. So as far as any computer with >4 cores is concerned, seL4 is not relevant at this time, and if you wish for that to happen your choice is really either funding the seL4 people or getting someone else to make a different microkernel (with hopefully a lot less CAmkES "all the world is C" mess).
- vacuity 2y ago
  Barrelfish! My dream project is developing a multikernel with seL4's focus on assurance. I want to go even further than seL4's minimalism, particularly with regards to the scheduler. I thiiiiink it doesn't have to be bad for performance. But I've not materialized anything and so I am just delusional. And yes, I am thinking of doing it in Rust. For all of Rust's shortcomings, especially for kernel development, I think it has a lot of promise. I also have the already-loves-Rust cognitive bias. Not trying to somehow achieve seL4's massive verification effort. (Will gasp AI faciliate it? Not likely.) I am sad that Barrelfish hasn't gotten more attention. We need more OS research.
  - yencabulator 2y ago
    You didn't mention capabilities, otherwise very much yes. Though I have to say I think I'd vote EROS or Theseus harder than Barrelfish; Barrelfish is "just" a multikernel. All I've materialized is a bunch of notes and bookmarks. Kani et al are very interesting, but can't handle large codebases yet. I'm trying to write Rust in very compartmentalized, sans-IO etc, way to have small libraries that are fuzzable and more amenable to Kani verification.
    - vacuity 2y ago
      Capabilities are implied; seL4 did it (everyone cool does it) and Barrelfish designed their capability system off of seL4's. When I say multikernel, that is the main innovation of Barrelfish to take; the kernel design otherwise is more like seL4 or perhaps EROS. Barrelfish also has some interesting takes on other OS services that I want to use, but that's not kernel design. I assume Theseus is [0]. It requires the whole system to buy in to one language and model, so I consider it untenable for a general-purpose OS. I think they're planning to use WASM to increase flexibility, but eh. > I'm trying to write Rust in very compartmentalized, sans-IO etc, way to have small libraries that are fuzzable and more amenable to Kani verification. Good design even if Kani isn't used in the end. [0] https://www.usenix.org/conference/osdi20/presentation/boos https://www.usenix.org/conference/osdi20/presentation/boos
EasyMark 2y ago
I mean why does it have to be formally verified. Seems to me like the performance tradeoff for microkernels can be worth it to have drivers and other traditional kernel layer code, that don't bring down the system and can just be restarted in case of failures. Probably not something that will work for all hardware, but I would bet the majority would be fine with it.
- kennysoona 2y ago
  > I mean why does it have to be formally verified. Because we can and the security advantages are worth it.
- darksaints 2y ago
  At this point, even an unverified kernel would be a huge step up in terms of security and reliability. And the performance disadvantages of a microkernel are all overblown, if not outright false [1]. Sure, you have to make twice as many syscalls as a monolithic kernel, but you can do it with much better caching behavior, due to the significantly smaller size. The SeL4 kernel is small enough to fit entirely in many modern processors' L2 cache. It's entirely possible (some chip designers have hinted as much), that with enough adoption they could prioritize having dedicated caches for the OS kernel...something that could never be possible with any monolithic kernel. [1] https://trustworthy.systems/publications/theses_public/23/Parker%3Absc.pdf https://trustworthy.systems/publications/theses_public/23/Pa...

darksaints 2y ago

I agree that SeL4 won't replace Linux anytime soon, but I beg to differ on the benefits of a microkernel, formally verified or not. Any ordinary well-designed microkernel gives you a huge benefit: process isolation of core services and drivers. That means that even in the case of an insecure and unverified driver, you still have reasonable expectations of security. There was an analysis of Linux CVE's a while back and the vast majority of critical Linux CVEs to that date would either be eliminated or mitigated below critical level just by using a basic microkernel architecture (not even a verified microkernel). Only 4% would have remained critical. https://microkerneldude.org/2018/08/23/microkernels-really-do-improve-security/ https://microkerneldude.org/2018/08/23/microkernels-really-d... The benefit of a verified microkernel like SeL4 is merely an incremental one over a basic microkernel like L4, capable of capturing that last 4% and further mitigating others. You get more reliable guarantees regarding process isolation, but architecturally it's not much different from L4. There's a little bit of clunkiness for writing userpace drivers for SeL4 that you wouldn't have for L4. That's what the LionsOS project is aiming to fix.

zozbot234 2y ago
Process isolation of drivers is just not very useful when the driver is interfacing with a device that has full access to system memory. Which is the case for many devices today unless you use IOMMU to prevent this.
- darksaints 2y ago
  The SeL4 microkernel specification assumes the use of a memory management unit, and is required by default. https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que...
  - comex 2y ago
    IOMMU, not regular (CPU) MMU. The FAQ _does_ address this, but it's under "What about DMA?". In short: drivers have to be trusted for now, except that there's experimental support for x86 VT-d (which is a type of IOMMU).
    - vacuity 2y ago
      I've been developing a notion that, in modern times, a microkernel is not the sole root of trust. It is just the most privileged component that glues other essential components. Without it, things fall apart, but we still need quality in the "business logic" components (everything else, from this view). So a user should deploy a trusted microkernel with trusted means of download and whatever opsec, and similarly for other crucial components like drivers. This is all essential trust anyways. The leaps and bounds we've achieved through hardware engineering have the burden that they aren't credible for security. You can use IOMMU, but perhaps I won't. Integrated co-development of hardware and software is ideal, but generally there is an adversarial relationship, and we must reflect that in the software. Trust and security are not yes/no questions. We have to keep pushing boundaries. seL4 is a good start; let's make more from it.
    - darksaints 2y ago
      Ah yes, thanks for the correction.
  - nine_k 2y ago
    Not memory management unit (MMU), but I/O memory access management unit (IOMMU). That is, can a device start a DMA transfer from/to anywhere in the physical RAM? Does this access have to pass through virtual address translation? For stuff like GPUs and even NICs the performance implications can be noticeable.
vacuity 2y ago
Your view is not espoused enough. Thank you for this comment. I'm not suggesting we just go and use seL4 myself, but it's a strong foundation that shows we don't have to be so cynical about the potential of microkernels.

yencabulator 2y ago

Oh don't worry, seL4 isn't formally proven on any multicore computer anyway. And the seL4 core architecture is fundamentally "one single big lock" and won't scale at all to modern machines. The intended design is that each core runs its own kernel with no coordination (multikernel a la Barrelfish) -- none of which is implemented. So as far as any computer with >4 cores is concerned, seL4 is not relevant at this time, and if you wish for that to happen your choice is really either funding the seL4 people or getting someone else to make a different microkernel (with hopefully a lot less CAmkES "all the world is C" mess).

vacuity 2y ago
Barrelfish! My dream project is developing a multikernel with seL4's focus on assurance. I want to go even further than seL4's minimalism, particularly with regards to the scheduler. I thiiiiink it doesn't have to be bad for performance. But I've not materialized anything and so I am just delusional. And yes, I am thinking of doing it in Rust. For all of Rust's shortcomings, especially for kernel development, I think it has a lot of promise. I also have the already-loves-Rust cognitive bias. Not trying to somehow achieve seL4's massive verification effort. (Will gasp AI faciliate it? Not likely.) I am sad that Barrelfish hasn't gotten more attention. We need more OS research.
- yencabulator 2y ago
  You didn't mention capabilities, otherwise very much yes. Though I have to say I think I'd vote EROS or Theseus harder than Barrelfish; Barrelfish is "just" a multikernel. All I've materialized is a bunch of notes and bookmarks. Kani et al are very interesting, but can't handle large codebases yet. I'm trying to write Rust in very compartmentalized, sans-IO etc, way to have small libraries that are fuzzable and more amenable to Kani verification.
  - vacuity 2y ago
    Capabilities are implied; seL4 did it (everyone cool does it) and Barrelfish designed their capability system off of seL4's. When I say multikernel, that is the main innovation of Barrelfish to take; the kernel design otherwise is more like seL4 or perhaps EROS. Barrelfish also has some interesting takes on other OS services that I want to use, but that's not kernel design. I assume Theseus is [0]. It requires the whole system to buy in to one language and model, so I consider it untenable for a general-purpose OS. I think they're planning to use WASM to increase flexibility, but eh. > I'm trying to write Rust in very compartmentalized, sans-IO etc, way to have small libraries that are fuzzable and more amenable to Kani verification. Good design even if Kani isn't used in the end. [0] https://www.usenix.org/conference/osdi20/presentation/boos https://www.usenix.org/conference/osdi20/presentation/boos

EasyMark 2y ago

I mean why does it have to be formally verified. Seems to me like the performance tradeoff for microkernels can be worth it to have drivers and other traditional kernel layer code, that don't bring down the system and can just be restarted in case of failures. Probably not something that will work for all hardware, but I would bet the majority would be fine with it.

kennysoona 2y ago
> I mean why does it have to be formally verified. Because we can and the security advantages are worth it.
darksaints 2y ago
At this point, even an unverified kernel would be a huge step up in terms of security and reliability. And the performance disadvantages of a microkernel are all overblown, if not outright false [1]. Sure, you have to make twice as many syscalls as a monolithic kernel, but you can do it with much better caching behavior, due to the significantly smaller size. The SeL4 kernel is small enough to fit entirely in many modern processors' L2 cache. It's entirely possible (some chip designers have hinted as much), that with enough adoption they could prioritize having dedicated caches for the OS kernel...something that could never be possible with any monolithic kernel. [1] https://trustworthy.systems/publications/theses_public/23/Parker%3Absc.pdf https://trustworthy.systems/publications/theses_public/23/Pa...