From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from jazzband.ncsc.mil (jazzband.ncsc.mil [144.51.5.4]) by tycho.ncsc.mil (8.12.8/8.12.8) with ESMTP id hB5I7pRb006585 for ; Fri, 5 Dec 2003 13:07:51 -0500 (EST) Received: from jazzband.ncsc.mil (localhost [127.0.0.1]) by jazzband.ncsc.mil with ESMTP id hB5I7oRV006463 for ; Fri, 5 Dec 2003 18:07:50 GMT Received: from smtp-bedford.mitre.org (smtp-bedford-x.mitre.org [192.160.51.76]) by jazzband.ncsc.mil with ESMTP id hB5I7ota006460 for ; Fri, 5 Dec 2003 18:07:50 GMT Received: from smtp-bedford.mitre.org (localhost.localdomain [127.0.0.1]) by smtp-bedford.mitre.org (8.11.6/8.11.6) with ESMTP id hB5I7oU08087 for ; Fri, 5 Dec 2003 13:07:50 -0500 To: SE Linux Cc: ramsdell@mitre.org Subject: SLAT: SE Linux policy file analysis. From: ramsdell@mitre.org (John D. Ramsdell) Date: 05 Dec 2003 13:07:49 -0500 In-Reply-To: <1070587102.27071.159.camel@hawaii.efficax.net> Message-ID: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: owner-selinux@tycho.nsa.gov List-Id: selinux@tycho.nsa.gov 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.