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
of Isabelle.

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 server side.

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.


	Makarius





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