3 ms·

In high-assurance, formal methods were one of many used for the system. It was reduced complexity, precisely-specified behavior, likewise for security policy, p

In high-assurance, formal methods were one of many used for the system. It was reduced complexity, precisely-specified behavior, likewise for security policy, proofs the design/code fulfilled it, exhaustive testing, leak analysis, pestering, and ability to recheck all this. That's so hard it was mostly done for only kernels commercially. From there, your real-world use will involve user-level components, protocols with interactions, and so on. Add one thing to the proven TCB and maybe your proof disappears. So, every trusted component has to be rigorously designed. Then, all the interactions for a holistic argument. Most don't do that. For example, seL4 hosting a web browser won't help you if it's a web application. IBOS and a WAF on seL4, all proven, might cover that. Harder argument. Most of these projects never go beyond the kernel or TLS stack or whatever. You can do stuff with that. Look up Nizza Secure Systems Architecture for a paper with many examples. Yet, they usually don't cut it. They're not compatible with popular apps either. So, most people just harden Linux or BSD or Windows.

mmooss 2y ago
> IBOS and a WAF on seL4, all proven If you mean web application firewall, that seems too complex to be proven? With infinite possible inputs, inspecting it would seem to require too much code to prove - unless it merely verifies traffic matches a short whitelist. Why talk about high assurance talked in the past tense? Is the field moribund? (I don't mean to point out a typo, if that's what it is.)
- nickpsecurity 2y ago
  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

> IBOS and a WAF on seL4, all proven If you mean web application firewall, that seems too complex to be proven? With infinite possible inputs, inspecting it would seem to require too much code to prove - unless it merely verifies traffic matches a short whitelist. Why talk about high assurance talked in the past tense? Is the field moribund? (I don't mean to point out a typo, if that's what it is.)

nickpsecurity 2y ago
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.