src/Pure/General/secure.ML
author wenzelm
Sun Sep 16 14:55:48 2007 +0200 (2007-09-16)
changeset 24600 5877b88f262c
parent 24058 81aafd465662
child 24663 015a8838e656
permissions -rw-r--r--
use_text/file: tune text (cf. ML_Parse.fix_ints);
     1 (*  Title:      Pure/General/secure.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Secure critical operations.
     6 *)
     7 
     8 signature SECURE =
     9 sig
    10   val set_secure: unit -> unit
    11   val is_secure: unit -> bool
    12   val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
    13   val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
    14   val use_noncritical: string -> unit
    15   val use: string -> unit
    16   val commit: unit -> unit
    17   val execute: string -> string
    18   val system: string -> int
    19 end;
    20 
    21 structure Secure: SECURE =
    22 struct
    23 
    24 (** secure flag **)
    25 
    26 val secure = ref false;
    27 
    28 fun set_secure () = secure := true;
    29 fun is_secure () = ! secure;
    30 
    31 fun deny_secure msg = if is_secure () then error msg else ();
    32 
    33 
    34 (** critical operations **)
    35 
    36 (* ML evaluation *)
    37 
    38 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
    39 
    40 fun orig_use_text x = use_text ML_Parse.fix_ints x;
    41 fun orig_use_file x = use_file ML_Parse.fix_ints x;
    42 
    43 fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () =>
    44   (secure_mltext (); orig_use_text name pr verbose txt));
    45 
    46 fun use_file pr verbose name = NAMED_CRITICAL "ML" (fn () =>
    47   (secure_mltext (); orig_use_file pr verbose name));
    48 
    49 fun use name = use_file Output.ml_output true name;
    50 
    51 fun use_noncritical name =
    52   (secure_mltext (); orig_use_file Output.ml_output true name);
    53 
    54 (*commit is dynamically bound!*)
    55 fun commit () = CRITICAL (fn () => orig_use_text "" Output.ml_output false "commit();");
    56 
    57 
    58 (* shell commands *)
    59 
    60 fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
    61 
    62 val orig_execute = execute;
    63 val orig_system = system;
    64 
    65 fun execute s = NAMED_CRITICAL "system" (fn () => (secure_shell (); orig_execute s));
    66 fun system s = NAMED_CRITICAL "system" (fn () => (secure_shell (); orig_system s));
    67 
    68 end;
    69 
    70 (*override previous toplevel bindings!*)
    71 val use_text = Secure.use_text;
    72 val use_file = Secure.use_file;
    73 val use = Secure.use;
    74 val execute = Secure.execute;
    75 val system = Secure.system;