"Not ASOS, no. I worked on KSOS-11"

Darn. Oh well. I'm aware of KSOS as we discussed it before. I appreciated the perspective on it.

"This is why microkernels are the way to go."

I've been thinking more about the alternative where you do monolithic ones decomposed internally like microkernels with medium-assurance techniques for development. Basically done like this without formal proofs:

http://flint.cs.yale.edu/certikos/certikos.html

Might be a better model as CPU's with more-efficient, isolation mechanisms come online. I'm recommending micro and separation kernels with mediated middleware in interim since they're proven to be better than traditional monoliths. The newer style of development might make new monoliths way better than before, though.

You should take a look at some of the rumpkernel/anykernel work in netbsd, or projects like the Linux kernel library (LKL). They rearchitect the kernel to make it more modular.

From what I recall, the Rumpkernels in NetBSD specifically avoided modifying the kernel to instead come up with an easy way to get to (or test) the drivers. I still have Anti's thesis & links saved for when I have time to dig into the concept more. LKL is interesting. A truly modular OS that's monolithic would let you do something like eCos does below under "Configurability:"

http://www.ecoscentric.com/ecos/

Each unnecessary module can be automatically stripped from the system to make the OS specific to your needs. The "Just Enough OS" projects for virtualization were aiming to do similar things with Linux but they kept the kernel that I'm aware. Ideally, you'd be able to select just the API's, drivers, etc you need with the rest being stripped out of the generated source before compile. Similarly for user-land.

Most of those 16 million lines are in drivers though, not the core kernel. (Which if I recall correctly is only about 200k lines. A far cry from 10k, but also a far cry from 16m.)

The question is how much code is inside the kernel protection boundary. All that code can potentially be exploited and can crash the kernel.

I'll add basically anything they can call in any way. That is (a) directly because it's currently in kernel, (b) loaded through some command they shouldn't be able to access, or even (c) some abnormal mode of operation they cause that has more kernel code running than usual. I'll supplant (c) with running obscure, kernel functions that get less attention in security review than the main ones. Quite a few, major vulnerabilities come from those parts people forget about or only used in weird contexts.