Comment by EasyMark
2 days 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.
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.