Friday, May 28 2010, 09:41
Qubes OS and formally verified microkernel
Qubes is an open source operating system designed to provide strong security for desktop computing. Qubes is based on Xen, X Window System, and Linux, and can run most Linux applications and utilize most of the Linux drivers. In the future it might also run Windows apps.
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.