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).
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