Re: [isabelle] Sandboxed evaluation of Isabelle theories?



Dear ML- and Isabelle-programmers,

Am Mittwoch, den 13.02.2013, 10:21 +0100 schrieb Joachim Breitner:
> 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.

would this be a good idea:

$ diff -u file.ML-orig file.ML
--- file.ML-orig	2013-02-13 10:35:41.886000990 +0100
+++ file.ML	2013-02-13 10:43:58.573982673 +0100
@@ -104,7 +104,9 @@
 
 fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
 fun open_input f = with_file TextIO.openIn TextIO.closeIn f o platform_path;
-fun open_output f = with_file TextIO.openOut TextIO.closeOut f o platform_path;
+fun open_output f path = 
+	(Secure.deny_secure "Cannot open file for writing in secure mode.";
+	with_file TextIO.openOut TextIO.closeOut f (platform_path path));
 fun open_append f = with_file TextIO.openAppend TextIO.closeOut f o platform_path;
 
 end;


It seems to work here.

For some reason I don’t see the error message, but rather
        
        Exception trace for exception - ERROR raised in library.ML line 264
        
        End of trace
        
        Exception- Interrupt raised

while using ML {* .. *}, which also causes a call to deny_secure, gives a nice error message.

        *** Cannot evaluate ML source in secure mode
        *** At command "ML" (line 3 of "/tmp/Deduction.thy")
        Exception- TOPLEVEL_ERROR raised
        

Would it be possible to include this or an equivalent feature in a
future Isabelle release, so that there is no risk of forgetting to patch
Isabelle when we upgrade the submission server to a new release?

Thanks,
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.