You must have heard about it before: formally verified microkernels that offer 100% security... Why don't we use such a microkernel in Qubes then? (The difference between a micro-kernel and a type I hypervisor is blurry. Especially in case of a type I hypervisor used for running para-virtualized VMs, such as Xen used in Qubes. So I would call Xen a micro-kernel in this case, although it can also run fully-virtualized VMs, in which case it should be called a hypervisor I think.) Formally verified microkernel, by Joanna Rutkowska

Joanna Rutkowska who is the founder and CEO of Invisible Things Lab (see complete profile)

This article follows the launch of a new open source operating system,Qubes , designed to provide strong security for desktop computing. Based on Xen, Linux and the X Window System.

The system is based on the Xen architecture which allows a strong isolation of virtual machines. The end-user can own multiple virtual machines to run its applications. These virtual machines are lightweight VMs based on Linux. The system is administrated from the Dom0 virtual machine which is by definition a privileged virtual machine, but without network access to prevent remote attacks. And finally, the system uses the VT technology to run in unprivileged virtual machines the network and storage hardware support.

A specific interface allows the user to switch between these virtual machines.

The full Qubes architecture is described in this document Qubes OS Architecture.

This looks like an existing secure Operating system PolyXene, with EAL5 common criteria evaluation and formally verified code, realized by the Bertin Technologies company.