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
|
SLAT: SE Linux policy file analysis.
The best source for user documentation is the file info/slat.html.
The best source for installation documentation is the file INSTALL.
This file contains only a quick overview.
BUILDING AND INSTALLING
Be sure that the static version of the sepol library is available.
Using GNU make, build the program with the commands:
$ ./configure
$ make
You're done! You can also install the software with "make install".
See INSTALL for the full instructions on the install target.
You can get command line help with the commands:
$ slat -h
$ lts2smv -h
SOURCE CONTENTS
The directory info contains user documentation, and the directory doc
contains design documentation.
The directory src contains all the program sources. The sources for
the slat program are in the subdirectory slat, and the sources for the
lts2smv program are in lts2smv. The slat program extracts an
information flow relation from two SELinux configuration files, and
stores it as a labeled transition system (LTS).
The directory formula contains C routines you can used to parse and
pretty print LTS formated data. A generic pretty printer as also
available for general use.
QUICK START
To translate an APOL style permission mapping into the one used by
slat, type
$ apol2slat apol_perm_mapping_ver18 > mls.spm
To generate a labeled transition system, type
$ slat -o slat.lts policy mls.spm
where slat.lts is the output file, policy is the SE Linux binary
policy file, and mls.spm is an old style multilevel security file.
To generate a NuSMV source file, type
$ lts2smv -o slat.smv slat.lts diagram.txt
where slat.smv is the output file, slat.lts contains the labeled
transition system generated by slat, and diagram.txt is a file
containing one or more diagrams separated by semicolons.
You can connect slat and lts2smv with a pipe via the command:
$ slat policy.conf mls.spm | lts2smv -o slat.smv -- - diagram.txt
To see how a diagram translates into SMV syntax without translating
a labeled transition system, type:
$ lts2smv "" diagram.txt
DIAGRAMS
The syntax of a diagram is:
diagram ::= "[" arrows "]" state excepts? | state
arrow ::= state "," action "+"?
excepts ::= "[" state ";" action "]"
where arrows is a semicolon separated sequence of a pair of a state
and an action given by the arrow syntax. An arrow annotated with "+"
indicates one or more steps are allowed satisfying the annotated
action.
The syntax of a state formula is
state ::=
| "t" ":" "{" comma-separated-atoms "}" -- type set
| "r" ":" "{" comma-separated-atoms "}" -- role set
| "u" ":" "{" comma-separated-atoms "}" -- user set
| "TRUE" | "FALSE"
| "!" state
| state "&" state
| state "|" state -- the precedence of "|" is lower than "&"
The syntax of an action formula is
action ::=
| "c" ":" "{" comma-separated-atoms "}" -- class set
| "p" ":" "{" comma-separated-atoms "}" -- permission set
| "TRUE" | "FALSE"
| "!" action
| action "&" action
| action "|" action -- the precedence of "|" is lower than "&"
Formula abbreviations include
X "=" atom => X ": {" atom "}"
X "!=" atom => "!(" X ": {" atom "})"
X "!:" set => "!(" X ":" set ")"
where X is t, r, u, c, or p.
EXAMPLE
[t=user_t & r=user_r & u!=jadmin, TRUE+;
t=sshd_tmp_t, c=process]
t=sshd_t
|
