= 27d567bc2d48d9f40e9ccc20ea370b15)
Metus comments on [LINK] seL4, secure operating system kernel is being open-sourced - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (9)
Keep in mind, these things are only proven to work as specified. There is no guarantee that the specification itself is secure. Or that there is no side channel attack possible. Or other stuff.
Correct. But what it achieves is a massive compression in the size of the attack surface. In as much as you trust the proof system, you know that the code matches the specification, so the only bugs which can exist are those in the specification itself.