Re: [isabelle] Isabelle Foundation & Certification



Hi Makarius,

Wouldn't it be highly relevant to include HOL Zero in the systems you
consider in your list?

Shouldn't you be considering pretty printing?  In most systems, you can
create all sorts of confusing stuff by exploiting flaws, as we've already
discussed in the past.

And the risk of a trojan horse inference kernel or pretty printer hasn't
been considered.

But then I don't think you were attempting to be complete.

> Makarius:
>> OCaml is much less safe than SML, e.g. strings are
>> mutable
>
> Freek:
> I think the newest OCaml support immutable strings?

Yes OCaml 4.02 does support immutable strings, but it's not yet considered
to fully incorporated into the language proper.  Unless you do something
specific, you're still using mutable strings.

Note that HOL Zero manages to avoid the problem by making copies of strings
at the interface to the kernel.  There are 21 instances of this in the
kernel.

>> Makarius:
>> ints overflow at unspecified word size without
>> any exception,
>
> Freek:
> And if in the kernel you would use nums instead of ints,
> then the second problems would be gone too?  (It would
> be interesting to know how much of a hassle this last
> change would be.  And maybe you only would need to
> go through nums when you actually calculate with ints in
> the kernel? Does this even happen, and if so, in which
> functions?)

HOL Light 'new_basic_type_definition' uses 'length' which returns a possibly
overflowing int.  So if the predicate in the supplied theorem had enough
type variables (2^30 in a 32-bit OS) then the returned theorem would be
wrong.  This is of course almost impossible to do in practice.

Note that HOL Zero avoids the risk entirely by using 'big_int' (which can be
arbitrarily big).  This requires two utilities used in the kernel, that are
implemented in 14 lines of code.

>> Makarius:
>> .. various other oddities and deviations from original ML
>> make it hard to understand mathematically (e.g possibility for
>> circular datatypes).  Signals allow to inject arbitrary ML
>> exceptions into user code, not just interrupts. (I am not taking
>> Obj.magic non-sense into account here, since its absence
>> can be easily detected by looking at the source.)

HOL Zero avoids these risks as far as I know.  But if you could find a way
and demonstrate it, perhaps exploiting exception injection, you could earn
yourself the $100 bounty..  HOL Zero avoids the Obj.magic problem by
overwriting the module.

Note that it's not good enough to grep the source to look for Obj.magic -
you can use obfuscated OCaml code to create an OCaml source code file
containing an Obj.magic, and then read this into the OCaml session.

Mark.




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