author | wenzelm |
Sat, 07 Jul 2007 18:39:17 +0200 | |
changeset 23637 | f3e16ee56f32 |
parent 22567 | 1565d476a9e2 |
child 23922 | 707639e9497d |
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 |
|
22144 | 42 |
fun use_text name pr verbose txt = (secure_mltext (); orig_use_text name pr verbose txt); |
21770 | 43 |
fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name); |
44 |
val use = use_file Output.ml_output true; |
|
20925 | 45 |
|
46 |
(*commit is dynamically bound!*) |
|
22144 | 47 |
fun commit () = orig_use_text "" Output.ml_output false "commit();"; |
20925 | 48 |
|
20992 | 49 |
|
50 |
(* shell commands *) |
|
51 |
||
52 |
fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode"; |
|
53 |
||
54 |
val orig_execute = execute; |
|
55 |
val orig_system = system; |
|
56 |
||
57 |
fun execute s = (secure_shell (); orig_execute s); |
|
58 |
fun system s = (secure_shell (); orig_system s); |
|
59 |
||
20925 | 60 |
end; |
61 |
||
21770 | 62 |
val use_text = Secure.use_text; |
63 |
val use_file = Secure.use_file; |
|
20925 | 64 |
val use = Secure.use; |
20992 | 65 |
val execute = Secure.execute; |
66 |
val system = Secure.system; |