author | wenzelm |
Wed, 21 Jan 2009 23:21:44 +0100 | |
changeset 29606 | fedb8be05f24 |
parent 28268 | ac8431ecd57e |
child 30625 | d53d1a16d5ee |
permissions | -rw-r--r-- |
20925 | 1 |
(* Title: Pure/General/secure.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Secure critical operations. |
|
5 |
*) |
|
6 |
||
7 |
signature SECURE = |
|
8 |
sig |
|
20977 | 9 |
val set_secure: unit -> unit |
20925 | 10 |
val is_secure: unit -> bool |
26080 | 11 |
val deny_secure: string -> unit |
28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
12 |
val use_text: ML_NameSpace.nameSpace -> int * string -> |
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
13 |
(string -> unit) * (string -> 'a) -> bool -> string -> unit |
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
14 |
val use_file: ML_NameSpace.nameSpace -> |
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
15 |
(string -> unit) * (string -> 'a) -> bool -> string -> unit |
20925 | 16 |
val use: string -> unit |
17 |
val commit: unit -> unit |
|
26220 | 18 |
val system_out: string -> string * int |
20992 | 19 |
val system: string -> int |
20925 | 20 |
end; |
21 |
||
22 |
structure Secure: SECURE = |
|
23 |
struct |
|
24 |
||
20992 | 25 |
(** secure flag **) |
20925 | 26 |
|
27 |
val secure = ref false; |
|
28 |
||
20977 | 29 |
fun set_secure () = secure := true; |
20925 | 30 |
fun is_secure () = ! secure; |
31 |
||
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22144
diff
changeset
|
32 |
fun deny_secure msg = if is_secure () then error msg else (); |
20925 | 33 |
|
34 |
||
25753 | 35 |
|
20992 | 36 |
(** critical operations **) |
37 |
||
38 |
(* ML evaluation *) |
|
20925 | 39 |
|
40 |
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode"; |
|
41 |
||
28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
42 |
fun raw_use_text ns = use_text ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns; |
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
43 |
fun raw_use_file ns = use_file ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns; |
20925 | 44 |
|
28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
45 |
fun use_text ns pos pr verbose txt = |
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
46 |
(secure_mltext (); raw_use_text ns pos pr verbose txt); |
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
47 |
|
28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
48 |
fun use_file ns pr verbose name = |
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
49 |
(secure_mltext (); raw_use_file ns pr verbose name); |
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
50 |
|
28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
51 |
fun use name = use_file ML_NameSpace.global Output.ml_output true name; |
23978 | 52 |
|
20925 | 53 |
(*commit is dynamically bound!*) |
28268
ac8431ecd57e
use_text/use_file now depend on explicit ML name space;
wenzelm
parents:
26883
diff
changeset
|
54 |
fun commit () = raw_use_text ML_NameSpace.global (0, "") Output.ml_output false "commit();"; |
20925 | 55 |
|
20992 | 56 |
|
57 |
(* shell commands *) |
|
58 |
||
59 |
fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode"; |
|
60 |
||
26220 | 61 |
val orig_system_out = system_out; |
20992 | 62 |
|
26220 | 63 |
fun system_out s = (secure_shell (); orig_system_out s); |
26332 | 64 |
|
65 |
fun system s = |
|
66 |
(case system_out s of |
|
67 |
("", rc) => rc |
|
68 |
| (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc)); |
|
20992 | 69 |
|
20925 | 70 |
end; |
71 |
||
23978 | 72 |
(*override previous toplevel bindings!*) |
21770 | 73 |
val use_text = Secure.use_text; |
74 |
val use_file = Secure.use_file; |
|
24663
015a8838e656
improved error behaviour of use (bootstrap version);
wenzelm
parents:
24600
diff
changeset
|
75 |
fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error"); |
26220 | 76 |
val system_out = Secure.system_out; |
20992 | 77 |
val system = Secure.system; |