Re: How regularly is the GnuPG source code examined?

From: David Wagner (daw_at_taverner.cs.berkeley.edu)
Date: 10/18/05


Date: Tue, 18 Oct 2005 17:55:31 +0000 (UTC)

Douglas A. Gwyn wrote:
>David Wagner wrote:
>> Douglas A. Gwyn wrote:
>> >in many instances verification is computationally infeasible.
>> Can you give any examples?
>
>As a simple case, suppose the computation depends on the
>solution to a computationally hard problem. Depending on
>the details, verification of correctness could be as hard
>as the hard problem itself, which for a large problem
>size would be computationally infeasible.

This doesn't make any sense to me. There is little or no relation
between the running time of the computation and the ease or difficulty
of verifying that the code meets the spec. Verification that a code
meets its spec does not involve running the code.

Note also that any function in NP may be hard to compute, but the
answer is easy to check at runtime. Thus the running time of computing
an answer is not necessarily related to the running time of checking
at runtime that the answer is correct (which is itself not necessarily
related to the cost of verifying statically that the code is correct).

>There are also "more realistic" situations where the
>operations performed depend on a complex way upon the
>input, so there is no simple model to use in verification.
>Indeed, past a certain point one has to worry whether the
>model itself is correct.

That's a different problem. If verification is to be well-defined,
we have to have some spec. Then there are two tasks: (1) identifying
the spec; (2) proving that the code meets the spec. Which one are
you claiming is computationally infeasible? I say that there is no
evidence that (2) is fundamentally computationally infeasible. As for
(1), I don't believe that (1) is a well-defined problem, so I don't
think it makes sense to talk about its computational feasibility.

>If you're interested in what *can* be done by formal
>verification, check out the Spin model checker (nee Spin
>protocol analyzer) at http://spinroot.com/

Yup, I'm familiar with Spin, thanks.



Relevant Pages

  • Re: How regularly is the GnuPG source code examined?
    ... >>solution to a computationally hard problem. ... > between the running time of the computation and the ease or difficulty ... > meets its spec does not involve running the code. ... If verifying the proof takes too long the "proof" ...
    (sci.crypt)
  • Re: How regularly is the GnuPG source code examined?
    ... >> between the running time of the computation and the ease or difficulty ... Verification that a code ... Validators have to be ... any Turing-complete programming language. ...
    (sci.crypt)
  • Re: How regularly is the GnuPG source code examined?
    ... David Wagner wrote: ... > between the running time of the computation and the ease or difficulty ... > meets its spec does not involve running the code. ... no given deterministic algorithm can prove correctness (e.g. ...
    (sci.crypt)
  • Re: How regularly is the GnuPG source code examined?
    ... >>in many instances verification is computationally infeasible. ... solution to a computationally hard problem. ... verification of correctness could be as hard ... check out the Spin model checker (nee Spin ...
    (sci.crypt)