author | wenzelm |
Sat, 06 Nov 2010 16:53:07 +0100 | |
changeset 40392 | 6f47c49fed84 |
parent 38799 | 712cb964d113 |
child 40748 | 591b6778d076 |
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 |
31330 | 12 |
val secure_mltext: unit -> unit |
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
13 |
val use_text: use_context -> int * string -> bool -> string -> unit |
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
14 |
val use_file: use_context -> bool -> string -> unit |
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
29606
diff
changeset
|
15 |
val toplevel_pp: string list -> string -> unit |
37239 | 16 |
val PG_setup: unit -> unit |
20925 | 17 |
val commit: unit -> unit |
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32739
diff
changeset
|
18 |
val bash_output: string -> string * int |
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32739
diff
changeset
|
19 |
val bash: string -> int |
20925 | 20 |
end; |
21 |
||
22 |
structure Secure: SECURE = |
|
23 |
struct |
|
24 |
||
20992 | 25 |
(** secure flag **) |
20925 | 26 |
|
32738 | 27 |
val secure = Unsynchronized.ref false; |
20925 | 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 |
||
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
42 |
val raw_use_text = use_text; |
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
43 |
val raw_use_file = use_file; |
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
44 |
val raw_toplevel_pp = toplevel_pp; |
20925 | 45 |
|
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
46 |
fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt); |
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
47 |
fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name); |
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
22567
diff
changeset
|
48 |
|
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
49 |
fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp); |
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
29606
diff
changeset
|
50 |
|
32739 | 51 |
|
52 |
(* global evaluation *) |
|
53 |
||
54 |
val use_global = raw_use_text ML_Parse.global_context (0, "") false; |
|
55 |
||
56 |
fun commit () = use_global "commit();"; (*commit is dynamically bound!*) |
|
37239 | 57 |
|
38799
712cb964d113
structure Unsynchronized is never opened and set/reset/toggle have been discontinued;
wenzelm
parents:
37977
diff
changeset
|
58 |
fun PG_setup () = |
712cb964d113
structure Unsynchronized is never opened and set/reset/toggle have been discontinued;
wenzelm
parents:
37977
diff
changeset
|
59 |
use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;"; |
20925 | 60 |
|
20992 | 61 |
|
62 |
(* shell commands *) |
|
63 |
||
64 |
fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode"; |
|
65 |
||
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32739
diff
changeset
|
66 |
val orig_bash_output = bash_output; |
20992 | 67 |
|
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32739
diff
changeset
|
68 |
fun bash_output s = (secure_shell (); orig_bash_output s); |
26332 | 69 |
|
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32739
diff
changeset
|
70 |
fun bash s = |
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32739
diff
changeset
|
71 |
(case bash_output s of |
26332 | 72 |
("", rc) => rc |
73 |
| (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc)); |
|
20992 | 74 |
|
20925 | 75 |
end; |
76 |
||
23978 | 77 |
(*override previous toplevel bindings!*) |
21770 | 78 |
val use_text = Secure.use_text; |
79 |
val use_file = Secure.use_file; |
|
30672
beaadd5af500
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents:
30625
diff
changeset
|
80 |
fun use s = Secure.use_file ML_Parse.global_context true s |
31473 | 81 |
handle ERROR msg => (writeln msg; error "ML error"); |
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
29606
diff
changeset
|
82 |
val toplevel_pp = Secure.toplevel_pp; |
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32739
diff
changeset
|
83 |
val bash_output = Secure.bash_output; |
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32739
diff
changeset
|
84 |
val bash = Secure.bash; |