Hello folks,
I normally wouldn't expect such a thing, but since NICTA has showed excellence in the past and is so intensively powered, I got my hopes up.
I honestly don’t see us having the resources for this kind of work. However, it would be n excellent community project.
There is actually one project already pursuing this goal: Genode [1] Genode is an general-purpose OS framework (with a GUI and other desktop features already implemented) that can run on top of several microkernels, particularly on top of several microkernels from the L4 family. AFAIK they are currently working adding support for seL4 [2][3]. The user space of Genode is not formally verified, but they authors of Genode focus very much on practical security, too. See the talk by Norman Feske [4]. Just my 2 cents. I don't work on Genode, but on a standalone general-purpose microkernel multiserver OS called HelenOS [5] that also targets desktops. HelenOS is unrelated to seL4 (or L4, for that matter). [1] http://genode.org/ [2] http://genode.org/documentation/articles/sel4_part_1 [3] https://github.com/nfeske/genode/commits/sel4 [4] https://www.youtube.com/watch?v=Nr2h9eigpqA [5] http://www.helenos.org/ Best regards Martin Decky -- ------------------------------------------------------------------ Martin Decky Department of Distributed and Dependable Systems, Faculty of Mathematics and Physics, Charles University in Prague, Czech Republic decky@d3s.mff.cuni.cz martin@decky.cz http://d3s.mff.cuni.cz/~decky/ http://www.decky.cz ------------------------------------------------------------------