Re: [isabelle] Sandboxed evaluation of Isabelle theories?



On Wed, 13 Feb 2013, Joachim Breitner wrote:

Does export_code still allow directory traversal and arbitrary file overwriting?

indeed it does; this is one problem.

Maybe export_code should be disabled with -S on, or at least export_code
with an file argument different from "-"...

From browsing the code (which I’m unfortunately not fluent in) it seems
that such safeguards could be added centrally
in ./src/Pure/General/file.ML, e.g. disabling open_output completely if
"-S" (or a stronger flag, say "-S -S") is on.

Another, lesser, problem is that the import statement can access
arbitrary .thy files if the path is known.

This is where Unix chroot (or better) comes into play. It is futile to try isolating file system access of the process in the implementation.

For the funny Secure.set_secure mode, I merely pinned down relatively well-defined things that can extend the code base dynamically.


	Makarius


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