3 ms·

Quote: "Galois is a leader in formal verification, a technique that goes beyond testing and evaluation to provide mathematical assurances that a system works on

by lutusp 10y ago

Quote: "Galois is a leader in formal verification, a technique that goes beyond testing and evaluation to provide mathematical assurances that a system works only as intended in all cases." Wait -- mathematical assurances that a system works only as intended in all cases? That's not possible. It pretends that the Turing Halting problem[1] is soluble. Not that this claim is at all uncommon. I regularly see similar claims about software validation, by people who either do not know, or who don't want to acknowledge, that this problem cannot be solved in the general case. 1. https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem : "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist."

ajamesm 10y ago
Real computers are finite state machines, not Turing machines.
- bmm6o 10y ago
  Correct but not relevant. No formal verification technique takes advantage of the fact that the computer has "only" 8 GB or RAM and 1 TB of disk space as its tape (~ 2^2^43 states).
georgeaf99 10y ago
You are correct that creating a program that verifies any other program is mathematically impossible. However, given some critical assumptions regarding the scope of the problem, we can use formal verification techniques to generate proofs for some programs. People in formal verification (https://en.m.wikipedia.org/wiki/Formal_verification https://en.m.wikipedia.org/wiki/Formal_verification) do research to find better ways of creating proofs for programs automatically.
throwaway729 10y ago
Surely you agree that it's possible to prove x>0 is true after executing this program: if(x <= 0) { x := 1; } People have come up with techniques for reasoning about loops and recursion. Not in general, of course, but for some specific property (e.g., x > 0) and some specific loop (e.g., while(x <= 0) x := x + 1) there are techniques for proving that the property holds after the loop. > I regularly see similar claims about software validation Validation and verification are very different things. Verification is "my program meets these formal specs". Validation is "my specs accurately encodes the whole problem". Indeed, there's no way to do validation in a provably correct way. (But, of course, mathematics and statistics can help :-) ). The good news is that a lot of security and other bugs arise even once you have the correct spec. So verification can be useful even if it's impossible to perfectly validate. > by people who either do not know, or who don't want to acknowledge, that this problem cannot be solved in the general case. It's somehow ironic that you invoke the Talking problem since Turing himself -- AFTER having proven the Halting problem -- basically conjectured the creation of formal methods.
deleted 10y ago
[deleted]
shpat 10y ago
This formal verification walkthrough goes through the hows and whys of a recent project with Amazon that may have some answers for you. Obviously a different project but the fundamentals are similar https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ (I work at Galois)
dllthomas 10y ago
> that this problem cannot be solved in the general case. They are not solving it for the general case. They are solving it for many specific cases. Presented with a system, there is no guarantee that this will be possible - there can't be, that's what the Halting Problem says. But there is also no guarantee that it will be impossible for the particular system under consideration - that is not what the Halting Problem says.

by lutusp 10y ago

ajamesm 10y ago

Real computers are finite state machines, not Turing machines.

bmm6o 10y ago
Correct but not relevant. No formal verification technique takes advantage of the fact that the computer has "only" 8 GB or RAM and 1 TB of disk space as its tape (~ 2^2^43 states).

georgeaf99 10y ago

You are correct that creating a program that verifies any other program is mathematically impossible. However, given some critical assumptions regarding the scope of the problem, we can use formal verification techniques to generate proofs for some programs. People in formal verification (https://en.m.wikipedia.org/wiki/Formal_verification https://en.m.wikipedia.org/wiki/Formal_verification) do research to find better ways of creating proofs for programs automatically.

throwaway729 10y ago

Surely you agree that it's possible to prove x>0 is true after executing this program: if(x <= 0) { x := 1; } People have come up with techniques for reasoning about loops and recursion. Not in general, of course, but for some specific property (e.g., x > 0) and some specific loop (e.g., while(x <= 0) x := x + 1) there are techniques for proving that the property holds after the loop. > I regularly see similar claims about software validation Validation and verification are very different things. Verification is "my program meets these formal specs". Validation is "my specs accurately encodes the whole problem". Indeed, there's no way to do validation in a provably correct way. (But, of course, mathematics and statistics can help :-) ). The good news is that a lot of security and other bugs arise even once you have the correct spec. So verification can be useful even if it's impossible to perfectly validate. > by people who either do not know, or who don't want to acknowledge, that this problem cannot be solved in the general case. It's somehow ironic that you invoke the Talking problem since Turing himself -- AFTER having proven the Halting problem -- basically conjectured the creation of formal methods.

deleted 10y ago

[deleted]

shpat 10y ago

This formal verification walkthrough goes through the hows and whys of a recent project with Amazon that may have some answers for you. Obviously a different project but the fundamentals are similar https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ (I work at Galois)

dllthomas 10y ago

> that this problem cannot be solved in the general case. They are not solving it for the general case. They are solving it for many specific cases. Presented with a system, there is no guarantee that this will be possible - there can't be, that's what the Halting Problem says. But there is also no guarantee that it will be impossible for the particular system under consideration - that is not what the Halting Problem says.