author | wenzelm |
Mon, 23 Jul 2007 14:06:12 +0200 | |
changeset 23922 | 707639e9497d |
parent 22567 | 1565d476a9e2 |
child 23978 | 6e8d5a05ffe8 |
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 |
20925 | 14 |
val use: string -> unit |
15 |
val commit: unit -> unit |
|
20992 | 16 |
val execute: string -> string |
17 |
val system: string -> int |
|
20925 | 18 |
end; |
19 |
||
20 |
structure Secure: SECURE = |
|
21 |
struct |
|
22 |
||
20992 | 23 |
(** secure flag **) |
20925 | 24 |
|
25 |
val secure = ref false; |
|
26 |
||
20977 | 27 |
fun set_secure () = secure := true; |
20925 | 28 |
fun is_secure () = ! secure; |
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 | 31 |
|
32 |
||
20992 | 33 |
(** critical operations **) |
34 |
||
35 |
(* ML evaluation *) |
|
20925 | 36 |
|
37 |
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; |
|
38 |
||
39 |
val orig_use_text = use_text; |
|
21770 | 40 |
val orig_use_file = use_file; |
20925 | 41 |
|
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
42 |
fun use_text name pr verbose txt = CRITICAL (fn () => |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
43 |
(secure_mltext (); orig_use_text name pr verbose txt)); |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
44 |
|
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
45 |
fun use_file pr verbose name = CRITICAL (fn () => |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
46 |
(secure_mltext (); orig_use_file pr verbose name)); |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
47 |
|
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
48 |
fun use name = CRITICAL (fn () => use_file Output.ml_output true name); |
20925 | 49 |
|
50 |
(*commit is dynamically bound!*) |
|
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
51 |
fun commit () = CRITICAL (fn () => orig_use_text "" Output.ml_output false "commit();"); |
20925 | 52 |
|
20992 | 53 |
|
54 |
(* shell commands *) |
|
55 |
||
56 |
fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode"; |
|
57 |
||
58 |
val orig_execute = execute; |
|
59 |
val orig_system = system; |
|
60 |
||
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
61 |
fun execute s = CRITICAL (fn () => (secure_shell (); orig_execute s)); |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
62 |
fun system s = CRITICAL (fn () => (secure_shell (); orig_system s)); |
20992 | 63 |
|
20925 | 64 |
end; |
65 |
||
21770 | 66 |
val use_text = Secure.use_text; |
67 |
val use_file = Secure.use_file; |
|
20925 | 68 |
val use = Secure.use; |
20992 | 69 |
val execute = Secure.execute; |
70 |
val system = Secure.system; |