slat

slat(1)                              slat                              slat(1)



NAME
       slat - SE Linux policy file analysis tools

SYNOPSIS
       apol2slat [MAPPING]
       slat [-v] [-o OUTPUT] POLICY [FLOW]
       lts2smv [-v] [-o OUTPUT] [LTS [DIAGRAMS]]

DESCRIPTION
       This  manual  page  briefly  describes the slat package.  It is used to
       analyze SE Linux policy, and see if it meets policy goals.  It does  so
       by  transforming  policy  and the goals into input for a model checker.
       The model checker reports policy goal failures it finds.

       There are three programs used to prepare input for the  model  checker,
       apol2slat, slat, and lts2smv.

       The  apol2slat program translates an APOL-style permission mapping into
       a slat permission mapping.  In both file formats, each class-permission
       pair is designated as allowing write-like flow, read-like flow, flow in
       both directions, or no flow at all.  When information flows from a pro-
       cess  to  a  resource, it is called write-like, and the reverse flow is
       called read-like.  Unspecified class-permission pairs  are  assumed  to
       not allow information flow in either direction.

       The  slat program extracts an information flow transition relation as a
       labeled transition system (LTS) from an SE Linux  binary  policy.   The
       policy  file defines the authorized transitions.  The flow file defines
       the direction of information flow for each authorized transition.

       Information flow policy goals are expressed  in  diagram  syntax.   The
       lts2smv  program  transforms  an information flow LTS and a sequence of
       diagrams into SMV model checker  input.   It  will  also  transform  an
       authorization  LTS  into  SMV model checker input.  To see how the dia-
       grams in diagrams.txt translate into SMV syntax without  translating  a
       labeled transition system, type:

       lts2smv "" diagram.txt

       The program NuSMV is a model checker that accepts SMV input syntax.  If
       NuSMV is not installed on your system,  the  package  is  available  at
       http://nusmv.irst.itc.it/.

       A complete example follows.  The policy file is the binary policy to be
       analyzed, the apol_perm_mapping file is an APOL permission mapping, and
       disk.txt  contains policy goals as diagrams.  The results are placed in
       the disk.log file.

       apol2slat apol_perm_mapping | slat -o flow.lts policy
       lts2smv -o disk.smv flow.lts disk.txt
       nice time NuSMV -f disk.smv > disk.log 2>&1


OPTIONS
       -v     display version information and exit

       -o OUTPUT
              send output to this file (default stdout)

       --     treat remaining args as file names, where - means stdin


AUTHOR
       This program, was written by Joshua D. Guttman, Amy L. Herzog, and John
       D. Ramsdell of The MITRE Corporation.  The man page was written by Rus-
       sell Coker <russell AT coker.au> and John D. Ramsdell.


SEE ALSO
       /usr/share/doc/slat/slat.html



russell AT coker.au                                                   slat(1)