3 ms·

Do any of the actually-bulletproof ones have enough momentum to have any likelihood of one day being widely used? It's sad that so many of them always seem to m

by zellyn 10y ago

Do any of the actually-bulletproof ones have enough momentum to have any likelihood of one day being widely used? It's sad that so many of them always seem to meander into dead-ends, or result in proprietary offshoots aimed at high-assurance environments. :-(

nickpsecurity 10y ago
There always has to be a core group of knowledgeable people either developing or maintaining submissions to them. It's just the nature of the game for highest quality/reliability/security. So far, this has produced almost entirely proprietary or academic solutions with the FOSS ones not receiving nearly the contributions they need. You can't just scratch an itch and improve something that's nearly NSA-proof most of the time. Only FOSS project actively soliciting and sometimes integrating best-of-breed components from high-assurance field is Genode OS framework. They recently went AGPL, though, for non-proprietary license. That's not promising... The others stopped getting any maintenance or their people and/or I.P. get poached into corporate circles.
- zellyn 10y ago
  Man, that makes me sad. I guess Fuchsia might end up being better than nothing. I wish one of the Google/Facebook/Apple/Microsoft/Amazons of the world would take up the flag and commit to a 10- to 20- year project :-)
  - nickpsecurity 10y ago
    It would be really nice given that Schell originally quoted 2 years per system on a verified kernel. The verified ones did always take 1-3 years but just using safe languages on verified kernels could be quicker. Google, Facebook, and Apple have nobody from high-assurance that I'm aware despite their resources. Microsoft Research snagged quite a few but they just build prototypes or tools that most of Microsoft doesn't use. None of the big names care overall that I can tell even though it would help them on certain components. Microsoft at least deployed SLAM intro production for drivers and applied formal verification to parts of Hyper-V. IBM had Paul Karger work with them on a security-enhanced CPU and smartcard OS (Caernarvon) with pieces of both being sold to customers. Otherwise, I don't know of anything happening with big companies and high-assurance tech. Only smartcard vendors seem to do it regularly for specific components in the hardware (esp MPU's) or software (esp JavaCard or MULTOS).

by zellyn 10y ago

nickpsecurity 10y ago

There always has to be a core group of knowledgeable people either developing or maintaining submissions to them. It's just the nature of the game for highest quality/reliability/security. So far, this has produced almost entirely proprietary or academic solutions with the FOSS ones not receiving nearly the contributions they need. You can't just scratch an itch and improve something that's nearly NSA-proof most of the time. Only FOSS project actively soliciting and sometimes integrating best-of-breed components from high-assurance field is Genode OS framework. They recently went AGPL, though, for non-proprietary license. That's not promising... The others stopped getting any maintenance or their people and/or I.P. get poached into corporate circles.

zellyn 10y ago
Man, that makes me sad. I guess Fuchsia might end up being better than nothing. I wish one of the Google/Facebook/Apple/Microsoft/Amazons of the world would take up the flag and commit to a 10- to 20- year project :-)
- nickpsecurity 10y ago
  It would be really nice given that Schell originally quoted 2 years per system on a verified kernel. The verified ones did always take 1-3 years but just using safe languages on verified kernels could be quicker. Google, Facebook, and Apple have nobody from high-assurance that I'm aware despite their resources. Microsoft Research snagged quite a few but they just build prototypes or tools that most of Microsoft doesn't use. None of the big names care overall that I can tell even though it would help them on certain components. Microsoft at least deployed SLAM intro production for drivers and applied formal verification to parts of Hyper-V. IBM had Paul Karger work with them on a security-enhanced CPU and smartcard OS (Caernarvon) with pieces of both being sold to customers. Otherwise, I don't know of anything happening with big companies and high-assurance tech. Only smartcard vendors seem to do it regularly for specific components in the hardware (esp MPU's) or software (esp JavaCard or MULTOS).