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
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
|
2005-07-05 John D. Ramsdell <ramsdell@mitre.org>
* CVS: tagged sources as slat-2_0.
2005-06-30 John D. Ramsdell <ramsdell@mitre.org>
* src/slat/slat.c: Changed slat to read binary policies. The
program is now built upon a library provided by the libsepol-devel
package.
* src/slat/apol2slat.in: Added a script that converts APOL style
permission mappings into the format used by SLAT. The format is
the common and class declaration part of an old-style mls file.
* src/poldecond/*: Deleted poldecond as reading source policies is
no longer supported.
* src/formula/formula.c (mk_tran*): Changed some formula
constructors so they do constant folding.
* src/formula/formula.c (ptran): Added a new group so that printed
LTS formulas better represent the precedence of conjunction and
disjunction.
* src/lts2smv/gensmv.c (ptran): Added a new group so that printed
SMV formulas better represent the precedence of conjunction and
disjunction
2005-02-28 Brian T. Sniffen <bsniffen@mitre.org>
* CVS: tagged sources as slat-1_2_6.
* parser.y: Be much more lax about if syntax: don't require
parens around the conditional.
2005-02-28 John D. Ramsdell <ramsdell@mitre.org>
* src/poldecond/scanner.l: Allow #line entries to be preceded by
other text on an input line.
2005-01-11 John D. Ramsdell <ramsdell@mitre.org>
* CVS: tagged sources as slat-1_2_5.
* src/poldecond/scanner.l: Fixed line numbering error and treat
#line entries by immediately printing them.
2004-12-20 John D. Ramsdell <ramsdell@mitre.org>
* info/slat.texi: Changed the top part of the document so that the
generated HTML omits bad links.
2004-11-06 John D. Ramsdell <ramsdell@mitre.org>
* CVS: tagged sources as slat-1_2_4.
* ml/Makefile.am (bin_SCRIPTS): Converted this directory so its
contents are built from a makefile generated by automake.
* doc/Makefile.am (dist_pkgdata_DATA): Converted this directory so
its contents are built from a makefile generated by automake.
2004-11-04 John D. Ramsdell <ramsdell@mitre.org>
* CVS: tagged sources as slat-1_2_3.
* src/lts2smv/gensmv.c (pnextop, paxop): The precedence used to
print the argument to EX and AX is now NEXT, instead of MIN_PREC.
This change ensures parenthesis are added when they needed.
2004-06-26 John D. Ramsdell <ramsdell@mitre.org>
* CVS: tagged sources as slat-1_2_2.
* ml/parse_policy_mls.mly: Require semicolon terminator for
typealias statement.
* src/poldecond/scanner.l: Reset lineno in yywrap so that error
messages identify the correct line number when taking input from
more than one input file.
* info/slat.1: Corrected errors and marked some options as slat
only.
2004-06-23 John D. Ramsdell <ramsdell@mitre.org>
* CVS: tagged sources as slat-1_2_1.
* src/poldecond/poldecond.c: Changed the command line arguments so
that input can be obtained from more than one file.
* info/{poldecond.1,slat.1,lts2smv.1}: Added manual pages. Thanks
go to Russell Coker.
2004-06-22 John D. Ramsdell <ramsdell@mitre.org>
* CVS: tagged sources as slat-1_2.
* slat.spec.in: Added definitions so that binaries are not
stripped. Binaries created by O'Caml will fail to find the
bytecode they contain if they are stripped.
2004-06-19 John D. Ramsdell <ramsdell@mitre.org>
* ml/identifier.ml, ml/parse_policy_mls.mly: Added support for
typealias statements, type exclusion notation, and nodecon ipv6
entries. The default policy included with Fedore Core 2 can now
be analyzed, as long as it is preprocessed with poldecond.
* src/lts2smv/*: Program lts2smv is now written in C.
2004-06-18 John D. Ramsdell <ramsdell@mitre.org>
* ml/Makefile.in: Makes a bytecode version of the slat program so
that the native O'Caml compiler need be available.
2004-06-15 John D. Ramsdell <ramsdell@mitre.org>
* libpprint.a, libslatform.a, and libslatformparser.a: These
libraries are installed along with their header files.
* libpprint.a: The generic pretty printing routines used for
formula printing have been placed in their own library. The
routines may be useful to projects other than those analyzing
SELinux policy configuration files.
* {ml,doc}/Makefile.in: Removed ref to mkinstdirs in favor of
mkdir_p.
2004-06-10 John D. Ramsdell <ramsdell@mitre.org>
* configure.ac, Makefile.am: Added latex check so that sources
build when latex is not available. Latex still must be available
in order to make a distribution.
* Sources: Placed non-O'Caml program sources in the src directory.
2004-02-19 John D. Ramsdell <ramsdell@mitre.org>
* CVS: Tagged sources as slat-1_1_0.
* poldecond: 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.
2003-12-16 John D. Ramsdell <ramsdell@mitre.org>
* ml/Makefile.in, doc/Makefile.in (install): Added $(DESTDIR).
2003-11-18 John D. Ramsdell <ramsdell@mitre.org>
* configure.ac, Makefile.am: Added obstack conditional.
2003-10-30 John D. Ramsdell <ramsdell@mitre.org>
* configure.ac: Updated and renamed the configuration script spec.
2003-10-24 John D. Ramsdell <ramsdell@mitre.org>
* slat.spec.in: Added RPM spec template.
* doc/Makefile.in (all): All target only makes PDF. Distribution
includes PDF.
* formula/parser.y: Allow optional semicolons in this parser too!
2003-10-21 John D. Ramsdell <ramsdell@mitre.org>
* Removed CVS keywords from the sources.
2003-10-17 John D. Ramsdell <ramsdell@mitre.org>
* ml/parse_formulas.mly (Formulas): Allow an optional semicolon at
the end of a set of arrows in a diagram, and at the end of a
sequence of diagrams.
2003-09-29 John D. Ramsdell <ramsdell@mitre.org>
* doc/Makefile.in: The command "make dist" includes the doc
directory.
2003-09-26 John D. Ramsdell <ramsdell@mitre.org>
* Tagged sources as slat-1_0_0.
* Added Jean-Christophe Filliatre's OCaml autoconf tricks, and
fixed various Makefiles. Also, version numbers are derived from
the one given in configure.in, and not from a CVS tag.
2003-09-24 John D. Ramsdell <ramsdell@mitre.org>
* Released version 1.0.0 beta 3.
* ml/lex_policy_mls.mll: Added parsing support for fs_use_xattr.
2003-07-22 John D. Ramsdell <ramsdell@mitre.org>
* Added the camuddy BuDDy OCaml integration package and produced a
version of typesallowed that uses BuDDy instead of the OCaml BDD
module in the ml directory.
2003-05-14 John D. Ramsdell <ramsdell@mitre.org>
* buddy/*: Added the BuDDy Binary Decision Diagrams package by
Jorn Lind-Nielsen.
2003-05-09 John D. Ramsdell <ramsdell@mitre.org>
* form/pp.c: Added a formula processing library written in C.
2003-05-08 John D. Ramsdell <ramsdell@mitre.org>
* info/slat.texi: The user manual was converted to texinfo.
* Reorganized the directory structure to allow C source
integration.
2003-04-25 John D. Ramsdell <ramsdell@mitre.org>
* Released version 1.0.0 beta 2 and added typesallowed
documentation.
2003-04-24 John D. Ramsdell <ramsdell@mitre.org>
* typesallowed.ml: Added the typesallowed program.
2003-04-02 John D. Ramsdell <ramsdell@mitre.org>
* parse_policy_mls.mly: parser changed to accept the extended
class of user identifiers and paths specified by the latest
version of the checkpolicy parser.
2003-04-01 John D. Ramsdell <ramsdell@mitre.org>
* README and INSTALL instructs installers to generate the native
Objective Caml compiler.
2003-03-28 John D. Ramsdell <ramsdell@mitre.org>
* Released version 1.0.0 beta
* configure.in: Added a configure script and (un)install targets.
* GNUmakefile: Removed the sources for the old version of slat.
2003-03-26 John D. Ramsdell <ramsdell@mitre.org>
* identifier.ml (emit_transition): The translation relation was
changed so that the constraints that result from the role and user
definitions apply to the current state too. Previously, they only
applied to the next state.
* lts2smv.ml: lts2smv can translate diagrams into SMV syntax
without translating a labeled transition system.
2003-03-25 John D. Ramsdell <ramsdell@mitre.org>
* identifier.ml (slat): Generate specifications from neverallows
only when generating an authorization transition relation.
* Released version 0.5.
* nusmv.ml: lts2smv can new emit specifications in LTL, or behave
as before and generate them in CTL.
* identifier.ml (emit_transition): slat can now emit an
authorization transition relation, or behave as before and emit an
information flow transition relation.
2003-03-24 John D. Ramsdell <ramsdell@mitre.org>
* identifier.ml: Completely new implementation based on the
algorithms described in doc/slat.tex.
* parse_policy_mls.mly: Added new parser and scanner based on
Stephen Smalley's code in checkpolicy.
2003-03-17 John D. Ramsdell <ramsdell@mitre.org>
* lts2smv.ml: This program generates NuSMV output from lts.
* slat.ml: The slat program no longer generates NuSMV output.
* GNUmakefile: Reorganized makefile so that it produces more than
one program and is easier to maintain.
2003-03-05 John D. Ramsdell <ramsdell@mitre.org>
* Released version 0.2.
* nusmv.ml (form): Added a variant that describes NuSMV syntax.
2003-03-04 John D. Ramsdell <ramsdell@mitre.org>
* Released version 0.1.
|
