/
permission.aml
217 lines (186 loc) · 8.47 KB
/
permission.aml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
(* code that handles creating permissions andchecking whether one permission allows another *)
(* Java permissions are of the following types:
datatype Perm =
(* located in allpermission.aml *)
AllPerm : Perm
(* located in filepermission.aml *)
| FilePerm : (Int, Bool, Bool, String) -> Perm
| SocketPerm
| NetPerm
| SecurityPerm
| RuntimePerm
| PropertyPerm
| AWTPerm
| ReflectPerm
| SerializablePerm *)
(* used to package strings, tuples, ints, and bool in an options object *)
datatype Arg = StringArg : String -> Arg
| TupleArg : (List Arg) -> Arg
| IntArg : Int -> Arg
| BoolArg : Bool -> Arg
| InetAddrArg : InetAddr -> Arg
case-advice around (| #val_to_string# |) (x:Arg, st, fi):String =
case x of
StringArg s => val_to_string s
| TupleArg l => val_to_string l
| IntArg i => val_to_string i
| BoolArg b => val_to_string b
| InetAddrArg ia => val_to_string ia
(*fun equalArg (a1, a2) =
case (a1, a2) of
(StringArg s1, StringArg s2) =>
s1 == s2
| (TupleArg a1s, TupleArg a2s) =>
equalArgs (a1s, a2s)
| (IntArg i1, IntArg i2) =>
i1 == i2
| (BoolArg b1, BoolArg b2) =>
b1 == b2
| (InetAddrArg ia1, InetAddrArg ia2) =>
netEquals (ia1, ia2)
fun equalsArgs (a1s, a2s) =
case (a1s, a2s) of
(a1::a1s, a2::a2s) =>
equalArg (a1, a2) andalso equalArgs (a1s, a2s)
| (Nil, Nil) => True
| _ => False
fun equalsPerm (p1, p2):Bool =
case (p1,p2) of
((n1, a1), (n2,a2)) =>
n1 == n2 andalso equalsArgs (a1, a2) *)
fun unwrapArg x =
case x of
(InetAddrArg a) :: t => a ::(unwrapArg t)
| Nil => Nil
| _ => abort "unwrapArg: Should be impossible"
(* a table containing the name of a permission in the policy file, a new function to create the permission, and an implies permission to determine if the permission implies another *)
val permission_table = ref (Nil : List (String, (String,String) -> (String, List Arg) , ((String, List Arg), (String, List Arg)) -> Bool, ((String, List Arg), (String, List Arg)) -> Option (String, List Arg)))
(* type permission = (String, List Arg) *)
(* type permission_entry = (String, (String,String) -> Perm, (Perm,Perm) -> Bool) *)
(* fun addPermission : permission_entry -> Unit *)
(* adds a permission name, new function, and implies function to the permission_table *)
fun addPermission (pe : (String,
(String,String) -> (String,List Arg),
((String,List Arg), (String,List Arg)) -> Bool,
((String,List Arg), (String,List Arg)) -> Option (String,List Arg))) : Unit =
permission_table := (pe::(!permission_table))
(* fun arg_to_string : Arg -> String *)
(* unwraps a value *)
fun arg_to_string (arg : Arg) : String =
case arg of
StringArg s => s
| TupleArg _ => "[unprintable]"
| IntArg i => int_to_string i
| BoolArg b => bool_to_string b
| _ => abort "args_to_string: Should be impossible.\n"
(* fun args_to_string : Arg list -> string *)
(* unwraps a list of values *)
fun args_to_string (args : List Arg) : String =
case args of
(arg::args) => (arg_to_string arg) ^ "," ^ (args_to_string args)
| Nil => ""
(* perm_to_string : permission -> string *)
(* pretty printing permissions *)
fun perm_to_string (name : String,
args : List Arg) : String =
name ^ "(" ^ args_to_string args ^ ")"
(* getPermissionName : permission -> string *)
(* pretty-printing name of permission *)
fun getPermissionName (p : (String,List Arg)) : String =
case p of
(n,_) => n
| _ => abort "getPermissionName: Should be impossible"
(* getPermissionArgs : permission -> Arg list *)
(* gets the internal structure of the permission *)
fun getPermissionArgs (p : (String, List Arg)) : List Arg =
case p of
(_,a) => a
| _ => abort "getPermissionArgs: Should be impossible"
(* getNamePermission : permission_entry -> string *)
(* gets the name of the permission from the permission table *)
fun getNamePermission (pe : (String,
(String,String) -> (String,List Arg),
((String,List Arg), (String,List Arg)) -> Bool,
((String,List Arg), (String,List Arg)) -> Option (String,List Arg))) : String =
case pe of
(n,_,_,_) => n
| _ => abort "getNamePermission: Should be impossible"
(* getNewPermission : permission_entry -> (String,String) -> permission *)
(* gets the new permission function of the permission from the permission table *)
fun getNewPermission (pe : (String,
(String,String) -> (String,List Arg),
((String,List Arg), (String,List Arg)) -> Bool,
((String,List Arg), (String,List Arg)) -> Option (String,List Arg))) : (String,String) -> (String,List Arg) =
case pe of
(_,np,_,_) => np
| _ => abort "getNewPermission: Should be impossible."
(* getImpliesPermission : permission_entry -> perm * perm -> bool *)
(* gets the implies permission function of the permission from the permission table *)
fun getImpliesPermission (pe : (String,
(String,String) -> (String,List Arg),
((String,List Arg), (String,List Arg)) -> Bool,
((String,List Arg), (String,List Arg)) -> Option (String,List Arg))) : ((String,List Arg), (String,List Arg)) -> Bool =
case pe of
(_,_,ip,_) => ip
| _ => abort "getImpliesPermission: Should be impossible."
fun getIntersectPermission (pe : (String,
(String,String) -> (String,List Arg),
((String,List Arg), (String,List Arg)) -> Bool,
((String,List Arg), (String,List Arg)) -> Option (String,List Arg))) : ((String,List Arg), (String,List Arg)) -> Option (String,List Arg) =
case pe of
(_,_,_,ip) => ip
| _ => abort "getIntersectPermission: Should be impossible."
(* getPermissionEntry' : string * permission_entry list -> permission_entry *)
(* helper function for finding a permission_entry from the permission table *)
fun getPermissionEntry' (name : String,
pes : List (String,
(String,String) -> (String,List Arg),
((String,List Arg), (String,List Arg)) -> Bool,
((String,List Arg), (String,List Arg)) -> Option (String,List Arg))) =
case pes of
(pe::pes) => if name == getNamePermission pe
then pe
else getPermissionEntry' (name, pes)
| Nil => abort ("Permission " ^ name ^ " not found.\n")
(* getPermissionEntry : string -> permission_entry *)
(* finds a permission_entry from the permission table *)
fun getPermissionEntry (name : String) =
getPermissionEntry' (name, !permission_table)
(* fun newPermission : string * string * string -> permission *)
(* takes the name of the permission and option strings 1 and 2, looks up the permission in the permission table, and creates a new permission *)
fun newPermission (name : String,
s1 : String,
s2 : String) : (String,List Arg) =
(getNewPermission (getPermissionEntry name)) (s1, s2)
(* fun impliesPermission : permission * permission -> bool *)
(* takes two permissions, looks up the first permission in the permission table, and calls the proper imples function *)
fun impliesPermission (p1 : (String,List Arg),
p2 : (String,List Arg)) : Bool =
(getImpliesPermission (getPermissionEntry (getPermissionName p1))) (p1, p2)
(* impliesPermissions : permission list * permission -> bool *)
(* takes a list of permissions and another permision, and calls the implies function on each of the first lists's permissions with the second permision *)
fun impliesPermissions (ps : List (String,List Arg),
p : (String, List Arg)) : Bool =
case ps of
(p'::ps') => ((impliesPermission (p', p)) orelse (impliesPermissions (ps', p)))
| Nil => False
fun intersectPermission (p1 : (String,List Arg),
p2 : (String,List Arg)) : Option (String,List Arg) =
(*let val _ = print (perm_to_string p1 ^ " ^ " ^ perm_to_string p2)
val p3opt = *)
(getIntersectPermission (getPermissionEntry (getPermissionName p1))) (p1, p2)
(*val _ = case p3opt of Some p3 => print (" = " ^ perm_to_string p3 ^ "\n") | None => print "none\n"
in
p3opt
end*)
fun intersectPermissions' (p1 : (String,List Arg), ps2 : List (String,List Arg)) : List (String,List Arg) =
case ps2 of
(p2::ps2') => (case intersectPermission (p1,p2) of
Some p3 => p3::(intersectPermissions' (p1, ps2'))
| None => intersectPermissions' (p1, ps2'))
| Nil => Nil
fun intersectPermissions (ps1 : List (String,List Arg), ps2 : List (String,List Arg)) : List (String,List Arg) =
case ps1 of
(p::ps) => listConcat (intersectPermissions' (p, ps2),
intersectPermissions (ps,ps2))
| Nil => Nil