Microkernels and seL4
What’s this about microkernels? Didn’t Linux kill that idea? Not at all! The L4 family of microkernels is widely deployed in applications where the benefits of microkernels are critical: security combined with excellent performance and worst-case execution time.
The family of microkernels featured in the Tanenbaum-Torvalds debate were also, to put it mildly, quite mediocre, especially when it came to IPC performance.
The introduction to the L4 users' manual states the fundamental principle of good micro kernel design:
[T]he main design criterion of the micro-kernel is minimality with respect to security: A service (feature) is to be included in the micro-kernel if and only if it is impossible to provide that service outside the kernel without loss of security. The idea is that once we make things small (and do it well), performance will look after itself.
seL4 is unique in that it is the only kernel ever to have an end-to-end formal, machine-checked proof of implementation correctness and security enforcement. See its brochure for a summary, or the conference paper From L3 to seL4 - what have we learnt in 20 years of L4 microkernels for a more detailed description.
The fundamental features seL4 provides are thread management, scheduling, and inter-process communication (IPC). On top of this, all else comes. It is up to userland to implement device drivers and higher-level operating system functionality such as the POSIX API.
Together with Rust, seL4 can be a powerful weapon in the war to secure the Internet of Things.