Re: How regularly is the GnuPG source code examined?

From: Jon A. Solworth (solworth_at_cs.uic.edu)
Date: 10/14/05


Date: Fri, 14 Oct 2005 07:12:59 -0500
To: David Wagner <daw-usenet@taverner.cs.berkeley.edu>


        Interesting discussion, and I'm certainly not disagreeing
with Vernon or David here. But I think the problem with formal
verification is the term itself---its misleading. The techniques
would be more accurately called "formal assurance".

        (It is not even that "formal verification" is wrong in an ordinary
english [rather than technical vocabulary] sense. There
are two senses of verification: one is truth and the other is evidence
in a legal sense of evidence. Just as it would be misleading to use
the term "proof" in a formal mathematical setting to talk about legal
proof rather than mathematical proof.)

Jon

David Wagner wrote:
> Vernon Schryver wrote:
>
>>It is not merely that full mechanical proofs of correctness have never
>>been demonstrated except for trivial cases, and then only with heroic
>>efforts,
>
>
> Well, I'm not sure this is true -- I think this might be a slight
> overstatement.
>
>
>>verification cannot do more than relate the program
>>to some other specification.
>
>
> Right, I agree, this is a key issue that is often overlooked. First,
> you have to know that your specification is correct (it is the spec
> you wanted). Also, you have to make sure that all the assumptions made
> during verification are valid (e.g., that your CPU correctly implements
> the instruction set; that your compiler correctly compiles the source
> language; and so on).
>
> But, as both you and Brian Gladman have written, formal verification is
> still useful despite these significant limitations.
>
>
>>Competent programmers write with proofs of correctness in mind. Any
>>code that does not have an informal proof of correctness obvious from
>>the source or from comments is dubious. That proof will be as informal
>>as proof of a mathematical statement.
>
>
> Right. This is often a very helpful way to structure your thinking
> about code, even if you never touch a theorem prover or write down the
> argument in any formal way. For instance, loop invariants are a useful
> concept even if the code is never formally verified in any way.
>
>
>>Just as errors will always be found in published proofs, there will
>>always be bugs in code. The tools of various sorts of verification
>>can significantly reduce those errors, but never eliminate them.
>
>
> Right. Significantly reducing the incidence of errors, and eliminating
> certain sources of errors, is useful, but it isn't going to bring us to
> zero defects.
>
> I guess I'm in violent agreement with most everything you say.



Relevant Pages

  • Re: return in loop for ?
    ... there is a single program which can verify itself. ... the Halting Problem is just a sub-set of the verification ... proving formal correctness, since you aren't concerned whether your ...
    (comp.lang.python)
  • Correctness is ALWAYS conditional
    ... Verification is ALWAYS done conditionally ... Correctness is EVEN MORE critical an issue in a combined system. ... The particular product came back flawed, even through the firmware had ... Never mind that the hardware comes out of a stock library. ...
    (comp.object)
  • Re: How regularly is the GnuPG source code examined?
    ... >>Verified code is only code for which the bugs have not yet been found. ... >There might be more to formal verification than you realize. ... It is not merely that full mechanical proofs of correctness have never ... language, such as whatever you verifier accepts as input other than ...
    (sci.crypt)
  • 2nd CFP - Workshop on Invariant Generation (WING 2009), York, UK, 22-23 March, 2009
    ... Program verification has a long research tradition, ... loops or recursions. ... challenges is automated discovery of inductive assertions, ... narrowing/widening techniques, static analysis, polynomial ...
    (comp.specification.z)
  • 1st CFP - Workshop on Invariant Generation (WING 2009), York, UK, 22-23 March, 2009
    ... Program verification has a long research tradition, ... loops or recursions. ... challenges is automated discovery of inductive assertions, ... narrowing/widening techniques, static analysis, polynomial ...
    (comp.specification.z)