Linux is a security shit show but it is at least publicly auditable, which is a prerequisite to form reasonably confidence in the security of software, or to rapidly correct mistakes found.
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.
In the case of seL4, don't confuse formal verification with security. The code matches the spec, and security properties can be extracted very precisely, but spec might contain oversights/bugs which would allow an attacker to perform unexpected behaviors.
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.
Besides spec bugs, the seL4 treat model is focused on making sure components are kept isolated. They do not deal with most of what we understand as attacks on a workstation at all.
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.
> The formal verification wasn't wrong, just incomplete, because modeling complex systems is inherently an intractable problem.
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.
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.
I find it hard to believe that the Linux codebase being auditable makes Linux more secure by default than MacOS, iOS, and Windows. I doubt it is humanly feasible to fully read and grok the several million LOC running within Linux.
I would, however, trust a default MacOS/iOS/Windows system over a default Linux system. The Linux community has a track record of being hostile to the security community - for their own good reasons. Whereas Apple and Microsoft pay teams to secure their OS by default.
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 regret my poor description of seL4. It has proofs for how it functions, and how code execution is isolated, etc. That is not -every- security issue by any means but reviewing a spec is easier than reviewing code, and a small code footprint that forces things out of the kernel that do not need to be there is a major win. I hope more projects follow their lead.
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.
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.
> I would, however, trust a default MacOS/iOS/Windows system over a default Linux system. The Linux community has a track record of being hostile to the security community - for their own good reasons. Whereas Apple and Microsoft pay teams to secure their OS by default.
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.
seL4 actually makes proofs for some core isolation promises, like realtime-ness and data flow adhering to capabilities (though with neglect of side channels for that aspect, which can be corrected for by also verifying the code that runs on top to not do shady stuff to probe side channels).
> 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.
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.
> 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
The code-signing is relatively trivial to workaround, you just have to get users to run xattr(1) to remove quarantine status.
Because even for FOSS stuff, unless you are an expert on all levels of the stack you will not be able to assert there are some hidden exploits disguides as perfectly safe code.
And if you have to rely on third parties to assert that for you, then you will have to trush their honesty and technical skills to be able to assert such statements.
So there is only hope that all players are experts, don't do any mistakes, keep being honest, and exercise their certification for every new release for all products that make up a standard installation.
It's... complicated. Linux is just the kernel, but good modern OS security requires the kernel, the userspace, and the kernel/userspace boundary to all be hardened a significant amount. This means defense in depth, exploit mitigation, careful security and API boundaries put in place to separate components, etc.
Until pretty recently (~3-4 years) Linux the kernel was actually pretty far behind in most respects versus competitors, including Windows and mac/iOS. I say this as someone who used to write a bunch of exploits as a hobby (mainly for Windows based systems and windows apps). But there's been a big increase in the amount of mitigations going into the kernel these days though. Most of the state of the art stuff was pioneered elsewhere from upstream but Linux does adopt more and more stuff these days.
The userspace story is more of a mixed bag. Like, in reality, mobile platforms are far ahead here because they tend to enforce rigorous sandboxing far beyond the typical access control model in Unix or Windows. This is really important when you're running code under the same user. For example just because you run a browser and SSH as $USER doesn't mean your browser should access your SSH keys! But the unix model isn't very flexible for use cases like this unless you segregate every application into its own user namespace, which can come with other awkward consequences. In something like iOS for example, when an application needs a file and asks the user to pick one, the operating system will actually open a privileged file picker with elevated permissions, which can see all files, then only delegate those files the user selects to the app. Otherwise they simply can't see them. So there is a permission model here, and a delegation of permissions, that requires a significant amount of userspace plumbing. Things like FlatPak are improving the situation here (e.g XDG Portal APIs for file pickers, etc.) Userspace on general desktop platforms is moving very, very slowly here.
If you want my honest opinion as someone who did security work and wrote exploits a lot: pretty much all of the modern systems are fundamentally flawed at the design level. They are composed of millions of lines of unsafe code that is incredibly difficult to audit and fix. Linux, the kernel, might actually be the worst offender in this case because while systems like iOS continue to move things out of the kernel (e.g. the iOS WiFi stack is now in userspace as of iOS 16 and the modem is behind an IOMMU) Linux doesn't really seem to be moving in this direction, and it increases in scope and features rapidly, so you need to be careful what you expose. It might actually be that the Linux kernel is possibly the weakest part of Android security these days for those reasons (just my speculation.) I mean you can basically just throw shit at the system call interface and find crashes, this is not a joke. Windows seems to be middle of the pack in this regard, but they do invest a lot in exploit mitigation and security, in no small part due to the notoriety of Windows insecurity in the XP days. Userspace is improving on all systems, in my experience, but it's a shitload of work to introduce new secure APIs and migrate things to use them, etc.
Mobile platforms, both Android and iOS, are in general significantly further ahead here in terms of "What kind of blast radius can some application have if it is compromised", largely because the userspace was co-designed along with the security model. ChromeOS also qualifies IMO. So just pick your poison, and it's probably a step up over the average today. But they still are comprised using the same fundamental building blocks built on lots of unsafe code and dated APIs and assumptions. So there's an upper limit here on what you can do, I think. But we can still do a lot better even today.
If you want something more open in the mobile sector, then probably the only one I would actually trust is probably GrapheneOS since its author (Daniel Micay) actually knows what he's doing when it comes to security mitigation and secure design. The FOSS world has a big problem IMO where people just think "security" means enabling some compiler flags and here's a dump of the source code, when that's barely the starting point -- and outside of some of the most scrutinized projects in the entire world, I would say FOSS security is often very very bad, and in my experience there's no indication FOSS actually generally improves security outside of those exceptional cases, but people hate hearing it. I suspect Daniel would agree with my assessment most of the fundamentals today are fatally flawed (including Linux) but, it is what it is.
Just for interest sake, is Linux better or worse than MacOS, iOS and Windows at this?