4 ms·
There are plenty with good security track records, formal specifications, formal proofs of various security properties, and decades of deployments. SCOMP, GEMS
by Veserv 2y ago
There are plenty with good security track records, formal specifications, formal proofs of various security properties, and decades of deployments.
SCOMP, GEMSOS, INTEGRITY-178, seL4.
- ArtixFox 2y agogod seL4 everywhere would be awesome.
- kyleee 2y agoDon’t forget Temple OS
- burnt-resistor 2y ago> Eschew flamebait. Avoid generic tangents. Omit internet tropes. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
- burnt-resistor 2y agoseL4 is far more rigorous that the others. The problem today is a widespread lack of understanding of software engineering approaches and tools for formal verification of source model verification, compiler toolchains, and binaries, and also a lack of diligence and effort in implementing rigorous practices.