Originally posted by brouhaha
View Post
Announcement
Collapse
No announcement yet.
seL4 Micro-Kernel Working Towards A General-Purpose, Multi-Server OS
Collapse
X
-
Originally posted by brouhaha View Post
Geez, a bunch of people here seem to think that software reliability is all or nothing, and that having a reliable kernel is useless.
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".
Comment
-
Originally posted by Luke_Wolf View Post
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, go do your homework, you're making an ass of yourself.
- Likes 4
Comment
-
Originally posted by bofh80
Great, suggesting other microkernels? Which ones? Are better? Go on ?
Comment
-
Originally posted by microcode View Post
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.
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.Last edited by Luke_Wolf; 07 February 2021, 09:31 PM.
Comment
-
Originally posted by bofh80
No it isn't.
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.
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.
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.
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.
Comment
-
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.
Comment
-
Originally posted by bofh80G E N O D E. Xen. Qubes. QNX. Android. Linux. All of this. is my userspace under a microkernel. How do you eat yours?Last edited by pal666; 11 February 2021, 04:55 PM.
Comment
-
Originally posted by jp78 View PostseL4 blazing fast IPC (and it's proven that it's fast)
Originally posted by jp78 View PostSo 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.Last edited by pal666; 11 February 2021, 05:09 PM.
Comment
-
Originally posted by pal666 View Postfor 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
These facilities could also be leveraged internally by the browser itself, to better sandbox its own components.
Comment
Comment