A number of comments here cover how one would use something like this to benefit security of real-world systems. After all, it's a building block you have to combine with other things. This was demonstrated by team behind Nizza in the paper below with examples including digital signatures, VPN's, and so on.
The first to get certified to high assurance under recent models and delivered in products was INTEGRITY-178B. Like Nizza, they implemented desktops that virtualized the machine with Windows/Linux partitions side-by-side with native apps directly on separation kernel. Runtimes for Ada and Java subsets let you write critical components without common errors from C. Special middleware applies security policies to interactions between components.
A recent product that's more accessible is the GenodeOS architecture that builds hierarchical, desktop system on top of components like seL4, NOVA, and Nitpicker GUI. They're dual-licensed with open-source available. Work in progress.
It should be noted that seL4 itself is aiming for embedded. Many of the top teams are also focusing on language and spec-level models for verification of holistic properties. The isolation approach isn't enough for the level of correctness they're aiming for. Anyone interested in such work should check out Galois's project or CertiKOS.
https://os.inf.tu-dresden.de/papers_ps/nizza.pdf
The first to get certified to high assurance under recent models and delivered in products was INTEGRITY-178B. Like Nizza, they implemented desktops that virtualized the machine with Windows/Linux partitions side-by-side with native apps directly on separation kernel. Runtimes for Ada and Java subsets let you write critical components without common errors from C. Special middleware applies security policies to interactions between components.
http://www.ghs.com/products/safety_critical/integrity-do-178...
A recent product that's more accessible is the GenodeOS architecture that builds hierarchical, desktop system on top of components like seL4, NOVA, and Nitpicker GUI. They're dual-licensed with open-source available. Work in progress.
https://genode.org/
It should be noted that seL4 itself is aiming for embedded. Many of the top teams are also focusing on language and spec-level models for verification of holistic properties. The isolation approach isn't enough for the level of correctness they're aiming for. Anyone interested in such work should check out Galois's project or CertiKOS.
http://smaccmpilot.org/
http://flint.cs.yale.edu/certikos/mcertikos.html