But that's one of the big promises of micro-kernels: You don't have to have 100% trust in the driver for that gamepad you bought from some unknown company.

What about that WiFi driver with 10,000s of lines of code? Are you absolutely sure there isn't some code in it that accidentally or purposefully leaks the rest of your kernel data structures to the outside world? With drivers in their own isolated address space, you wouldn't have to be.

That was the point behind Singularity OS[1] IIRC. Using managed code which could be verified safe by the OS using static analysis.

Can't find it right now, but I recall reading they implemented a network driver with minimal overhead compared to a traditional OS. While they used message passing, a lot of overhead could be eliminated due to the assumptions of safe code.

[1]: https://en.wikipedia.org/wiki/Singularity_%28operating_syste...

Message passing by itself doesn't have to be slow (you can use the paging subsystem for this purpose), but you are looking at two more context switches per system call.

The kernel will have a lot of "unsafe" (the keyword) code.