seL4 as a kernel is complete, as far as I can tell, but what about the userspace and hardware support? As soon as this formally verified OS boots into a graphical interface and one can get a simple web browser and media player working, it will be pretty much ready for day-to-day use for most users. 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. Will users soon be able to use a completely formally verified OS (kernel, userspace and everything)? Or is that something too far fetched to dream about?
Best wishes, Marc Collin
On 30 Dec 2014, at 9:54 , Marc Hans marc.collin7@gmail.com wrote:
seL4 as a kernel is complete, as far as I can tell, but what about the userspace and hardware support?
Still very much rudimentary.
As soon as this formally verified OS boots into a graphical interface and one can get a simple web browser and media player working, it will be pretty much ready for day-to-day use for most users.
While certainly possible, desktop use is actually not our main focus. Unless you’re happy with something like a Chromebook, it takes a fair bit more. Instead we’re focussing on use in embedded/cyber-physical systems, and maybe servers (but that’s much lower priority).
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.
Will users soon be able to use a completely formally verified OS (kernel, userspace and everything)? Or is that something too far fetched to dream about?
There’s much more to an OS then the microkernel.
Having said that, you don’t need a completely verified userland (or at least not much) to get very strong security/safety guarantees on seL4. The kernel enforces isolation, the only userland components that are part of the isolation story are the basic resource managers. And we’re actively working on verifying those. Plus there’s work on verified systems code (http://ssrg.nicta.com.au/projects/TS/filesystems), synthesised device drivers (http://ssrg.nicta.com.au/projects/TS/drivers/synthesis/) and a complete high-assurance system (http://ssrg.nicta.com.au/projects/TS/SMACCM/).
But it’s actually far from trivial to connect verified userland components with a verified kernel to an overall verification story (http://ssrg.nicta.com.au/projects/TS/overallproof).
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
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
Hi Gernot and Marc - I'm wondering how hard it might really be myself. I have been thinking of a "chrome book" kind of approach. With desktop virtualization, a smart desktop phone would be very useful. We need to examine what is feasible architecturally atop seL4.
Colin - Please check my profile on LinkedIn http://www.linkedin.com/in/fredseigneur. I can't find you on LinkedIn, are you there?
Happy New Year all, Fred Seigneur
On Tue, Dec 30, 2014 at 5:51 AM, Gernot Heiser gernot@nicta.com.au wrote:
On 30 Dec 2014, at 9:54 , Marc Hans marc.collin7@gmail.com wrote:
seL4 as a kernel is complete, as far as I can tell, but what about the userspace and hardware support?
Still very much rudimentary.
As soon as this formally verified OS boots into a graphical interface and one can get a simple web browser and media player working, it will be pretty much ready for day-to-day use for most users.
While certainly possible, desktop use is actually not our main focus. Unless you're happy with something like a Chromebook, it takes a fair bit more. Instead we're focussing on use in embedded/cyber-physical systems, and maybe servers (but that's much lower priority).
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.
Will users soon be able to use a completely formally verified OS (kernel, userspace and everything)? Or is that something too far fetched to dream about?
There's much more to an OS then the microkernel.
Having said that, you don't need a completely verified userland (or at least not much) to get very strong security/safety guarantees on seL4. The kernel enforces isolation, the only userland components that are part of the isolation story are the basic resource managers. And we're actively working on verifying those. Plus there's work on verified systems code ( http://ssrg.nicta.com.au/projects/TS/filesystems), synthesised device drivers (http://ssrg.nicta.com.au/projects/TS/drivers/synthesis/) and a complete high-assurance system ( http://ssrg.nicta.com.au/projects/TS/SMACCM/).
But it's actually far from trivial to connect verified userland components with a verified kernel to an overall verification story ( http://ssrg.nicta.com.au/projects/TS/overallproof).
Gernot
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-
Fred Seigneur -
Gernot Heiser -
Marc Hans -
Martin Decky