src/Pure/General/secure.ML
author wenzelm
Thu, 06 Mar 2008 20:17:50 +0100
changeset 26220 d34b68c21f9a
parent 26080 d920e4c8ba82
child 26332 aa54cd3ddc9f
permissions -rw-r--r--
common setup for system_out/system;
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
26080
d920e4c8ba82 export deny_secure;
wenzelm
parents: 25753
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
26220
d34b68c21f9a common setup for system_out/system;
wenzelm
parents: 26080
diff changeset
    17
  val system_out: string -> string * int
20992
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
22567
1565d476a9e2 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents: 22144
diff changeset
    31
fun deny_secure msg = if is_secure () then error msg else ();
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    32
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    33
25753
99c9fc5e11f2 tuned spaces;
wenzelm
parents: 25703
diff changeset
    34
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    35
(** critical operations **)
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    36
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    37
(* ML evaluation *)
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    38
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    39
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    40
24600
5877b88f262c use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents: 24058
diff changeset
    41
fun orig_use_text x = use_text ML_Parse.fix_ints x;
5877b88f262c use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents: 24058
diff changeset
    42
fun orig_use_file x = use_file ML_Parse.fix_ints x;
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    43
25698
8c335b4641a5 use_text/use_file: non-critical (Poly/ML compiler is thread-safe);
wenzelm
parents: 25503
diff changeset
    44
fun use_text name pr verbose txt =
8c335b4641a5 use_text/use_file: non-critical (Poly/ML compiler is thread-safe);
wenzelm
parents: 25503
diff changeset
    45
  (secure_mltext (); orig_use_text name pr verbose txt);
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 22567
diff changeset
    46
25698
8c335b4641a5 use_text/use_file: non-critical (Poly/ML compiler is thread-safe);
wenzelm
parents: 25503
diff changeset
    47
fun use_file pr verbose name =
8c335b4641a5 use_text/use_file: non-critical (Poly/ML compiler is thread-safe);
wenzelm
parents: 25503
diff changeset
    48
  (secure_mltext (); orig_use_file pr verbose name);
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 22567
diff changeset
    49
23978
6e8d5a05ffe8 added use_noncritical;
wenzelm
parents: 23922
diff changeset
    50
fun use name = use_file Output.ml_output true name;
6e8d5a05ffe8 added use_noncritical;
wenzelm
parents: 23922
diff changeset
    51
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    52
(*commit is dynamically bound!*)
25503
fe14c6857f1d commit: non-critical, otherwise session restart will result in deadlock!
wenzelm
parents: 25204
diff changeset
    53
fun commit () = orig_use_text "" Output.ml_output false "commit();";
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    54
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    55
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    56
(* shell commands *)
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    57
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    58
fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    59
26220
d34b68c21f9a common setup for system_out/system;
wenzelm
parents: 26080
diff changeset
    60
val orig_system_out = system_out;
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    61
26220
d34b68c21f9a common setup for system_out/system;
wenzelm
parents: 26080
diff changeset
    62
fun system_out s = (secure_shell (); orig_system_out s);
d34b68c21f9a common setup for system_out/system;
wenzelm
parents: 26080
diff changeset
    63
fun system s = #2 (system_out s);
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    64
20925
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    65
end;
2d19e511fe2c Secure critical operations.
wenzelm
parents:
diff changeset
    66
23978
6e8d5a05ffe8 added use_noncritical;
wenzelm
parents: 23922
diff changeset
    67
(*override previous toplevel bindings!*)
21770
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    68
val use_text = Secure.use_text;
ea6f846d8c4b added use_file;
wenzelm
parents: 20992
diff changeset
    69
val use_file = Secure.use_file;
24663
015a8838e656 improved error behaviour of use (bootstrap version);
wenzelm
parents: 24600
diff changeset
    70
fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
26220
d34b68c21f9a common setup for system_out/system;
wenzelm
parents: 26080
diff changeset
    71
val system_out = Secure.system_out;
20992
05c3703cc6c5 added execute/system;
wenzelm
parents: 20977
diff changeset
    72
val system = Secure.system;