Capability-based OSes have been around for some time, largely developed by the team that produced DRoPS, Fiasco, and other L4 based systems (as tonyhb pointed out).<p>Those advances are mostly from the Dresden OS folks, and the NICTA group (which went on to make one of Qualcomm's best kernels, OKL4).<p>seL4 was an attempt to convert the API and specification for the L4 kernel into an executable format (using Haskell) and confirm the specification was solid. The system was then extended to actually test the L4 kernel itself.<p>In the most recent versions, you can run entire device drivers and OS layers under the capability management system. One only needs to look at the Genode tooling (which is the logical continuation of the work started in DRoPS): <a href="http://genode.org/documentation/general-overview/index" rel="nofollow">http://genode.org/documentation/general-overview/index</a><p>Genode, Fiasco.OC, L4 (including seL4), and the work on secure GUIs all deserve to be far more popular than they are.