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.


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
)
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).

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â.


Cheers,

Manuel






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