src/Pure/General/secure.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 22567 1565d476a9e2
child 23922 707639e9497d
permissions -rw-r--r--
tuned signature;
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@20925
    14
  val use: string -> unit
wenzelm@20925
    15
  val commit: unit -> unit
wenzelm@20992
    16
  val execute: string -> string
wenzelm@20992
    17
  val system: string -> int
wenzelm@20925
    18
end;
wenzelm@20925
    19
wenzelm@20925
    20
structure Secure: SECURE =
wenzelm@20925
    21
struct
wenzelm@20925
    22
wenzelm@20992
    23
(** secure flag **)
wenzelm@20925
    24
wenzelm@20925
    25
val secure = ref false;
wenzelm@20925
    26
wenzelm@20977
    27
fun set_secure () = secure := true;
wenzelm@20925
    28
fun is_secure () = ! secure;
wenzelm@20925
    29
wenzelm@22567
    30
fun deny_secure msg = if is_secure () then error msg else ();
wenzelm@20925
    31
wenzelm@20925
    32
wenzelm@20992
    33
(** critical operations **)
wenzelm@20992
    34
wenzelm@20992
    35
(* ML evaluation *)
wenzelm@20925
    36
wenzelm@20925
    37
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
wenzelm@20925
    38
wenzelm@20925
    39
val orig_use_text = use_text;
wenzelm@21770
    40
val orig_use_file = use_file;
wenzelm@20925
    41
wenzelm@22144
    42
fun use_text name pr verbose txt = (secure_mltext (); orig_use_text name pr verbose txt);
wenzelm@21770
    43
fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name);
wenzelm@21770
    44
val use = use_file Output.ml_output true;
wenzelm@20925
    45
wenzelm@20925
    46
(*commit is dynamically bound!*)
wenzelm@22144
    47
fun commit () = orig_use_text "" Output.ml_output false "commit();";
wenzelm@20925
    48
wenzelm@20992
    49
wenzelm@20992
    50
(* shell commands *)
wenzelm@20992
    51
wenzelm@20992
    52
fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
wenzelm@20992
    53
wenzelm@20992
    54
val orig_execute = execute;
wenzelm@20992
    55
val orig_system = system;
wenzelm@20992
    56
wenzelm@20992
    57
fun execute s = (secure_shell (); orig_execute s);
wenzelm@20992
    58
fun system s = (secure_shell (); orig_system s);
wenzelm@20992
    59
wenzelm@20925
    60
end;
wenzelm@20925
    61
wenzelm@21770
    62
val use_text = Secure.use_text;
wenzelm@21770
    63
val use_file = Secure.use_file;
wenzelm@20925
    64
val use = Secure.use;
wenzelm@20992
    65
val execute = Secure.execute;
wenzelm@20992
    66
val system = Secure.system;