3 ms·

It could potentially be proven. We think it's unlikely due to cost or complexity. So, the fields default position was that most things would be low to medium as

It could potentially be proven. We think it's unlikely due to cost or complexity. So, the fields default position was that most things would be low to medium assurance. Only select components would be high assurance. I hope that answers your broader question about adoption of seL4-like techniques for larger systems. Far as past tense, I left high-assurance security when I found out Jesus died for my sins and rose again. Had to learn an entirely new life with a focus on human beings instead of tech. I'm recently considering going back into security since I spend up to 12 hours a day at work anyway (two jobs). I should also note another reason I say past tense. Many people I learned from have died, retired, or switched focuses. The reason for the later is that there's no real market for high-assurance security. Most won't spend the money or make the tradeoffs. So, security-enhancing popular platforms while assuming they'll get hacked (and responding correctly) seemed like a better use of time. I mean, I could probably could all the high-security vendors on my hands...

mmooss 2y ago
Congratuations on your big change, and on your courage. Security can help people, of course; it just depends on who you work for?
- nickpsecurity 2y ago
  Thank you! And, yes, security can help people when your job allows you to do that. I was talking about high-assurance security specifically. That's products built with techniques like B3/A1 or EAL6/EAL7 required. Examples: https://www.aesec.com/classic/DesigningTheGemsosSecurityKernel-OCR-120409-DRAFT.158131458.pdf https://www.aesec.com/classic/DesigningTheGemsosSecurityKern... https://lukemuehlhauser.com/wp-content/uploads/Karger-et-al-A-retrospective-on-the-VAX-VMM-security-kernel.pdf https://lukemuehlhauser.com/wp-content/uploads/Karger-et-al-... https://apps.dtic.mil/sti/pdfs/AD1014758.pdf https://apps.dtic.mil/sti/pdfs/AD1014758.pdf https://ghs.com/products/safety_critical/integrity_178_security.html https://ghs.com/products/safety_critical/integrity_178_secur... The market for this is tiny. NSA once estimated the labor force for developing them was under 200 people worldwide. I know maybe a dozen or so companies even selling such things. Given tough tradeoffs (eg less features), the buyer market is tiny even though development cost is higher. Medium assurance is the best route commercially. That really just means a solid, development process with selective use of assurance-improving techniques. People writing key parts of their code in SPARK Ada or Rust with careful, design reviews is an example. Certain products, like HAProxy or OpenBSD, are coded so well they rarely have problems. Some web frameworks have security baked into them. Using such approaches is the most likely to succeed commercially. Others use architecture or hardware to great advantage, like Hydra Firewall or Secure64's SourceT. The fields last idea for commercial high-assurance was "selfless acts of security" per Bell. He thought, one component or system type at a time, companies with the money should sponsor experts to build exemplars. They get maintained over time at hopefully lower cost. They're designed to be integrated into low-assurance systems to boost them. While using hybrid funding, CompCert, miTLS, and Muen SK are examples of this. I just rarely see this happen. Both companies and FOSS favor ease of development or velocity over assurance of artifacts. The market usually requires integration with insecure systems whose integration itself might be impossible to secure. So, I have no optimism about high assurance but selective improvements are doable.

mmooss 2y ago

Congratuations on your big change, and on your courage. Security can help people, of course; it just depends on who you work for?

nickpsecurity 2y ago
Thank you! And, yes, security can help people when your job allows you to do that. I was talking about high-assurance security specifically. That's products built with techniques like B3/A1 or EAL6/EAL7 required. Examples: https://www.aesec.com/classic/DesigningTheGemsosSecurityKernel-OCR-120409-DRAFT.158131458.pdf https://www.aesec.com/classic/DesigningTheGemsosSecurityKern... https://lukemuehlhauser.com/wp-content/uploads/Karger-et-al-A-retrospective-on-the-VAX-VMM-security-kernel.pdf https://lukemuehlhauser.com/wp-content/uploads/Karger-et-al-... https://apps.dtic.mil/sti/pdfs/AD1014758.pdf https://apps.dtic.mil/sti/pdfs/AD1014758.pdf https://ghs.com/products/safety_critical/integrity_178_security.html https://ghs.com/products/safety_critical/integrity_178_secur... The market for this is tiny. NSA once estimated the labor force for developing them was under 200 people worldwide. I know maybe a dozen or so companies even selling such things. Given tough tradeoffs (eg less features), the buyer market is tiny even though development cost is higher. Medium assurance is the best route commercially. That really just means a solid, development process with selective use of assurance-improving techniques. People writing key parts of their code in SPARK Ada or Rust with careful, design reviews is an example. Certain products, like HAProxy or OpenBSD, are coded so well they rarely have problems. Some web frameworks have security baked into them. Using such approaches is the most likely to succeed commercially. Others use architecture or hardware to great advantage, like Hydra Firewall or Secure64's SourceT. The fields last idea for commercial high-assurance was "selfless acts of security" per Bell. He thought, one component or system type at a time, companies with the money should sponsor experts to build exemplars. They get maintained over time at hopefully lower cost. They're designed to be integrated into low-assurance systems to boost them. While using hybrid funding, CompCert, miTLS, and Muen SK are examples of this. I just rarely see this happen. Both companies and FOSS favor ease of development or velocity over assurance of artifacts. The market usually requires integration with insecure systems whose integration itself might be impossible to secure. So, I have no optimism about high assurance but selective improvements are doable.