6 ms·

Formal verification doesn't mean your design can't be flawed in other ways that your theorem prover can't identify. See also: Software AES with cache-timing in

Formal verification doesn't mean your design can't be flawed in other ways that your theorem prover can't identify. See also: Software AES with cache-timing information leaks.

AnimalMuppet 10y ago
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...
- CiPHPerCoder 10y ago
  See: https://github.com/w3c/svgwg/issues/266 https://github.com/w3c/svgwg/issues/266
  - nickpsecurity 10y ago
    Well-written report. I agree with the recommendation.
nickpsecurity 10y ago
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/usenixsecurity13/sec13-paper_doychev.pdf https://www.usenix.org/system/files/conference/usenixsecurit... http://www-bcf.usc.edu/~wang626/pubDOC/EldibWS14_TOSEM.pdf 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. :)
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 ago
  The 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 ago
    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 doesn't mean your design can't be flawed in other ways that your theorem prover can't identify. See also: Software AES with cache-timing information leaks.

AnimalMuppet 10y ago

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

CiPHPerCoder 10y ago
See: https://github.com/w3c/svgwg/issues/266 https://github.com/w3c/svgwg/issues/266
- nickpsecurity 10y ago
  Well-written report. I agree with the recommendation.

nickpsecurity 10y ago

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/usenixsecurity13/sec13-paper_doychev.pdf https://www.usenix.org/system/files/conference/usenixsecurit... http://www-bcf.usc.edu/~wang626/pubDOC/EldibWS14_TOSEM.pdf 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. :)

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 ago
The 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 ago
  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!