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