Re: [isabelle] lexical matters



On Tue, 18 Jan 2011, Tjark Weber wrote:

On Tue, 2011-01-18 at 11:23 +0100, Makarius wrote:
On Tue, 18 Jan 2011, Tjark Weber wrote:
As long as you assume a non-malicious user who wants to create a valid
machine-checked proof, it is not much of an issue.

This does not sound like you are speaking here about Isabelle at all. We
do not assume a "non-malicious" user.  You can always inspect internal
certificates, even before embarking on full proof terms.

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.

Actually, this my favourite theoretical attack on LCF prover integrity. After "The Matrix" it also has a name, see http://en.wikipedia.org/wiki/Blue_Pill_%28malware%29

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.


	Makarius





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