Re: [isabelle] Clone detection for Isabelle theories
But that needs the language pragma to be present
(at the start of the file)
and I can call ghc (the compiler) with "-XSafe"
and it will reject such code outright.
From the Haskell documentation:
âSafe Haskell, however, does not offer compilation safety. During
compilation time it is possible for arbitrary processes to be
launched, using for example the custom pre-processor flag. This can be
manipulated to either compromise a users system at compilation time,
or to modify the source code just before compilation to try to alter
set Safe Haskell flags.â
Also, I don't recall the details, but I think there were some problems
with Safe Haskell in the past. If you want to be (more) sure, you
probably still have to sandbox compilation and execution on the OS level.
First of all, the ability to write custom tactics in ML is an integral
part of Isabelle. Preventing people from doing that is too immense a
restriction for it to be a useful feature in pretty much any context
except course homework (where writing tactics is usually not done â
although I did in fact do that for one of my homework submissions to
make my life easier).
I wonder why Isabelle plans to abandon
its "safe" flag (as Lars mentioned in
Secondly, if I recall, Isabelle's âsafeâ mode isn't actually very safe.
I don't know what it prevents and what it does not prevent, but even
without the ability to embed arbitrary ML code, you can do all kinds of
nasty things with code generation and the âvalueâ command. Isabelle is a
huge system and as far as I am aware, none of it was ever designed with
a âmaliciousâ user in mind.
I guess if one were to go over the entire code base of Isabelle with the
express intent of finding possible security problems and then ensuring
that all of these are disallowed in the safe mode could result in a
version of Isabelle that provides a reasonable amount of confidence in
its safety, but that would be a big endeavour and the only real use case
would be automatic homework processing.
Considering that you can do the same thing with considerably less
effort, no restrictions imposed on the expressivity of Isabelle, and
with much better confidence in the safety of the approach by using
sandboxes/containers, I don't think there is any reason to invest time
and energy into a âsafe modeâ.
This archive was generated by a fusion of
Pipermail (Mailman edition) and