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.”

The headline is what I take issue with. Calling it hacker-proof just because it's formally verified is wrong.

Yeah, 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!

"Formal verification makes your code invulnerable against a very specific (though very powerful) attacker"

It's true but that's a specification problem. The hardware should be in the model since it's in the TCB. The earliest tools used for high-assurance security, like Gypsy Verification Environment, had information-flow analysis for detecting covert channels. Today, we have information flow control, distributed version of it, and hardware versions of non-interference that go to the gates. We're actually past being able to handle that with current tooling if ultra-high-performance is a non-goal.

https://www.usenix.org/system/files/conference/usenixsecurit...

http://www-bcf.usc.edu/~wang626/pubDOC/EldibWS14_TOSEM.pdf

It's analog and RF side channels that's going to screw them. DOD et al did decades of cat and mouse games under that with their TEMPEST activities. Open research just getting started. Just waiting for The Flood. :)

See: Microsoft Outlook deciding that executable attachments were a good idea. The feature worked according to spec (I assume), but wow did that ever open the door to a whole lot of hacking...

See: https://github.com/w3c/svgwg/issues/266

Well-written report. I agree with the recommendation.