Re: [isabelle] Sandboxed evaluation of Isabelle theories?



On Tue, 12 Feb 2013, Lawrence Paulson wrote:

Given the combination of an LCF architecture and ML's static scoping rules, I don't see what harm could be done by the insertion of arbitrary ML code. In any event, anybody who can master Isabelle's APIs sufficiently to do anything interesting by inserting ML code deserves top marks for your course :-)

That's a cource where top marks are very easy to get:

  ML {* Isabelle_System.bash "echo 666" *}

It is left as an exercise to put something really dangerous into the above shell script.


To tighten up the system a little bit, there is isabelle-process option -S to disallow such gross insecurities.

If one wanted to take that issue very seriously, one could sandbox the ML compiler invocation that is embedded into Isabelle/Isar. The infrastructure is in principle all there, but we don't have concrete applications for that, and nobody paying large sums to make it work and keep it working over time.


	Makarius





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