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