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 <[email protected]> wrote: > On 30 Dec 2014, at 9:54 , Marc Hans <[email protected]> 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 > [email protected] > https://sel4.systems/lists/listinfo/devel >
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
