4 ms·
The practice of formal methods has progressed by acknowledging and accepting those limitations. It now attempts to prove useful properties of your code, rather
by lmkg 10y ago
The practice of formal methods has progressed by acknowledging and accepting those limitations. It now attempts to prove useful properties of your code, rather than stamping it "correct" or "incorrect."
FTA:
“We’re not claiming we’re going to prove an entire system is correct, 100 percent reliable in every bit, down to the circuit level,” Wing said. “That’s ridiculous to make those claims. We are much more clear about what we can and cannot do.”
- CiPHPerCoder 10y agoThe headline is what I take issue with. Calling it hacker-proof just because it's formally verified is wrong.
- thingexplainer 10y ago"Formal verification makes your code invulnerable against a very specific (though very powerful) attacker"
- nickpsecurity 10y agoYeah, they really need to knock that off. Formal verification creates hard-to-hack code is still a decent headline. Or "Researchers using formal verification stopped hackers in their tracks." That's entirely accurate plus can be followed by specifics to understand what context it was true and what contexts it might be true elsewhere. Hacker-proof is just going to hurt branding of formal methods the second a hacker takes out a high-assurance system. Whereas, the formal methods and high-assurance literature written by anyone with sense acknowledges plenty of assumptions that might be targeted plus just human error. Even the people they quote in the article don't say it's hacker-proof!