Re: [isabelle] soundness of Isabelle/HOL



That's right, what I didn't say was that proof checking can address many of
the remaining soundness-related vulnerabilities (and HOL Zero is very much
intended to be used in precisely this way, as a proof checker).  For
example, any concern that the datatype for theorems is being overwritten by
the proof script can be addressed by recording the proof and exporting it to
another system.

But this proof checking can still suffer problems if the system importing
the proof is not suitably trustworthy.  For example, if both systems have a
pretty printer that have the same vulnerability (e.g. not distinguishing
between two overloaded HOL variables), then the problem won't get noticed in
either system.

Mark.

on 30/1/12 2:50 PM, Randy Pollack <rpollack0 at gmail.com> wrote:

> A well known approach to soundness, not discussed here yet, is
> independent checking.
>
> As Larry points out, a user must read and understand the statements of
> theorems s/he wants to believe, and all definitions they hereditarily
> depend on.
>
> Further there must be confidence that whatever form these theorems are
> presented in is correctly captured by a proof tool's internal
> representation (issues of printing/parsing/overloading, etc).
>
> But the actual proofs are no cause to worry, at least in principle, at
> least in a system like Coq or Isabelle that can produce complete,
> independently checkable proof scripts. in some completely unambiguous
> notation.
>
> Randy Pollack
> --
> On Mon, Jan 30, 2012 at 7:59 AM, "Mark" <mark at proof-technologies.com>
wrote:
>> Larry, you rightly point out that there are more important worries for
>> theorem prover users.  But this doesn't mean that soundness-related
>> vulnerabilities should be ignored now.
>>
>> And also, importantly, I would say that theorem proving hasn't yet
reached
>> its potential.  Nowadays formal proof is largely confined to university
>> departments and a handful of reputed specialist companies.  If/when
> theorem
>> proving does become big, commercial realities mean that there will be
>> considerable outsourcing of proofs to contractors.  Undoubtedly
commercial
>> pressures will tempt some contractors to maliciously exploit
>> soundness-related vulnerabilities, and so we should be taking steps now
to
>> address this.  I'm sure there would have been many in 1970s/80s
> pooh-poohing
>> the risk of computer users exploiting security-related vulnerabilities.
>>
>> Mark.
>>
>> on 30/1/12 11:51 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>>
>>> Forgive me if I launch into my usual lecture: I have never seen a piece
> of
>>> work spoilt by soundness bugs in a theorem prover. I have seen many
> pieces
>>> of work spoilt by unrealistic models, incorrect axioms or proofs of
>>> irrelevant properties. Soundness is vital, but (contrary to a widely
held
>>> belief) it doesn't absolve users of the need to know what they are
doing.
>>>
>>> Larry Paulson
>>>
>>> On 30 Jan 2012, at 09:59, Matthias Schmalz wrote:
>>>
>>>> Hi,
>>>>
>>>> Out of curiosity and for my thesis introduction, I have the following
>>> question.
>>>> I am wondering whether there is a theorem prover out there that gives
>>> stronger soundness guarantees than Isabelle/HOL and whether there is
>>> empirical evidence showing that the difference is practically relevant.
>>>> I would also like to know when the last unsoundness bug in Isabelle's
>>> inference core has been observed.
>>>>
>>>> I already know that Isabelle follows the LCF approach and that HOL is
>>> built from a modest number of axioms using conservative extension
> methods.
>>> It is therefore very likely that proofs by Isabelle are correct. I also
>> know
>>> that this soundness guarantee is restricted to the inference core; for
>>> example, nothing prevents users from configuring the parser to parse
>> "False"
>>> as "True" and therefore giving the impression that "False" can be
proved.
>>> (And of course, soundness rests on the assumption that compiler, ML
>>> libraries, operating system, and hardware behave correctly.)
>>>>
>>>> Many thanks in advance,
>>>> Matthias
>>>>
>>>
>>>
>>>
>>>
>>
>>
>
>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.