Re: [isabelle] Sandboxed evaluation of Isabelle theories?
Isn't this what virtual machines are for?
But a student who injected malicious code in such circumstances would be lucky to avoid expulsion, and I can't see it happening here.
On 12 Feb 2013, at 12:46, Makarius <makarius at sketis.net> wrote:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and