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