Look into seL4 and related work.

/