True, but the last time I checked (several years ago), the size of the portion of code that is not drivers or kernel modules was still 7 million lines of code, and the average system still has to load a few million more via kernel modules and drivers. That is still a phenomenally large attack surface.
The SeL4 kernel is 10k lines of code. OKL4 is 13k. QNX is ~30k.
SeL4 was not built for multiple CPU cores, it's not going to perform with modern day "high end" hardware and last I looked its formal proofs don't apply to multicore systems.
True, but the last time I checked (several years ago), the size of the portion of code that is not drivers or kernel modules was still 7 million lines of code, and the average system still has to load a few million more via kernel modules and drivers. That is still a phenomenally large attack surface.
The SeL4 kernel is 10k lines of code. OKL4 is 13k. QNX is ~30k.
Can I run Firefox or PostgreSQL with reasonable performance on SeL4, OKL4, or QNX?
Reasonable performance includes GPU acceleration for both rendering and decoding media, right?
2 replies →
SeL4 was not built for multiple CPU cores, it's not going to perform with modern day "high end" hardware and last I looked its formal proofs don't apply to multicore systems.
You've still got combinatorial complexity problem though, because you never know what a specific user is going to load.
Often you do know what a specific user is going to load