---
name: "slat"
section: "1"
platform: "linux"
package: "slat"
version: "2.0-5"
release: "Debian 5.0 (Lenny)"
platforms: ["linux"]
url: "https://new.carta.tech/slat"
---

# slat(1)

SE Linux policy file analysis tools

## 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 process 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 diagrams 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 Russell Coker \<russell@coker.com.au\> and John D. Ramsdell.

## SEE ALSO

**/usr/share/doc/slat/slat.html**