That's what OK Labs did before GD bought them: https://web.archive.org/web/20111130031013/http://www.ok-labs.com/solutions/secure-hypercell-technology https://

That's what OK Labs did before GD bought them: https://web.archive.org/web/20111130031013/http://www.ok-labs.com/solutions/secure-hypercell-technology https://web.archive.org/web/20111130031013/http://www.ok-lab... CompSci folks have been doing it, too. Here's a paper describing the design style: https://os.inf.tu-dresden.de/papers_ps/nizza.pdf https://os.inf.tu-dresden.de/papers_ps/nizza.pdf Genode OS Framework is only one I know building something like this in FOSS. The rest, esp used in phones, were commercial. One might port Android to something like it or seL4 with dynamic, resource management. Rewrite drivers or anything that's moved to kernel mode for performance in safe language or lots of verification tooling thrown at it.