7 ms·
>The problem is that "secure firmware" is a relativistic statement. No it isn't, software formally verified to EAL7 is guaranteed to be secure.
by RobotToaster 7mo ago
>The problem is that "secure firmware" is a relativistic statement.
No it isn't, software formally verified to EAL7 is guaranteed to be secure.
- crote 7mo agoSure, you formally verified that the software confirms to the specification, but how are you going to prove that the specification is correct?
- AnthonyMouse 7mo agoI would like to introduce you to Spectre and Rowhammer.
- RobotToaster 7mo agoSecure software won't protect you from insecure hardware, which also needs to be formally verified for a secure system.
- AnthonyMouse 7mo ago> Secure software won't protect you from insecure hardware Then what's KPTI etc.? > which also needs to be formally verified for a secure system. Now we just need a correct and complete theory of quantum mechanics and to do something about that Heisenberg thing. In general formal proofs tell you if something is true given a stipulated set of assumptions. They don't tell you if one of the stipulated assumptions is wrong or can be caused to be wrong on purpose by doing something nobody had previously known to be possible.
- kelnos 7mo agoYou're being sarcastic, right? The entire concept of "guaranteed to be secure" is a fantasy. Even EAL7 can't guarantee anything. It can only say that the tools used for verification didn't find anything wrong. I'm not saying the tools are garbage, but the tools were made by humans, and humans are fallible.
- rcxdude 7mo agoIt's guaranteed to have more paperwork. Actually secure, maybe.