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.

Larry Paulson


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.
> 
> 
> 	Makarius
> 






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