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

[pabloski]

Wasn't Genode OS used with L4?

Yes https://genode.org/documentation/articles/sel4_part_2

Genode has a bunch of kernels under his belt https://genode.org/documentation/platforms/index

[kvuj]

Yes https://genode.org/documentation/articles/sel4_part_2

Genode has a bunch of kernels under his belt https://genode.org/documentation/platforms/index

Looking around, I couln't find if SculptOS (their precompiled binary) was using SeL4 by default under the hood.

If so, I'm definitely trying it! It looks so cool.

[pal666]

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.

btw :

Formal verification (alias proof of correctness) has been found to be as error-prone as software construction itself, and for that and other reasons it is unlikely to be that silver bullet (Glass 2002).

[Luke_Wolf]

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.

Congratulations on being scooped up by marketing. No It's literally just as I said. Oh boy you have 100% code coverage on your tests which means you were following TDD. "Mathematically Proven" is as much a bullshit term as "Artificial Intelligence". It is only suitable for annoying actual developers.

[Luke_Wolf]

Formal verification (alias proof of correctness) has been found to be as error-prone as software construction itself, and for that and other reasons it is unlikely to be that silver bullet (Glass 2002).

Come to think of it... when was the last time there was actually a significant Linux kernel exploit rather than a hardware exploit or a userspace exploit?

[kvuj]

Come to think of it... when was the last time there was actually a significant Linux kernel exploit rather than a hardware exploit or a userspace exploit?

Bleeding tooth?

I love what Linux stands for (user freedom / open source), but I would gladly accept a smaller & more secure kernel if there weren't too many compromises.

[Luke_Wolf]

Bleeding tooth?

I love what Linux stands for (user freedom / open source), but I would gladly accept a smaller & more secure kernel if there weren't too many compromises.

I guess? But that's a driver bug that seL4 having complete test coverage wouldn't have protected against either. Microkernel architecture in general could potentially stop the privilege escalation (you actually need certain hardware guarantees around memory access) but it wouldn't stop the underlying security flaw.

[Luke_Wolf]

Yes it would. It's not a security flaw if all you have is a crashed driver. duh.

Ah yes because it's not as if a Network Protocol Stack contains information that would potentially be bad to have leaked or anything, which is what Bleeding Tooth is as much about.

[brouhaha]

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.

Geez, a bunch of people here seem to think that software reliability is all or nothing, and that having a reliable kernel is useless.

[pal666]

I love what Linux stands for (user freedom / open source), but I would gladly accept a smaller & more secure kernel if there weren't too many compromises.

smaller kernel comes with smaller(read: non-existent) userspace