The problem is giant kernels that change constantly. It doesn't have to be that way. Look at L4 and QNX.
With sufficient code bloat, all bugs are deep.
That's an interesting statement. Might have to think on it. While we're on secure kernels, did you ever have any experience with the ASOS system or hear about it from someone who did? It was the only Ada OS aim for A1 class that actually got delivered far as I can tell from papers. Then info disappears into a black hole. Be interesting to find out how well it worked or didn't as putting a modern version of that in a container or on top of seL4 might be worth trying.
Note: MaRTE OS is an Ada-based, open-source RTOS still in development and use. Not security-focused, though. Muen is just a separation kernel. A secure one could draw on them a bit.
As for "with sufficient code bloat, all bugs are deep," that's my answer to Torvalds' "given enough eyeballs, all bugs are shallow". Time has proven him wrong - the number of bugs in the Linux kernel continues to increase as the kernel becomes more bloated. 16 million lines of code and still growing![1]
This is why microkernels are the way to go. Good microkernels run about 10,000 lines of code. It's possible with 10,000 lines of code to have a steadily decreasing number of bugs.
We now have a situation where neither Linux nor Windows is securable. We're paying the price for that.
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.
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.
Is KASLR broken or is TSX broken? Seems to me that TSX is broken, yet again. For example, substituting Rowhammer for TSX and L4 for Linux, you could then say that L4 is broken because of Rowhammer when what's really broken is DRAM.
http://techreport.com/news/26911/errata-prompts-intel-to-dis...
With sufficient code bloat, all bugs are deep.
You might call it bloat, but I'd classify ASLR as Defense in Depth.
Reminds me of[1]:
> Consider this our "I told you so" that we hope you'll remember in the coming years as KASLR is "broken" time and again. Then again, in this offensive-driven industry, that's where the money is, isn't it?
[1] https://forums.grsecurity.net/viewtopic.php?f=7&t=3367&sid=e...