Lessons Learned from 30 Years of MINIX

Could you clarify? That comes off as arguing against a whole model of preventing problems because an implementation of that model might have a bug. I'll add that separation kernels, strongest of this approach, were usually between 4-12Kloc with EAL6-7 verification activities performed. Two have endured years of pentesting as well. Far as MMU, there are a number of verified HW systems with several verified for security through mathematical analysis, full testing, and pentesting. Those include Rockwell Collins AAMP7G and some smart card MPU's. So, we do shift goal posts as follows:

Goal post 1 (Linus): Hundreds of sys calls. Hundreds of thousands to millions of lines of code with full read-write access to memory. Buggy drivers included. Explicity and implicit communications plus loops throughout. Unsafe language used throughout.

Goal post 2 (opponents): Handful of sys calls for fundamental abstractions. Tens of thousands of lines worst case preferrably a few thousand w/ full access to memory. Rest isolated in own memory. All communication goes through IPC or shared memory segments explicitly marked w/ kernel calls (and analyzable). Prefer safer language (eg Ada/SPARK) plus verification for kernel or trusted partitions w/ some avaiable in proprietary and FOSS.

There's a world of difference between the two goals. Linus's has been proven ridiculous in two ways: attempts by high-assurance security to secure UNIX previously discovering fundamental obstacles; the results of Linux's development processes in terms of bugs found, severity of their impact, availability loss during defects, and plentiful covert channels. Interestingly, that's the same stuff found in early attempts. One can't prevent such problem in small UNIX but will in obese Linux? Unlikely.

The other goal is supported by theory and practice. In the theory, you can only understand a system if you make it modular, localize the effects of components much as possible, analyze interactions of those components, and add in failure modes. Each of these is supported empirically with some of it even done by Linus. Otherwise, you run into both combinatorial explosion in analysis and systems' version of Butterfly effect in error propagation. Separation kernels are one, but not only, method that sticks with theory through and through while eliminating two whole classes of severe errors: kernel-mode failures in obsese software & drivers; unintended communication of logically, distinct partitions. Experience supports them as field evidence, CompSci pentesting, and NSA pentesting all showed their techniques to dramatically reduce risk as such that they didn't experience problem monolithic OS's and hypervisors did.

So, Linus is defying literally decades of experimental activity in CompSci and high-security field without citing anythign to back it up. He does this even while his own work fails to do better in reliability or security. He is, as we say in the business, talking out his ass.

"A lot of exploits rely on the userland, I suppose, and at that point the observed complexity would be increased for a microkernel system, too."

This much is true. Microkernels are one technique among many to break down and manage complexity then enforce that at some HW level on popular, insecure-by-design CPU's. Only so much one can do without unbearable performance loss. Other CPU's designed for security let one try more things, even monoliths. Thing is, one still has to layer and modularize the system with careful attention to resource sharing and interfaces. What microkernels do. ;) Dijkstra's THE was first attempt at these techniques with design and results described in p16 of this link:

http://brinch-hansen.net/papers/2001b.pdf

"But I digress, actually I'm one of the commentators Tanenbaum mentions. "

You have a talent for making vague references. He mentioned all kinds of claims, esp negative, that people made. Which ones did you make? And did anything I wrote so far help to address it? I can be more specific on whatever topic with references hopefully.

"I don't know if the systems should be isomorph in the end and it's just the development process, or if speed is inversely proportional to complexity, as speed is always the other measure next to correctness."

You're the third person in a few days to essentially wonder about that in front of me or ask me how I'd do it in a high assurance product. I've been piecing together a high-level view of a few new models in parallel. Maybe I need to focus on that more since my secure ASIC research is mostly done. From what I've learned, it's more about the logical design, breakdown, interactions, mapping to real hardware, and any information/energy flows. So, designing secure, reliable, or maintainable systems is necessarily a holistic process split between development and implementation mechanisms. Trick is finding just right set of techniques in each spot to maximize benefit.

I'm actually done with microkernels outside insecure CPU's like Intel as high-security research taught us to focus on hardware-software combos as software-only model is a fundamentally bad idea. I'm looking at tagged, capability, control-flow, crypto-protected, and language-oriented methods. Incidentally, the first machine that hit most goals we want used a combo of good architecture, safer language for OS, CPU designed for it (eg enforces bounds-checks), and HW redundancy. We know what works because systems like Burroughs B5000 already did it in the 1960's. ;) SAFE project (crash-safe.org) follows that lineage plus adds mechanisms for arbitrary security policies at CPU and compiler levels with functional programming for trusted components.

In such work, you may find the answer to your question. Or new, better questions to ask. :)