Re: [isabelle] Clone detection for Isabelle theories



>> ... Isar is very much like Perl.
> 
> Great! Use this for advertising.
> Should open up a whole new population of users ...

This was on purpose ;-)

> User-defined syntax is perhaps
> more a matter of readability
> (I guess it's mostly about operator precedences,
> and a few special forms - unless you actively abuse it).
> But code injection really scares me.

I think your mental model of Isabelle is slightly off. There's no point
in discussing the design decisions made decades ago when we're really
discussing how clone detection works with the system we have right now.

To rephrase: Isabelle has arbitrary user-extensible syntax and it has
arbitrary executable ML code. If you want to do realistic syntax
analysis today you have to accept that.

I'm not saying that in the future there couldn't be some other
mechanism. But it is what it is right now.

> I wonder why Isabelle plans to abandon
> its "safe" flag (as Lars mentioned in
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00034.html
> )

There are no plans to abandon it. It has already been abandoned.

But the reasoning goes as follows: Many people understand many different
things about what "secure mode" is supposed to mean. The fact that it
won't run custom ML code means neither that

a) malicious users are prevented from tricking the system into accepting
theorems which are not actually proven (e.g. by using axiomatization)

b) malicious users are prevented from affecting the operating system or
the machine running Isabelle

But it means that many legitimate things (e.g. custom tactics, loading
AFP libraries which contain ML code) are impossible.

Because of that it wasn't really useful to begin with. Having a "secure"
flag which doesn't actually protect anything is worse than having no
flag at all.

Again, in the future, there could be different mechanisms. But before
doing so we actually need to come up with a solid threat model and a
specification on what "secure" should mean.

Cheers
Lars




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