Re: [seL4] Day-to-day usability of seL4

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 wrote:

On 30 Dec 2014, at 9:54 , Marc Hans 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