*To*: "\"Mark\"" <mark at proof-technologies.com>*Subject*: Re: [isabelle] soundness of Isabelle/HOL*From*: Konrad Slind <konrad.slind at gmail.com>*Date*: Mon, 30 Jan 2012 09:43:41 -0600*Cc*: Matthias.Schmalz at inf.ethz.ch, lp15 at cam.ac.uk, rpollack0 at gmail.com, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1327937741607@names.co.uk>*References*: <1327937741607@names.co.uk>

Hi all, Matt Kaufmann and I ran a workshop on topics related to this issue (Trusted Extensions of Interactive Theorem Provers). See http://www.cs.utexas.edu/~kaufmann/itp-trusted-extensions-aug-2010/ for the homepage and http://www.cs.utexas.edu/~kaufmann/itp-trusted-extensions-aug-2010/summary/summary.pdf for a summary of the techniques. Cheers, Konrad. On Mon, Jan 30, 2012 at 9:35 AM, "Mark" <mark at proof-technologies.com> wrote: > 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 >>>>> >>>> >>>> >>>> >>>> >>> >>> >> >> >> >

**References**:**Re: [isabelle] soundness of Isabelle/HOL***From:*"Mark"

- Previous by Date: Re: [isabelle] soundness of Isabelle/HOL
- Next by Date: Re: [isabelle] Fwd: soundness of Isabelle/HOL
- Previous by Thread: Re: [isabelle] soundness of Isabelle/HOL
- Next by Thread: [isabelle] WING 2012: First Call for Papers
- Cl-isabelle-users January 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list