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
|
SLAT NEWS -- history of user-visible changes. 2005-06-30
Copyright (C) 2003 The MITRE Corporation
See the end for copying conditions.
* Changes in SLAT 2.0
** SLAT reads binary policies.
Reading binary policy files simplifies many aspects of SLAT, for
example, the handling of conditionals. Other tools are used to
change the values of conditions before an analysis run. Therefore,
the poldecond program has been removed.
** APOL style permission mappings provide flow direction information.
The apol2slat script has been added. It translates APOL permission
mappings into a format that can be used by SLAT. The format is the
common and class declaration part of an old-style mls file.
* Changes in SLAT 1.2.1
** Added manual pages for poldecond, slat, and lts2smv.
** Changed the command line arguments of poldecond.
The output is now specified using the -o option. All other file names
on the command line are used to obtain input. One can change the
sense of boolean conditions by defining them in the first file read,
and then reading the original text policy configuration file.
* Changes in SLAT 1.2
** Updated slat so it handles new policy configuration language.
The new languages features supported follow.
*** Typealias statements
The statements allow one to declare additional aliases for a type
separate from the base type declaration.
*** Type exclusion notation
This notation allows expressions that denote a set of identifiers to
include ones that provide a limited form of set difference, by
excluding particular types or attributes from a type set.
*** Nodecon IPv6 entries
In addition to IPv4 addresses, one can now also specify IPv6
addresses.
** The slat program is slower.
Due to problems encountered while compiling O'Caml programs on Fedora
Core 2, the slat program is compiled into bytecode, rather than native
code. As a result, the program is slower, but the time it takes to
run is still tiny as compared with the time required by the model
checker.
** The typesallowed program is no longer provided.
Due to problems encountered while compiling O'Caml programs on Fedora
Core 2, all programs in future versions of this package will be
written in languages compiled by GCC. Since the typesallowed
program's value seems limited, it has been dropped rather than
scheduled for translation. The slat program is the currently the only
remaining program written in O'Caml.
The BuDDY package is still in the distribution in case typesallowed,
or another similar program is written in a language compiled by GCC.
** Info documentation improved.
The info document assumes most new policy.conf files will have boolean
conditionals, so usage examples include a poldecond command. The
sample Makefile also invokes the poldecond command.
* Changes in SLAT 1.1.0
** Added the poldecond program to handle policies that use conditionals.
The poldecond program handles policy configuration files that use the
conditional policy extension. The program extracts the
conditional-less policy defined by using the default value for each
boolean in the input. The value for the first boolean declaration
overrides all others, so one can derive other policies by adding
boolean declarations with different defaults at the beginning of the
input.
* Changes in SLAT 1.0.0
** The user manual in info/slat.html has been greatly improved.
** The slat program has been divided into two applications.
The slat program now generates only a labeled transition system. The
lts2smv program translates a labeled transition system into SMV
syntax.
** The slat parser now accepts periods and hyphens in user identifiers.
** The slat program generates an authorization transition relation.
When given the -auth flag, the slat program generates an authorization
transition relation instead of an information flow transition
relation. This labeled transition system can be used to check
neverallow specifications in a policy file by translating it into
SMV syntax using lts2smv, and giving the output to NuSMV.
** The lts2smv program translates diagrams into LTL specifications.
When given the -ltl flag, the lts2smv program generates LTL
specifications instead of CTL specifications.
** The lts2smv program can translate only diagrams.
If the first command line argument given the lts2smv program is ""
(the empty string), the program will not attempt to translate a
labeled transition system, and only translate diagrams.
** The typesallowed program can query authorization transition relations.
The typesallowed program can be used to list the set of output types
that are allowed by an authorization transition relation
restricted by a transition relation which forms the query.
** The design document in doc/slat.tex has been greatly improved.
----------------------------------------------------------------------
Copyright information:
Copyright (C) 2003 The MITRE Corporation
Permission is granted to anyone to make or distribute verbatim copies
of this document as received, in any medium, provided that the
copyright notice and this permission notice are preserved,
thus giving the recipient permission to redistribute in turn.
Permission is granted to distribute modified versions
of this document, or of portions of it,
under the above conditions, provided also that they
carry prominent notices stating who last changed them.
Local variables:
mode: outline
paragraph-separate: "[ ]*$"
end:
|
