---
name: "poldecond"
section: "1"
platform: "linux"
package: "slat"
version: "1.2.6-1"
release: "Debian 3.1 (Sarge)"
platforms: ["linux"]
url: "https://new.carta.tech/slat"
---

# poldecond(1)

SE Linux policy file analysis tools

Part of [slat(1)](/slat/1.md).

## NAME

slat - SE Linux policy file analysis tools

## SYNOPSIS

**poldecond** \[**-v**\] \[**-o***OUTPUT*\] \[*INPUT...*\]\
 **slat** \[**-v**\] \[**-a**\] \[**-f**\] \[**-o***OUTPUT*\] \[*POLICY* \[*MLS*\]\]\
 **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, **poldecond**, **slat**, and **lts2smv**.

The **poldecond** program removes boolean conditional expressions from the policy source. The program extracts the unconditional 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. Better yet, one can place the overriding definitions in their own file and read the policy configuration file after the overriding definitions. The **poldecond** program's input is obtained by concatenating the content from the input files given on the command line.

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

The **slat** program can also be used to extract an authorization transition relation and check **neverallow** statements in the policy. The authorization transition relation as a labeled transition system is obtained by using the **-a** option, and omitting the MLS file.

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.conf file is the policy to be analyzed, the mls file is the multilevel security file, the overrides.conf file contains boolean overrides, and disk.txt contains policy goals as diagrams. The results are placed in the disk.log file.

poldecond -o decond-policy.conf overrides.conf policy.conf\
 slat -o flow.lts decond-policy.conf mls\
 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

- **-a**

  generate an authorization transition relation (slat only)

- **-f**

  generate an information flow transition relation (default, slat only)

- **-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**