Comment by bigfatkitten
3 days ago
> 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.
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).
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.
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.
2 replies →
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-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.
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.
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-que...
5 replies →
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.
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.
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/Pa...
> I mean why does it have to be formally verified.
Because we can and the security advantages are worth it.