This OS isn't completely hypothetical--what you describe is similar to the design of Singularity OS, a (now-dormant?) project at Microsoft Research. Large parts

This OS isn't completely hypothetical--what you describe is similar to the design of Singularity OS, a (now-dormant?) project at Microsoft Research. Large parts of the OS were written in managed code (related to C#), and programs did require proofs that certain invariants were maintained. As you say, most (all?) code was run in ring 0, with security maintained by software rather than hardware. http://en.wikipedia.org/wiki/Singularity_(operating_system) http://en.wikipedia.org/wiki/Singularity_(operating_system)