4 ms·

Were you involved in a Common Criteria certification at EAL5 or higher? Anything below EAL5 is just paperwork. As stated above, EAL4 is explicitly only intende

by Veserv 3y ago

Were you involved in a Common Criteria certification at EAL5 or higher? Anything below EAL5 is just paperwork. As stated above, EAL4 is explicitly only intended to certify a system protects against casual and inadvertent attacks. Checkbox security is largely sufficient to meet that standard. In contrast, it takes actual effort to certify at EAL5 or higher which is why Microsoft and Apple have consistently failed every time they have attempted to do so. Even EAL5 is just the baby steps and at best only comparable to mid-level security like what Multics achieved in the 80s. You need to target something like the Separation Kernel Protection Profile (SKPP) if you want serious security. That demanded formal specifications, formal proofs of security, and a multi-month NSA penetration test that must fail to find any vulnerabilities. That was the certification process used for the operating system used in the F-22 and F-35, Integrity-178B.

emmelaich 3y ago
And yet afaik no Linux is certified higher than eal4+ and no-one buys them anyway. Efforts are better placed at isolation and hardening of a standard distro.
- Veserv 3y ago
  I have no idea what you are even trying to say. In this thread we are talking about how cybersecurity is broken and how certification requirements have been continuously degraded to allow insecure systems to be deployed in inappropriate contexts. This has removed one of the vital incentives for secure systems, having requirements that actually demand and verify security instead of just caving into vendor incompetence. Saying that people use systems known to have poor security because they are not required to use systems with high security supports my point. It is not even like they were asking for the impossible. High security systems designed and verified to protect against state actors were developed and deployed. Just everybody demanded they be allowed to use cheap garbage because they value their budgets over your security. Incidentally, we also learned from this process that it is basically impossible to retrofit security onto a insecure design. Any system with a insecure design must be thrown out and redesigned from scratch. Numerous attempts over multiple decades and billions of dollars were spent trying to retrofit security onto existing designs and literally every single one of them failed to this day. Attempting to "harden" existing systems to achieve meaningful security is just a fools errand when there are plenty of examples showing you can develop a secure, general purpose base from scratch, and no examples of anybody ever successfully hardening a existing system.
  - alephnerd 3y ago
    > I have no idea what you are even trying to say The person is (correctly) pointing out that Engineering/Technology is only 50% of the cause of a breach. Security breaches are equal part technical issues (eg. Bugs, misconfigurations) and process failures (eg. requiring multiple VPs giving the go-ahead on upgrading your Artifcatory server). Purely technical solutions will not stop breaches. The belief that bug free formally verified code for something as complex as a fully functional OS (not an embedded or RTOS) can be developed and scaled out is unrealistic and wouldn't solve plenty of much easier vectors of attack. I'll let Trail of Bits explain for me (thank goodness they recently published a blogpost about this very topic) [0] [0] - https://blog.trailofbits.com/2024/03/22/why-fuzzing-over-formal-verification/ https://blog.trailofbits.com/2024/03/22/why-fuzzing-over-for...
    - Veserv 3y ago
      I have no idea why you think that explains anything. It is just saying that fuzzing is a inferior substitute for formal methods, but much cheaper and thus a more cost-effective option. That is totally divorced from literally any point I have ever made anywhere. Formal verification is a known mechanism for establishing highly secure systems. It is not the only way. But it is a way that is known to work. A certification process that demands formal verification and practical penetration testing by the NSA is, as far as we know, a highly effective means of identifying a high security system designed to protect against state actors. It may generate false negatives, but it is highly unlikely to generate false positives. In contrast, extrapolation from processes used by systems that are known to be insecure and security procedures that have never once produced systems that can do things like withstand a practical penetration test by the NSA are highly speculative at best. You must not only do them, you must then generate empirical evidence of security against highly sophisticated and well-funded adversaries, such as practical penetration tests by highly competent red teams, before you can determine if your theories are correct. Anybody who has never achieved success against such adversaries has no business dictating forward looking strategy. As to your assertion that a highly secure fully functional OS can not be developed and scaled out. Then you must either believe that it is okay to connect nuclear power plants and medical devices to the internet with insecure systems or that we must not connect and disconnect all safety-critical systems from the internet. We can not have it both ways. We must either solve the problem technologically or socially, the alternative is catastrophe. You can advocate unproven techniques that have failed for everybody who has ever tried them, but I prefer to advocate using techniques that are empirically known to work and building from there up to more security and down to easier implementation.
- alephnerd 3y ago
  > Efforts are better placed at isolation and hardening of a standard distro Amen! I love the work Chainguard is doing to push that philosophy btw. > no-one buys them anyway Well, there is a very niche market for this at a very specific federal agency (not the one you think) but IBM Mainframes and Green Hills are more than enough to meet that market need.
alephnerd 3y ago
EAL5+ becomes very very very niche and hardware driven. EAL5+ only really kicks in for cryptographic systems (think SmartCards and whatnot) or very critical RTOSes developed by Green Hill. The RoI on formal verification just isn't there, and imo detracts from a lot more pressing and basic security concerns that can and need to he resolved. Something like SKPP just doesn't make sense outside of certain niche usecases as you mentioned. Like, you can have a nice formally verified kernel, yet you still need to ingress and egress data. You might retort that you can encrypt, and then I can retort that I can MTIM, ..... The cycle goes on and on and doesn't resolve the core fact - nothing can be 100% secure. And Formal Verification, while a useful tool, cannot solve all security issues. And being friends with several 8200 and similar program alums, trust me when I say formal verification wouldn't solve some of the attacks or vectors they would use. David Micken's article in USENIX about realism in security a couple years ago is a good overview [0] [0] - https://scholar.harvard.edu/files/mickens/files/thisworldofours.pdf https://scholar.harvard.edu/files/mickens/files/thisworldofo...
- Veserv 3y ago
  Okay, so you were not involved in a EAL5 or higher software certification. You did a checkbox-level certification and think that proves the harder certifications are all useless. Sure, if the harder certification was useless then you would have a point. If the Navy SEAL test is easy, bootcamp is easy. That logic does not go the other way. Just because you can pass bootcamp does not mean you can be a Navy SEAL. As to your point about ROI, well duh, we are literally in a post about how cybersecurity is broken because nobody cares about cybersecurity. Of course the ROI is poor if nobody cares. I also never even said that formal verification is a goal. I said that the SKPP is a means of demonstrating a product has serious security as it demands a very stringent process that, as far as we know, is theoretically and empirically verified to protect against highly capable state actors. You could theorize some other means of doing so and then verify those means are effective by empirically testing it against highly capable red teams, but you can not claim those techniques are effective prior to the tests, and the SKPP is a known effective certification mechanism for the level of security needed against state actors. As to the fact that there is more work to be done than just a secure foundation. Again, another duh. But again, should we rely on processes that have failed to produce secure systems for decades, or should be rely on processes that have demonstrably achieved a level of security that most people believe to be impossible. All the high security processes have ever done is succeed at a small scale. That is clearly inferior to the regular processes that continuously fail at immense scale. I mean, everybody knows how to scale and hardly anybody knows how to make things secure, but clearly scaling is the hard part in this equation. And frankly, this is all besides the point. We need highly secure systems at scale or we must disconnect safety-critical systems. Saying that we do not know how to be secure at scale does not mean it is magically okay to be insecure at scale. Engineering is about minimum requirements, you do not get to just muddle through and harm people because you want to do things beyond your capacity.

by Veserv 3y ago

emmelaich 3y ago

And yet afaik no Linux is certified higher than eal4+ and no-one buys them anyway. Efforts are better placed at isolation and hardening of a standard distro.

Veserv 3y ago
I have no idea what you are even trying to say. In this thread we are talking about how cybersecurity is broken and how certification requirements have been continuously degraded to allow insecure systems to be deployed in inappropriate contexts. This has removed one of the vital incentives for secure systems, having requirements that actually demand and verify security instead of just caving into vendor incompetence. Saying that people use systems known to have poor security because they are not required to use systems with high security supports my point. It is not even like they were asking for the impossible. High security systems designed and verified to protect against state actors were developed and deployed. Just everybody demanded they be allowed to use cheap garbage because they value their budgets over your security. Incidentally, we also learned from this process that it is basically impossible to retrofit security onto a insecure design. Any system with a insecure design must be thrown out and redesigned from scratch. Numerous attempts over multiple decades and billions of dollars were spent trying to retrofit security onto existing designs and literally every single one of them failed to this day. Attempting to "harden" existing systems to achieve meaningful security is just a fools errand when there are plenty of examples showing you can develop a secure, general purpose base from scratch, and no examples of anybody ever successfully hardening a existing system.
- alephnerd 3y ago
  > I have no idea what you are even trying to say The person is (correctly) pointing out that Engineering/Technology is only 50% of the cause of a breach. Security breaches are equal part technical issues (eg. Bugs, misconfigurations) and process failures (eg. requiring multiple VPs giving the go-ahead on upgrading your Artifcatory server). Purely technical solutions will not stop breaches. The belief that bug free formally verified code for something as complex as a fully functional OS (not an embedded or RTOS) can be developed and scaled out is unrealistic and wouldn't solve plenty of much easier vectors of attack. I'll let Trail of Bits explain for me (thank goodness they recently published a blogpost about this very topic) [0] [0] - https://blog.trailofbits.com/2024/03/22/why-fuzzing-over-formal-verification/ https://blog.trailofbits.com/2024/03/22/why-fuzzing-over-for...
  - Veserv 3y ago
    I have no idea why you think that explains anything. It is just saying that fuzzing is a inferior substitute for formal methods, but much cheaper and thus a more cost-effective option. That is totally divorced from literally any point I have ever made anywhere. Formal verification is a known mechanism for establishing highly secure systems. It is not the only way. But it is a way that is known to work. A certification process that demands formal verification and practical penetration testing by the NSA is, as far as we know, a highly effective means of identifying a high security system designed to protect against state actors. It may generate false negatives, but it is highly unlikely to generate false positives. In contrast, extrapolation from processes used by systems that are known to be insecure and security procedures that have never once produced systems that can do things like withstand a practical penetration test by the NSA are highly speculative at best. You must not only do them, you must then generate empirical evidence of security against highly sophisticated and well-funded adversaries, such as practical penetration tests by highly competent red teams, before you can determine if your theories are correct. Anybody who has never achieved success against such adversaries has no business dictating forward looking strategy. As to your assertion that a highly secure fully functional OS can not be developed and scaled out. Then you must either believe that it is okay to connect nuclear power plants and medical devices to the internet with insecure systems or that we must not connect and disconnect all safety-critical systems from the internet. We can not have it both ways. We must either solve the problem technologically or socially, the alternative is catastrophe. You can advocate unproven techniques that have failed for everybody who has ever tried them, but I prefer to advocate using techniques that are empirically known to work and building from there up to more security and down to easier implementation.
alephnerd 3y ago
> Efforts are better placed at isolation and hardening of a standard distro Amen! I love the work Chainguard is doing to push that philosophy btw. > no-one buys them anyway Well, there is a very niche market for this at a very specific federal agency (not the one you think) but IBM Mainframes and Green Hills are more than enough to meet that market need.

alephnerd 3y ago

EAL5+ becomes very very very niche and hardware driven. EAL5+ only really kicks in for cryptographic systems (think SmartCards and whatnot) or very critical RTOSes developed by Green Hill. The RoI on formal verification just isn't there, and imo detracts from a lot more pressing and basic security concerns that can and need to he resolved. Something like SKPP just doesn't make sense outside of certain niche usecases as you mentioned. Like, you can have a nice formally verified kernel, yet you still need to ingress and egress data. You might retort that you can encrypt, and then I can retort that I can MTIM, ..... The cycle goes on and on and doesn't resolve the core fact - nothing can be 100% secure. And Formal Verification, while a useful tool, cannot solve all security issues. And being friends with several 8200 and similar program alums, trust me when I say formal verification wouldn't solve some of the attacks or vectors they would use. David Micken's article in USENIX about realism in security a couple years ago is a good overview [0] [0] - https://scholar.harvard.edu/files/mickens/files/thisworldofours.pdf https://scholar.harvard.edu/files/mickens/files/thisworldofo...

Veserv 3y ago
Okay, so you were not involved in a EAL5 or higher software certification. You did a checkbox-level certification and think that proves the harder certifications are all useless. Sure, if the harder certification was useless then you would have a point. If the Navy SEAL test is easy, bootcamp is easy. That logic does not go the other way. Just because you can pass bootcamp does not mean you can be a Navy SEAL. As to your point about ROI, well duh, we are literally in a post about how cybersecurity is broken because nobody cares about cybersecurity. Of course the ROI is poor if nobody cares. I also never even said that formal verification is a goal. I said that the SKPP is a means of demonstrating a product has serious security as it demands a very stringent process that, as far as we know, is theoretically and empirically verified to protect against highly capable state actors. You could theorize some other means of doing so and then verify those means are effective by empirically testing it against highly capable red teams, but you can not claim those techniques are effective prior to the tests, and the SKPP is a known effective certification mechanism for the level of security needed against state actors. As to the fact that there is more work to be done than just a secure foundation. Again, another duh. But again, should we rely on processes that have failed to produce secure systems for decades, or should be rely on processes that have demonstrably achieved a level of security that most people believe to be impossible. All the high security processes have ever done is succeed at a small scale. That is clearly inferior to the regular processes that continuously fail at immense scale. I mean, everybody knows how to scale and hardly anybody knows how to make things secure, but clearly scaling is the hard part in this equation. And frankly, this is all besides the point. We need highly secure systems at scale or we must disconnect safety-critical systems. Saying that we do not know how to be secure at scale does not mean it is magically okay to be insecure at scale. Engineering is about minimum requirements, you do not get to just muddle through and harm people because you want to do things beyond your capacity.