src/Pure/General/secure.ML
author wenzelm
Sun, 21 Jan 2007 16:43:42 +0100
changeset 22144 c33450acd873
parent 21770 ea6f846d8c4b
child 22567 1565d476a9e2
permissions -rw-r--r--
use_text: added name argument;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/secure.ML
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
     4
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
     5
Secure critical operations.
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
     6
*)
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
     7
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
     8
signature SECURE =
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
     9
sig
20977
dbf1eca9b34e tuned signature;
wenzelm
parents: 20925
diff changeset
    10
  val set_secure: unit -> unit
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    11
  val is_secure: unit -> bool
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    12
  val deny_secure: string -> unit
22144
c33450acd873 use_text: added name argument;
wenzelm
parents: 21770
diff changeset
    13
  val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
21770
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    14
  val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    15
  val use: string -> unit
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    16
  val commit: unit -> unit
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    17
  val execute: string -> string
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    18
  val system: string -> int
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    19
end;
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    20
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    21
structure Secure: SECURE =
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    22
struct
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    23
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    24
(** secure flag **)
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    25
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    26
val secure = ref false;
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    27
20977
dbf1eca9b34e tuned signature;
wenzelm
parents: 20925
diff changeset
    28
fun set_secure () = secure := true;
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    29
fun is_secure () = ! secure;
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    30
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    31
fun deny_secure msg = deny (is_secure ()) msg;
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    32
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    33
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    34
(** critical operations **)
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    35
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    36
(* ML evaluation *)
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    37
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    38
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    39
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    40
val orig_use_text = use_text;
21770
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    41
val orig_use_file = use_file;
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    42
22144
c33450acd873 use_text: added name argument;
wenzelm
parents: 21770
diff changeset
    43
fun use_text name pr verbose txt = (secure_mltext (); orig_use_text name pr verbose txt);
21770
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    44
fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name);
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    45
val use = use_file Output.ml_output true;
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    46
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    47
(*commit is dynamically bound!*)
22144
c33450acd873 use_text: added name argument;
wenzelm
parents: 21770
diff changeset
    48
fun commit () = orig_use_text "" Output.ml_output false "commit();";
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    49
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    50
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    51
(* shell commands *)
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    52
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    53
fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    54
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    55
val orig_execute = execute;
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    56
val orig_system = system;
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    57
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    58
fun execute s = (secure_shell (); orig_execute s);
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    59
fun system s = (secure_shell (); orig_system s);
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    60
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    61
end;
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    62
21770
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    63
val use_text = Secure.use_text;
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    64
val use_file = Secure.use_file;
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    65
val use = Secure.use;
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    66
val execute = Secure.execute;
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    67
val system = Secure.system;