News for hackers. Stuff that matters.

A comment on Hardening attack surfaces with formally proven binary format parsers. Parent comment

Re:Hardening attack surfaces with formally proven binary for... by jnash on Tuesday July 05, 2022 @12:40AM (#31984375)
I don't think you understand what "proven correct" means. If you formally prove a spec correct using modern proof tools then it is guaranteed to have zero bugs. Nobody has found even a single bug in the proven correct CompCert C compiler for example. However people find bugs in gcc all the time.
[ Parent | on HN ]
Re:Hardening attack surfaces with formally proven binary for... by staticassertion on Tuesday July 05, 2022 @01:09AM (#31984543)
It means that a program has been verified against a model, and properties of that model are held true.

What it does not mean is that the program is bug free. That would, of course, violate the halting problem, or its generalization Rice's Theorem - non-trivial programs can not have arbitrary properties proven about them.

There's also Gödel's Incompleteness Theorem, obviously, as well as the fact that a proof is only as good as its model.

[ Parent | on HN ]
Re:Hardening attack surfaces with formally proven binary for... by UncleMeat on Tuesday July 05, 2022 @11:53AM (#31989769)
It wouldn’t break Rice’s Thm to prove it for a particular program. All Rice’s Thm says is that any algorithm must fail on some programs.
[ Parent | on HN ]
Re:Hardening attack surfaces with formally proven binary for... by staticassertion on Tuesday July 05, 2022 @09:27PM (#31995775)
It would if you're talking about arbitrary classes of bugs.
[ Parent | on HN ]
Re:Hardening attack surfaces with formally proven binary for... by UncleMeat on Tuesday July 05, 2022 @09:56PM (#31995929)
Not so. Consider the algorithm that reports "Yes" for all inputs for all program properties. For a large number of programs and properties, this algorithm will report the correct information.
[ Parent | on HN ]
Re:Hardening attack surfaces with formally proven binary for... by mbrodersen on Tuesday July 05, 2022 @09:19PM (#31995728)
Not true for non-Turing complete languages. Which is why all proof tools require a proof of termination. Some do it automatically (essential ruling out Turing complete languages) others require a formal proof of termination by the user.
[ Parent | on HN ]
Re:Hardening attack surfaces with formally proven binary for... by UncleMeat on Tuesday July 05, 2022 @11:52AM (#31989752)
Ages ago my advisor had a paper proving WEP to be correct. Many years later, a serious flaw was discovered.

Even formal verification can be insufficient.

[ Parent | on HN ]
Re:Hardening attack surfaces with formally proven binary for... by mbrodersen on Tuesday July 05, 2022 @09:20PM (#31995734)
Was it a proof by hand or using a formal proof tool? Never trust proofs that aren’t formally verified by a modern proof tool.
[ Parent | on HN ]
Re:Hardening attack surfaces with formally proven binary for... by UncleMeat on Tuesday July 05, 2022 @09:57PM (#31995934)
Formal verification with model checking.
[ Parent | on HN ]
Re:Hardening attack surfaces with formally proven binary for... by mbrodersen on Wednesday July 06, 2022 @08:51PM (#32008742)
That frankly sounds hard to believe. Which proof tool did he use? Link to paper?
[ Parent | on HN ]