new | show | ask | jobs Github

RobotToaster 9 hours 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.

▲

AnthonyMouse 9 hours ago | parent | next [-]

I would like to introduce you to Spectre and Rowhammer.

▲

RobotToaster 9 hours ago | parent [-]

Secure software won't protect you from insecure hardware, which also needs to be formally verified for a secure system.

	▲	AnthonyMouse 9 hours ago \| parent [-]
		> 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.

▲

crote 4 hours ago | parent | prev | next [-]

Sure, you formally verified that the software confirms to the specification, but how are you going to prove that the specification is correct?

▲

kelnos 5 hours ago | parent | prev [-]

You'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.