Day-to-day usability of seL4

newer
simple_default_cap_count doesn't...

Marc Hans

30 Dec 2014 30 Dec '14

9:54 a.m.

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

Show replies by date

Gernot Heiser

30 Dec 30 Dec

9:51 p.m.

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.

Martin Decky

10:34 p.m.

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

Fred Seigneur

31 Dec 31 Dec

3:18 a.m.

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

3642

Age (days ago)

3643

Last active (days ago)

List overview

Download

3 comments

4 participants

participants (4)

Fred Seigneur
Gernot Heiser
Marc Hans
Martin Decky