4 ms·

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 ra

by lrvick 4y ago

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.

snvzz 4y ago
>seL4 as an extreme is a micro-kernel with mathematically provable security by design, but no workstation software runs on it yet. With Genode, POSIX compatibility is at the point where you can run a webkit2-derived browser natively. There is also 3d acceleration.
px43 4y ago
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. https://github.com/seL4/seL4/blob/master/SECURITY.md https://github.com/seL4/seL4/blob/master/SECURITY.md
- lrvick 4y ago
  > don't confuse formal verification with security 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.
- didericis 4y ago
  > 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. Here’s a brief overview of one of the features that seems most impressive/useful: https://youtu.be/x_xm69gd3fE https://youtu.be/x_xm69gd3fE The clarity of Grigore’s explanations and the quality of what I’ve found here: https://kframework.org/ 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.
- marcosdumay 4y ago
  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.
highwaylights 4y ago
> 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.
- PaulDavisThe1st 4y ago
  > 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.
  - highwaylights 4y ago
    But, you would need to get users to do that?
- raxxorraxor 4y ago
  I have yet to see this giving security in practice anywhere. I think this is primarily a lock-in mechanism.
fsociety 4y ago
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
- krn 4y ago
  > 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.
- namibj 4y ago
  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).
- raxxorraxor 4y ago
  > The Linux community has a track record of being hostile to the security community - for their own good reasons 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.
- lrvick 4y ago

by lrvick 4y ago

snvzz 4y ago

>seL4 as an extreme is a micro-kernel with mathematically provable security by design, but no workstation software runs on it yet. With Genode, POSIX compatibility is at the point where you can run a webkit2-derived browser natively. There is also 3d acceleration.

px43 4y ago

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. https://github.com/seL4/seL4/blob/master/SECURITY.md https://github.com/seL4/seL4/blob/master/SECURITY.md

lrvick 4y ago
> don't confuse formal verification with security 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.
didericis 4y ago
> 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. Here’s a brief overview of one of the features that seems most impressive/useful: https://youtu.be/x_xm69gd3fE https://youtu.be/x_xm69gd3fE The clarity of Grigore’s explanations and the quality of what I’ve found here: https://kframework.org/ 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.
marcosdumay 4y ago
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.

highwaylights 4y ago

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

PaulDavisThe1st 4y ago
> 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.
- highwaylights 4y ago
  But, you would need to get users to do that?
raxxorraxor 4y ago
I have yet to see this giving security in practice anywhere. I think this is primarily a lock-in mechanism.

fsociety 4y ago

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

krn 4y ago
> 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.
namibj 4y ago
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).
raxxorraxor 4y ago
> The Linux community has a track record of being hostile to the security community - for their own good reasons 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.
lrvick 4y ago