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 mea

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. Also re-implementations of most features from grsecurity have been in the mainline kernel for years. https://gist.github.com/madaidan/2031b844d760683af19e85bda184b623 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.