src/Pure/General/secure.ML
author wenzelm
Tue, 03 Apr 2007 19:24:11 +0200
changeset 22567 1565d476a9e2
parent 22144 c33450acd873
child 23922 707639e9497d
permissions -rw-r--r--
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
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
22144
c33450acd873 use_text: added name argument;
wenzelm
parents: 21770
diff changeset
    12
  val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
21770
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    13
  val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    14
  val use: string -> unit
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    15
  val commit: unit -> unit
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    16
  val execute: string -> string
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    17
  val system: string -> int
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    18
end;
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    19
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    20
structure Secure: SECURE =
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    21
struct
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    22
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    23
(** secure flag **)
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    24
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    25
val secure = ref false;
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    26
20977
dbf1eca9b34e tuned signature;
wenzelm
parents: 20925
diff changeset
    27
fun set_secure () = secure := true;
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    28
fun is_secure () = ! secure;
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    29
22567
1565d476a9e2 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents: 22144
diff changeset
    30
fun deny_secure msg = if is_secure () then error msg else ();
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    31
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    32
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    33
(** critical operations **)
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    34
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    35
(* ML evaluation *)
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    36
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    37
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    38
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    39
val orig_use_text = use_text;
21770
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    40
val orig_use_file = use_file;
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    41
22144
c33450acd873 use_text: added name argument;
wenzelm
parents: 21770
diff changeset
    42
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
    43
fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name);
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    44
val use = use_file Output.ml_output true;
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    45
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    46
(*commit is dynamically bound!*)
22144
c33450acd873 use_text: added name argument;
wenzelm
parents: 21770
diff changeset
    47
fun commit () = orig_use_text "" Output.ml_output false "commit();";
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    48
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    49
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    50
(* shell commands *)
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    51
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    52
fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    53
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    54
val orig_execute = execute;
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    55
val orig_system = system;
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    56
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    57
fun execute s = (secure_shell (); orig_execute s);
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    58
fun system s = (secure_shell (); orig_system s);
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    59
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    60
end;
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    61
21770
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    62
val use_text = Secure.use_text;
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    63
val use_file = Secure.use_file;
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    64
val use = Secure.use;
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    65
val execute = Secure.execute;
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    66
val system = Secure.system;