With Genode, POSIX compatibility is at the point where you can run a webkit2-derived browser natively. There is also 3d acceleration.
If you define security as a "lack of exploitable bugs", then security can never be proven, because it's impossible to prove a negative. Also many formally verified systems have had critical bugs discovered, like the KRACK attacks in WPA. The formal verification wasn't wrong, just incomplete, because modeling complex systems is inherently an intractable problem.
The fact that seL4 doesn't even offer bug bounties should be a huge red flag that this is still very much an academic exercise, and should not be used in places where security actually matters.
I’m not involved in this kind of research or low level auditing, but I have some mathematical training and fascination with the idea of formal verification.
I ran across this thing called “K-Framework” that seems to have invested a lot in making formal semantics approachable (to the extent that’s possible). It’s striving to bridge that gap between academia and practicality, and the creator seems to really “get” both the academic and practical challenges of something like that.
Here’s a brief overview of one of the features that seems most impressive/useful: https://youtu.be/x_xm69gd3fE
The clarity of Grigore’s explanations and the quality of what I’ve found here: https://kframework.org/ makes me think K has a lot of potential, but again, this is not my direct area of expertise, and I haven’t been able to justify a deep dive to judge beyond impressions.
You’re correct in pointing out that complex systems are inevitably difficult to verify, but I think stuff like K could help provably minimize surface area a lot.
It sure makes auditing that code conforms to an expected design a lot easier, which is most security bugs. This is a fantastic design choice for a security focused kernel.
I will grant that proving something was implemented as designed does not rule out design flaws so, fair enough.
In fact, in a seL4 system, most of the vulnerabilities we find on Linux wouldn't even be on the kernel, and their verification logic can't test something that isn't there.
That said, the seL4 model does probably lead to much better security than the Linux one. It's just not as good as the OP's one-liner implies.
Not sure how fair this is, even though I agree with you with regards to Linux being auditable and the others not.
Windows and macOS these days have vendor-provided code signing authorities that can be leveraged (and are by default), which provides at least some protection against malware at the macro level (in that the certificates can be revoked if something nefarious is identified). This doesn't exist at all in Linux, although third party products are in the early stages.
Windows 11 and macOS have hardware-backed root-of-trust. In Windows the root of trust is the TPM, on macOS it's the T2 (Intel) or the chip package (ARM).
Any of these features could be compromised without your knowing, but at least where you have control authorities for these systems you can draw some comfort in knowing that once new malware has been identified spreading on pretty much any machine, it can be stopped quite rapidly on all machines by revocation until the bug can be patched.
The code-signing is relatively trivial to workaround, you just have to get users to run xattr(1) to remove quarantine status.
If you install something like grsecurity or use SELinux policies, I could buy the argument. I have yet to see these used in production though.
Also seL4 is not mathematically proven to be secure, it is formally verified which means it does what it says it does. Part of that spec may include exploitable code
I think we can have the best of both worlds here: OS distributions that are being maintained by paid teams of security experts, and that can be audited by anybody.
What are the major ones? Android, Chromium OS, RedHat (Fedora, CentOS), and SUSE.
I think the reasons are indeed quite good, the security community or industry has a lot of black sheep.
Problem with MS and Apple is that they force intimacy by design. That itself is a security threat to me.
As for Linux, piles of companies pay for Linux kernel security, though many bugs are found by academics and unpaid independent security researchers. Linux is one of the best examples of many-eyes security. None of those brilliant and motivated researchers are allowed to look at the inner workings of MacOS or Windows though Darwin is at least partly open source so I put it way ahead of Windows here.
Also re-implementations of most features from grsecurity have been in the mainline kernel for years. https://gist.github.com/madaidan/2031b844d760683af19e85bda18...
On system-call firewalling tactics like SELinux it is true very few use these in practice as most devs have no idea what a system call is, let alone how to restrict it. That said Kernel namespacing features have come into very wide mainstream use thanks to Docker and similar containerization frameworks which cover much of the scope of things like SELinux while being much easier to use.
As for most Linux /distributions/, I sadly must agree they favor compatibility and ease of use over security basically always. I will grant that Windows/MacOS enable basic sandboxing features that, while proprietary, are likely superior to nothing at all like most Linux distros. Other choices exist though.
QubesOS is the Linux distro for those that want high security. It is what I run on all my workstations and I would trust it out of the box over anything else that exists today as hardware access and application workflows are isolated by virtual machines and the base OS is offline.
QubesOS is a Xen distro that happens to use Fedora by default as dom0 vm.
OpenBSD by contrast has dual auditing and a stellar security reputation, but development is much slower and compatibility is very low.
seL4 as an extreme is a micro-kernel with mathematically provable security by design, but no workstation software runs on it yet.
MacOS, iOS, and Windows are proprietary so they are dramatically worse off than Linux in security out of the gate. No one should use these that desires to maximize freedom, security and privacy.