You formally verify that your incorrect solution executes without a hitch, but you might just be formally verifying that any user can hit your API and download all your plaintext passwords.
Lots of security bugs are caused by incorrect specs from misunderstanding the problem and a formal verifier can’t fix these. Humans can’t think through every situation either (or the bugs wouldn’t exist) SMS that’s doubly true because NOBODY understands all the interactions of the system as a whole and how changes in the part they understand affect everything else.
I’m not saying formal verification is bad, but it’s not a panacea and I’d wager would only fix a small percentage of existing bugs.
I think this is exactly it though. Instead of targeting the moving target of "correctness", we should be proving the absence of common defects. Proving that secrets CANNOT be downloaded is a very nice example actually:
* Understandable
* Portable across projects, you could imagine something like
from specs import no_stealing_secrets
no_stealing_secrets(secret_table)
* Implicitly proves the absence of RCE, though I suppose
it could allow something truly crazy like an interpreter
that will run any attacker supplied program that can
be proven not to steal the specified secrets
Lots of security bugs are caused by incorrect specs from misunderstanding the problem and a formal verifier can’t fix these. Humans can’t think through every situation either (or the bugs wouldn’t exist) SMS that’s doubly true because NOBODY understands all the interactions of the system as a whole and how changes in the part they understand affect everything else.
I’m not saying formal verification is bad, but it’s not a panacea and I’d wager would only fix a small percentage of existing bugs.