Re: [isabelle] Sandboxed evaluation of Isabelle theories?



Hi,

Am Dienstag, den 12.02.2013, 22:47 +0100 schrieb C. Diekmann:
> 2013/2/12 Joachim Breitner <breitner at kit.edu>:
> > 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.

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

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



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