Re: [isabelle] Sandboxed evaluation of Isabelle theories?



On Tue, 2013-02-12 at 11:42 +0000, Lawrence Paulson wrote:
> Given the combination of an LCF architecture and ML's static scoping
> rules, I don't see what harm could be done by the insertion of
> arbitrary ML code.

"You take the blue pill - the story ends, you wake up in your bed and
believe whatever you want to believe. You take the red pill - you stay
in Wonderland, and I show you how deep the rabbit hole goes."

Arbitrary ML code can hijack any communication between the LCF kernel
and the user, thus creating a perfect illusion of unsoundness even when
the kernel itself is unaffected.

Perhaps more interestingly, arbitrary ML code can spawn external
processes, which can potentially modify the system state (including the
memory of the running Isabelle process) in arbitrary ways.

Anyway, I am guessing that Joachim is more concerned about features
like unrestricted file system or network access than about soundness of
Isabelle.

Best regards,
Tjark






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