Bah, don't conflate 'microkernel' with 'secure'.

For a small system like that, the shining ideal is probably a formally verified single program with no real OS to speak of.

I don't need to - the paper just did that by conflating monolithic kernels with security failures that were avoidable.

That doesn't mean they are the only way to get security.

If you can afford formal verification and application programmers also fluent in hardware level coding, you can probably afford more RAM.

I'd want to see a solid paper comparing the security of the approach you mention to a microkernel+app. Until then we have this.

But agreed, there are other ways, of varying practicality, to achieving security.