Formal Verification Creates Hacker-Proof Code

Re:Formal Verification Creates Hacker-Proof Code by CGamesPlay on Friday October 21, 2016 @12:42PM (#12761949)

If there's a bug in the theorem prover and it proves itself, it still has that bug.

[ Parent | on HN ]

Re:Formal Verification Creates Hacker-Proof Code by nabla9 on Friday October 21, 2016 @01:07PM (#12762281)

It would have to be kind of fixed point of bugs (like finding cryptographic hash that equal to the input value). It wold be incredibly unlikely.

[ Parent | on HN ]

Re:Formal Verification Creates Hacker-Proof Code by burke on Friday October 21, 2016 @12:48PM (#12762015)

Yep. Imagine a prover that accepts all statements. It would accept a buggy program, and it would accept itself.

It would obviously help reduce errors but it wouldn't categorically eliminate them.

[ Parent | on HN ]

Re:Formal Verification Creates Hacker-Proof Code by spott on Friday October 21, 2016 @12:46PM (#12761990)

Only if the bug in the prover allows the bug in the prover, which seems unlikely (unless the bug is pretty huge).

[ Parent | on HN ]

Re:Formal Verification Creates Hacker-Proof Code by timjver on Friday October 21, 2016 @12:49PM (#12762039)

"seems unlikely" isn't really cutting it, when we're talking about formal systems.

[ Parent | on HN ]

Re:Formal Verification Creates Hacker-Proof Code by mekaj on Friday October 21, 2016 @09:13PM (#12766383)

Trivial, small example: the bug is the prover accepts all inputs.

[ Parent | on HN ]