I fear it'll just move the problem one layer up. Sure, you've now proven that the code matches the specification - but how do you ensure the specification is watertight?
I fear it'll just move the problem one layer up. Sure, you've now proven that the code matches the specification - but how do you ensure the specification is watertight?
The specification doesn't have to be.
But yeah, writing specs is usually harder than reviewing the code 4 times :)
It kinda does.
See WPA2 KRACK, you could've had a formally verified WPA2 implementation and it still would've been exploitable because the flaw was the specification itself.
Moving the problem one layer up is the desired outcome because it makes exploitation much more difficult. Your attack surface becomes much smaller.