Re: [isabelle] lexical matters

on 18/1/11 2:28 PM, Makarius <makarius at> wrote:

> On Tue, 18 Jan 2011, Tjark Weber wrote:
>> ...
>> And a malicious user, by misusing ML in Isabelle theory files, couldn't
>> replace the functions that you would use to inspect internal
>> certificates -- or the entire inference kernel; or even the entire
>> Isabelle process -- with his own implementation?
> Yes, depending how much criminal energy you want to invest.

Like the printer problems I mention, I also see these ML trojan horse issues
as important, easy-to-address and yet problems that have not yet been
addressed.  The ML interpreter should support being able to block
overwriting in some way or other.  E.g. supply the interpreter with a
datatype or a function name that cannot be overwritten.  It isn't exactly
rocket science, and it removes a risk.  I just don't understand why nothing
has been done about this.

> Actually, this my favourite theoretical attack on LCF prover integrity.
> After "The Matrix" it also has a name, see
> We could harden Isabelle/ML against this, since the ML environment is
> under our control.  Since this has no practical relevance, though, it has
> not been done so far.  It is important to keep focused on real problems.

How could this be done?


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