*To*: <Matthias.Schmalz at inf.ethz.ch>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] soundness of Isabelle/HOL*From*: "Mark" <mark at proof-technologies.com>*Date*: Mon, 30 Jan 2012 12:39:24 +0000*Reply-to*: "Mark" <mark at proof-technologies.com>

I would summarise the potential soundness-related vulnerabilities of LCF-style systems as follows: 1. Small risk that the inference kernel still has problems with the design/implementation of its logic. This might include: - a) errors in tricky term operations such as substitution (most or perhaps every HOL system has had problems with this at some stage); - b) errors in the inference rules or axiom/definition commands (this risk is amplified if the kernel implements various derivable inference rules as primitives). 2. Vulnerabilities in the implementation of the LCF-style architecture. This might include: - a) backdoors to creating theorems, thus sidestepping the logic (e.g. by importing theorems from disk purely as statements without proof); - b) not keeping track of theory (e.g. not maintaining a list of the definitions of each constant in the theory, thus making it difficult to review definitions and what has been assumed); - c) ability to overwrite crucial ML values and/or abstract datatypes (such as the list of axioms or the datatype for theorems); - d) vulnerability from aspects of the implementation language (e.g. OCaml's mutable strings, OCaml's Obj.magic) . 3. Problems associated with the pretty printer (and arguably the parser) fooling the user about what has been proved. This might include: - a) ambiguously displaying theorems (such as not annotating theorems with their types, or not distinguishing between overloaded entities). This has become know recently as Pollack Inconsistency; - b) vulnerability to having the pretty printer overwritten or extended in a problematic way. My HOL Zero system addresses most of these vulnerabilities, although there is little that can be done about some of the 2c), 2d) and 3b) vulnerabilities if an ML toplevel is allowed. It is implemented in OCaml, but does manage to avoid the mutable strings problem. I will be porting it to SML sometime soon hopefully, which is a fundamentally more secure language. I give out $100 bounty rewards for anyone uncovering new unsoundness-related vulnerabilities. The website includes a list of all soundness-related vulnerabilities that have been uncovered (even those found by myself). See the HOL Zero page at: http://www.proof-technologies.com/holzero.html The inference kernels of most other LCF-style systems are actually a bit complex, involving a few thousand lines of ML. As of 2012, the risks of vulnerability 1 are probably quite small because they get used so much, but there have been some unsoundnesses uncovered in the 1990s, and I would very much like developers to clearly publish all discovered soundness-related vulnerabilities in their systems. HOL Light manages to keep the inference kernel down to about 500 lines (depending on exactly how you count the lines) by various measures, including: not implementing derivable inference rules in the kernel (other than TRANS) and having a monolithic theory instead of maintaining a theory hierarchy. John Harrison has proved the consistency of the HOL Light kernel, but this just addresses vulnerability 1. Indeed I can prove false without leaving a trace in the HOL Light state in about 5 lines of ML! I'm fairly sure that alll existing HOL systems (other than HOL Zero) still have various known vulnerabilities in their pretty printer, although some have been addressed. Mark Adams. on 30/1/12 10:00 AM, Matthias Schmalz <Matthias.Schmalz at inf.ethz.ch> 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

- Previous by Date: Re: [isabelle] graph theory in isabelle - nominal?
- Next by Date: Re: [isabelle] soundness of Isabelle/HOL
- Previous by Thread: Re: [isabelle] soundness of Isabelle/HOL
- Next by Thread: Re: [isabelle] soundness of Isabelle/HOL
- 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