Re: [isabelle] lexical matters
on 18/1/11 2:28 PM, Makarius <makarius at sketis.net> 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