Re: [isabelle] Sandboxed evaluation of Isabelle theories?



On Tue, 12 Feb 2013, Lawrence Paulson wrote:

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.

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.

The Nijmegen guys also had a course with assignments and solutions managed by the web server.

What they did back then was plain Linux chroot. Current Linux variants probably offer a bit more, similar to classic BSD "jail". Variants of virtualization are also possible, of course. I think that certain "cloud computing" infrastructure works like that.

The question of "LCF prover as secure web service" has many aspects to be explored more seriously. One could easily make a research project out of that, with everybody still speaking about clouds until the next buzzword is emerging.


	Makarius





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