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
This archive was generated by a fusion of
Pipermail (Mailman edition) and