Re: [isabelle] Sandboxed evaluation of Isabelle theories?


Am Dienstag, den 12.02.2013, 22:47 +0100 schrieb C. Diekmann:
> 2013/2/12 Joachim Breitner <breitner at>:
> > Hi,
> >
> > 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.
> >
> > exactly. Should -S be sufficient for that?
> Does export_code still allow directory traversal and arbitrary file overwriting?

indeed it does; this is one problem.

Maybe export_code should be disabled with -S on, or at least export_code
with an file argument different from "-"...

From browsing the code (which I’m unfortunately not fluent in) it seems
that such safeguards could be added centrally
in ./src/Pure/General/file.ML, e.g. disabling open_output completely if
"-S" (or a stronger flag, say "-S -S") is on.

Another, lesser, problem is that the import statement can access
arbitrary .thy files if the path is known.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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