Since this is essentially an anti-bloat and shitty software design thread, I'll go ahead and shill seL4 and Genode again
We need something better than all the Win/Mac/Linux shitware we have now. Software nowadays is unmaintainable and bloated as hell. The answer is a secure microkernel OS with formal verification and a clean codebase with minimalism and isolation in mind.
At this point, pretty much everything can be hacked. Our cars can be hacked (which will become even more serious with the self-driving ones). Everything is connected and sending signals. The IoT is coming.
This wouldn't be such a problem if the software was actually designed properly
It's impossible to truly know how many bugs are in our code, but a general rule of thumb is that for every thousand lines, there are about one to five bugs. That sounds reasonable... until you realize how fucking massive codebases are. The Linux kernel is in the tens of millions now, and Bluetooth alone is hundreds of thousands. As system complexity goes up, the security goes down.
It's not just macroshit. It's Loonix too.
Yeah we could patch stuff, and we do. Oh we certainly do, but with our massive codebases, there are massive amounts of bugs. Eventually a vulnerability comes out, which prompts devs to actually do something about one, so they patch it. Yay, we removed one bug! Except in the process of patching, or in the process of continuing to maintain the program, we just introduced another bug. And the cycle continues...
Sure we could use firewalls, but that doesn't treat the problem at the root. It only mitigates our issues. Actually it barely does that, because our firewalls also run on big vulnerable operating systems with millions of lines of code, often the same ones we use on our normal systems.
And no, the AI and machine learning memes won't help. They're the same shit as firewalls. They run on a broken foundation, and once again don't actually treat the core of what's wrong.
We need an operating system running on a trustworthy kernel, one that isolates processes based on whether they are critical and trusted or not. What is malware? What is malicious activity? A common definition is a program that does something that the user does not know it will do, does not expect, is not documented or specified. Therefore, a trustworthy program is one the conforms exactly to its specification, does things in a timely manner, and ensures that things will be executed securely. We need to think of this the same way we think of network security. There's the ideal of zero trust. We don't allow traffic in unless it is confirmed to be safe. Whitelist instead of Blacklist. In the same way, a system must be considered untrustworthy unless proven otherwise.
Enter, SeL4, the provably secure operating system kernel. This little fucker is only 10k lines of C and ASM. This gives it a really small attack surface and means it can be verified FULLY. Now I know what you're thinking. "Oh but it's a MICROKERNEL! They're so slow they're a failed academic meme just look at muh mach!"
Mach was like four decades ago at this point. Microkernels have progressed a lot since then. In fact, they can be really, really freaking fast.
This one in particular also makes use of capability-based security. It may be small, but it doesn't take shit from anyone. Non-kernel code can only access stuff if it's explicitly allowed. If not, tough luck, CIAniggers.
There can be unprivileged code, but it certainly shouldn't be anywhere near the kernelspace. That's the privileged core of the operating system, and we need to keep it secure.
And to hammer that point home about the developments, see this lovely chart of the microkernel innovations stemming from the original L3 and L4. This stems all the way back from 1993, and has gone in so many interesting directions. From ports to MIPS and Alpha, to inspirations off into Fiasco and Pistacho, the latter of which has variants seen in Apple and Qualcomm products. seL4 is just the latest and greatest in this line.
Sauce code here
github.com/seL4/seL4
An operating system that can utilize seL4 and other microkernels of this type.
genode.org/
A look at its architecture
genode.org/documentation/general-overview/index
Road map. This year they plan to work on making it usable for common use cases.
genode.org/about/road-map
Attached: sel4.png (1164x869, 145.71K)