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

[Luke_Wolf]

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

Hardly, the difference is that seL4 makes a very specific claim that having complete code coverage of testing makes them magically more secure and reliable than other microkernels, when the truth is that the piece of code they have complete coverage on is but a tiny portion of the stack, and so while there are advantages that microkernels provide in terms of security and reliability, seL4 isn't really all that special... and its benefit is meaningless outside of tightly controlled embedded environments where you can certify the entire stack.

But even then that certification basically just means that that software does what the Requirements Docs say it does. If the requirements documents say "Send passwords in clear text" then as long as it does that then it's "proven".

[pal666]

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

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

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

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

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

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

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?

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

[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).