SLAT: SE Linux policy file analysis.

[ramsdell@mitre.org (John D. Ramsdell)]

The SELinux Analysis Tools (SLAT) provide a systematic way to
determine if security goals are achieved by a given SELinux policy
configuration.  In particular, SLAT is concerned with information flow
security goals, which describe desired paths by which information
moves throughout a system.  We provide a simple syntax in which to
express these goals.

The tools extract the allowed information flows specified by a given
SELinux policy configuration.  The information flow and the security
goals are translated into model checker input, which attempts to prove
that the policy configure meets the specified security goals.  Each
counterexample generated by the model checker indicates some
sort of configuration failure.

To make the tools more accessible, I've placed a source distribution
and an RPM at the following location:

http://www.ccs.neu.edu/home/ramsdell/tools/selinux/slat-1.0.1.tar.gz

http://www.ccs.neu.edu/home/ramsdell/tools/selinux/slat-1.0.1-1.i386.rpm  

The SLAT software uses OCaml, a dialect of ML.  The easiest way to
install it is with an RPM from:

http://caml.inria.fr

John

--
This message was distributed to subscribers of the selinux mailing list.
If you no longer wish to subscribe, send mail to majordomo@tycho.nsa.gov with
the words "unsubscribe selinux" without quotes as the message.