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
|
(* Security context formulas *)
type 'atoms contexts =
Ctx_true
| Ctx_false
| Ctx_types of 'atoms
| Ctx_roles of 'atoms
| Ctx_users of 'atoms
| Ctx_not of 'atoms contexts
| Ctx_and of 'atoms contexts * 'atoms contexts
| Ctx_or of 'atoms contexts * 'atoms contexts
| Ctx_imply of 'atoms contexts * 'atoms contexts
| Ctx_iff of 'atoms contexts * 'atoms contexts
(* Action formulas *)
type 'atoms actions =
Act_true
| Act_false
| Act_classes of 'atoms
| Act_permissions of 'atoms
| Act_not of 'atoms actions
| Act_and of 'atoms actions * 'atoms actions
| Act_or of 'atoms actions * 'atoms actions
| Act_imply of 'atoms actions * 'atoms actions
| Act_iff of 'atoms actions * 'atoms actions
(* Transition formulas *)
type 'atoms transitions =
Tran_true
| Tran_false
| Tran_classes of 'atoms
| Tran_permissions of 'atoms
| Tran_types of 'atoms
| Next_types of 'atoms
| Same_types (* t = t' *)
| Tran_roles of 'atoms
| Next_roles of 'atoms
| Same_roles (* r = r' *)
| Tran_users of 'atoms
| Next_users of 'atoms
| Same_users (* u = u' *)
| Tran_not of 'atoms transitions
| Tran_and of 'atoms transitions * 'atoms transitions
| Tran_or of 'atoms transitions * 'atoms transitions
| Tran_imply of 'atoms transitions * 'atoms transitions
| Tran_iff of 'atoms transitions * 'atoms transitions
(* Diagrams *)
type 'atoms diagram =
('atoms contexts * 'atoms actions * bool) list * (* arrows *)
'atoms contexts * (* final state *)
'atoms contexts * 'atoms actions (* exceptions *)
(* An information flow policy labeled transition system *)
type 'atoms lts = {
types : 'atoms; (* All security context types *)
roles : 'atoms; (* All security context roles *)
users : 'atoms; (* All security context users *)
classes : 'atoms; (* All action classes *)
permissions : 'atoms; (* All action permissions *)
initial : 'atoms contexts; (* The initial security contexts *)
transition : 'atoms transitions; (* The transition relation *)
specifications : 'atoms transitions list (* Specifications to be checked *)
(* The specifications are generated from neverallow and the like. *)
}
(* Printers *)
val print_contexts : string list contexts -> unit
val print_actions : string list actions -> unit
val print_transitions : string list transitions -> unit
val print_diagram : string list diagram -> unit
val print_lts : string list lts -> unit
|
