seL4 Micro-Kernel Working Towards A General-Purpose, Multi-Server OS

[mdedetrich]

Here let me translate that for you:


Doesn't sound so impressive now does it?

While TDD is something we should all strive for, touting it as your main selling point... just isn't that impressive unless you're running a DOD contract writing software to run aircraft engines or something. As others are being quick to point out it doesn't mean jack shit for typical server or desktop usage scenarios.

This has nothing to do with TDD. seL4 is a mathematically formally verified kernel (see https://docs.sel4.systems/projects/s...20is%20correct.). The formal proof for sel4 is written in Isabelle/HOL and iirc some specifications are written in Haskell.

[ayumu]

will it save you from browser vulnerability? will you formally verify your browser?

No, but the capability mechanisms in seL4 would allow the browser to be really well isolated from the rest of the system. These facilities could also be leveraged internally by the browser itself, to better sandbox its own components.

[microcode]

Here let me translate that for you:


Doesn't sound so impressive now does it?

While TDD is something we should all strive for, touting it as your main selling point... just isn't that impressive unless you're running a DOD contract writing software to run aircraft engines or something. As others are being quick to point out it doesn't mean jack shit for typical server or desktop usage scenarios.

No, this is not TDD; this is an actual system of mathematical and symbolic proofs. It is a completely different galaxy of verification.

Something that you get with proofs that you do not get with tests, is a complete picture of what the code could do (assuming the processor is functioning as designed, and your model of it is accurate), not just the subset of what it should/might do that you think of when you're writing tests.

[microcode]

Minix has been used as a desktop OS by hobbyists. It is used in the Intel ME. It has some nice features ( like dead servers restart ). Imho Minix is better positioned to go forward. The big problem is that the community ( especially the opensource one ) sees microkernels as slow. It is a big misconception, but very hard to die.

When it comes to Minix 3, especially when compared to seL4, it's not a misconception. Minix3 has some interesting overall design decisions in user space, but seL4 is by far the better kernel. I'd be down for a port of the Minix3 userspace to seL4 (yes, I am aware this is a lot of work because of the different ideas of just how micro the kernel should be).

[Luke_Wolf]

The advantage of seL4 over other microkernels is that seL4 is formally verified. It has been mathematically proven to meet its specification, including enforcement of security properties. The proof is done both at the C code level and at the object code (compiler output) level. There is no other real-world kernel which has been formally verified.

Here let me translate that for you:

The advantage of seL4 over other microkernels is that seL4 used Test Driven Development to have 100% code coverage for the kernel itself.

Doesn't sound so impressive now does it?

While TDD is something we should all strive for, touting it as your main selling point... just isn't that impressive unless you're running a DOD contract writing software to run aircraft engines or something. As others are being quick to point out it doesn't mean jack shit for typical server or desktop usage scenarios.

[_ReD_]

The big problem is that the community ( especially the opensource one ) sees microkernels as slow. It is a big misconception, but very hard to die.

Well, It's so hard to die, because it's not a misconception.

[billyswong]

Yeah I looked at (part of) the presentation. Skipped most of it since that pdf was a bit heavy on my pdf reader/system. Personally I could not care less if it was mathematically proven - is it proven in practice?! Another thing, as others have already mentioned - what good is a safe kernel when you got vulnerable software running on top of it - or more concerning even vulnerable hardware? does seL4 have mitigations for all those pesky CPU bugs found in recent years? spectre/meltdown/etc ?! or worst of the worst - anything resembling the intel management engine?

Starting from page 23 they are talking of their "Time Protection" research and innovation in seL4. When finished, it should mitigate all kinds of spectre/meltdown vulnerabilities in present and future. But I guess nothing in OS can stop firmware bug/backdoor like Intel ME as they got a higher privilege than the OS you are running and they can spy whatever they like. Hardware DRM is backdoor by design and what we can only hope for is containing them by IOMMU.

P.S. In future I guess multi-user systems such as hypervisors and cloud backends will all implement something similar to what web browsers do lately: no cache sharing across domain.

[Rallos Zek]

The advantage of seL4 over other microkernels is that seL4 is formally verified. It has been mathematically proven to meet its specification, including enforcement of security properties. The proof is done both at the C code level and at the object code (compiler output) level. There is no other real-world kernel which has been formally verified.

That's just the kernel part that has been verified, none of the drivers and glue code which would make it work has had the same testing or verification applied to them.

[horizonbrave]

It'll never be able to compete with a RustOS

[waxhead]

The advantage of seL4 over other microkernels is that seL4 is formally verified. It has been mathematically proven to meet its specification, including enforcement of security properties. The proof is done both at the C code level and at the object code (compiler output) level. There is no other real-world kernel which has been formally verified.

Yeah I looked at (part of) the presentation. Skipped most of it since that pdf was a bit heavy on my pdf reader/system. Personally I could not care less if it was mathematically proven - is it proven in practice?! Another thing, as others have already mentioned - what good is a safe kernel when you got vulnerable software running on top of it - or more concerning even vulnerable hardware? does seL4 have mitigations for all those pesky CPU bugs found in recent years? spectre/meltdown/etc ?! or worst of the worst - anything resembling the intel management engine?