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?
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.
Reasonable performance includes GPU acceleration for both rendering and decoding media, right?
2 replies →
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