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

[ayumu]

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

Browsers lean hard on sandboxing for security purposes.

Sandboxes implemented with seL4 have formal guarantees; capabilities are enforced.

Sandboxes implemented on Linux are a joke.

[blahbleh]

If your proofs are instead in tests then it's much easier to modify them, because radical changes aren't required, and the "mathematical proof" is that all branches have been hit.

"all branches have been hit" is nothing mathematical. It means neither fast, nor secure, nor good, nor correct.

[ayumu]

for most people browser is the system. it contains all your passwords, all your credit card numbers etc. and i wasn't even thinking about chromeos

You've conveniently ignored the second half of my post, which was:

These facilities could also be leveraged internally by the browser itself, to better sandbox its own components.

[pal666]

seL4 blazing fast IPC (and it's proven that it's fast)

neither "fast" nor "blazing" is a number. in real world outside of your marketing hype the only fast ipc is no ipc. and in addition to being slow, ipc is complicated. so you only need order of magnitude more manpower than linux

So not only is the kernel safer, it allows to write safer components and isolate security risks while remaining perfomant. And you can run older unadapted code (l4linix) fast and isolated.

you mean, you can run all your non-imaginary code fast and "isolated". guess what? you can do it without microkernels

[pal666]

G E N O D E. Xen. Qubes. QNX. Android. Linux. All of this. is my userspace under a microkernel. How do you eat yours?

it ate your brain. linux is not under microkernel. and if it's under some hypervisor - that hypervisor is useless in kernel role, since it is used in hypervisor role and requires real kernel.

[jp78]

True the kernel is only a part of the stack. But there is a project to write an operating system in Rust on top of of seL4. Also you can write servers in Rust for Genode. With that in theory you can write safer code that a Linux subsystem written in C.
Also you can isolate the unsafe components and thanks to seL4 blazing fast IPC (and it's proven that it's fast) the performance overhead is negligible.
So not only is the kernel safer, it allows to write safer components and isolate security risks while remaining perfomant. And you can run older unadapted code (l4linix) fast and isolated.
I think it's worthwhile.

[Luke_Wolf]

No it isn't.

Someone hasn't read any of the writeups on it. https://www.securityweek.com/bleedin...-click-attacks

First There's this:

The most severe of these flaws is CVE-2020-12351, a heap-based type confusion that affects Linux kernel 4.8 and higher. The issue features a high severity rating (CVSS score of 8.3).

The bug can be exploited by a remote attacker within Bluetooth range of the victim and which knows the bd address of the target device. To trigger the flaw, the attacker would have to send a malicious l2cap packet, which can lead to denial of service or even execution of arbitrary code, with kernel privileges.

you can protect against arbitrary code with kernel privileges but probably not the denial of service.

There's this:

The second issue, CVE-2020-12352, is a stack-based information leak that impacts Linux kernel 3.6 and higher. The bug is considered medium severity (CVSS score of 5.3).

“A remote attacker in short distance knowing the victim's bd address can retrieve kernel stack information containing various pointers that can be used to predict the memory layout and to defeat KASLR. The leak may contain other valuable information such as the encryption keys,” Google’s researchers explain.

Which is an information leak that means that within a microkernel you could still likely read the address space of the bluetooth stack without triggering a segfault. Network stacks such as Bluetooth do contain sensitive information users wouldn't want leaked.

then we have

Tracked as CVE-2020-24490 and considered medium risk (CVSS score of 5.3), the third vulnerability is a heap-based buffer overflow that affects Linux kernel 4.19 and higher.

A remote attacker within short range of a vulnerable device can trigger the flaw through broadcasting extended advertising data. This could lead to denial of service or even arbitrary code execution with kernel privileges.

which again... denial of services aren't stopped by microkernels.

We'll assume for the sake of argument that appropriate memory protections are in place to stop arbitrary code execution in userspace (NX Bit and all that), but the rest of these are still serious and not halted by the memory isolation provided by using a microkernel.

[Luke_Wolf]

If you don't know what a formal proof is, you don't know, but don't go telling others that they got it wrong when you literally have no idea what you're talking about. The concept of "test coverage" doesn't even apply to this, and they aren't even tests. A formal proof is a real tangible thing, unlike a marketing claim of "artificial intelligence"

Luke, go do your homework, you're making an ass of yourself.

You might want to look into a mirror. You're making an ass of yourself trying to decry the fact that I ripped off all the shitty wrapping paper that your marketing speak wrapped up around a nothingburger. I'm the one that actually did do his research and so isn't being taken away by hand waving terms about "mathematical symbols". All your "proof" means is that your program matches your requirements doc to the letter and it has the tests to prove it. That does not mean it's secure, that does not mean it's fast, that does not mean that it is good.

In principle sure you can sit there in the documentation masturbating about your algorithm and using a logic proof to say that the inputs and outputs are "correct" (not fast, not secure, not good, correct) and thus the function is proven... but do you know why nobody does that? Why "Mathematically Proven" in seL4's case and generally in software means "100% code coverage"? Because if your correct output is not fast, secure, or good then you have to change the code and rewrite the proof from scratch. If your proofs are instead in tests then it's much easier to modify them, because radical changes aren't required, and the "mathematical proof" is that all branches have been hit.

[Luke_Wolf]

Great, suggesting other microkernels? Which ones? Are better? Go on ?

Minix, QNX, Singularity, (in the future) Redox... The list can go for quite some time. The L4 kernels are hardly the only entry in the market and they're far from the most interesting or "complete". They were useful to prove that it was just a Mach fuckup that microkernels were considered slow, but at this point their main argument in favour of themselves is mastubatory marketing crap that doesn't actually mean much of anything.

[microcode]

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.

If you don't know what a formal proof is, you don't know, but don't go telling others that they got it wrong when you literally have no idea what you're talking about. The concept of "test coverage" doesn't even apply to this, and they aren't even tests. A formal proof is a real tangible thing, unlike a marketing claim of "artificial intelligence"

Luke, go do your homework, you're making an ass of yourself.