Re: [isabelle] Sandboxed evaluation of Isabelle theories?
On Tue, 12 Feb 2013, Joachim Breitner wrote:
Am Dienstag, den 12.02.2013, 13:27 +0100 schrieb Tjark Weber:
Anyway, I am guessing that Joachim is more concerned about features
like unrestricted file system or network access than about soundness
Should -S be sufficient for that?
To some extent, yes. It makes doing bad things harder.
That option was originally motivated by semi-public prover webservices,
notably the Proofweb project from Nijmegen, around 2006/2007. What they
also did of course, was the usual sandboxing of the Unix process on the
It is in principle possible to make this all much more secure, and
restrict ML inside Isar to a precisely specified subset of the language
and its libraries.
This archive was generated by a fusion of
Pipermail (Mailman edition) and