Re: [isabelle] soundness of Isabelle/HOL
On Mon, 30 Jan 2012, "Mark" wrote:
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
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:
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.
Before everything is repeated, see also the following thread from Jan
IIRC, the thread also contains some explanations why your points 2c), 2d)
and 3b) concerning the "ML toplevel" are merely an accidental feature of
your implementation that follows the classic Cambridge HOL paradigm. The
Isabelle/ML toplevel is integrated with the prover differently -- it would
easily allow to amend these issues if they were of practical relevance,
but there are more imporant things to do.
This archive was generated by a fusion of
Pipermail (Mailman edition) and