\documentclass[twocolumn]{article}
%
\usepackage{url}

\newcommand{\slat}{\textsf{Slat}}
\newcommand{\selinux}{\textsf{SELinux}}
\newcommand{\nusmv}{\textsf{NuSMV}}

% Draft notes.  Remove these when finished.
% \newcommand{\note}[1]{\textsf{[#1]}}

\newcommand{\all}[1]{\forall #1\mathpunct.}
\newcommand{\cn}[1]{\mathop{\smash{\sf#1}}\!\mathop{\vphantom{#1}}\nolimits}
\newcommand{\dom}[1]{\mathop{\smash{\rm#1}}\!\mathop{\vphantom{#1}}\nolimits}
\newcommand{\ctl}[1]{\mathop{\smash{\bf#1}}\!\mathop{\vphantom{#1}}\nolimits}
\newcommand{\means}[1]{[\![#1]\!]}
\newcommand{\alts}{\mathbin|}

% CTL commands
\newcommand{\ctle}{\ctl{E}}
\newcommand{\ctla}{\ctl{A}}
\newcommand{\ctlu}{\mathbin{\bf U}}
\newcommand{\ctlr}{\mathbin{\bf R}}
\newcommand{\ctlef}{\ctl{EF}}
\newcommand{\ctlex}{\ctl{EX}}
\newcommand{\ctlag}{\ctl{AG}}

% LTL commands
\newcommand{\ltlg}{\mathop{\bf G}}
\newcommand{\ltlf}{\mathop{\bf F}}
\newcommand{\ltlx}{\mathop{\bf X}}
\newcommand{\ltlu}{\mathbin{\bf U}}
\newcommand{\ltlr}{\mathbin{\bf R}}
\newcommand{\ltlo}{\mathbin{\mathcal{O}}}

\newcommand{\initstate}{\mathcal{S}_0}
\newcommand{\transit}{\mathcal{R}}

\title{SLAT: Information Flow Analysis in Security Enhanced Linux\null
\thanks{This work was funded by the United States National Security
Agency.
Authors' address: The MITRE Corporation, 202 Burlington Road, Bedford MA,
01730-1420.}}
\author{Joshua D. Guttman \and Amy L. Herzog \and John D. Ramsdell}

\begin{document}

\maketitle

This paper describes the theoretical foundation of the Security
Enhanced Linux policy analysis tool
{\slat}~\cite{GuttmanHerzogRamsdell03}.  The goal of this paper is an
accurate and complete treatment of the subject, and is not intended as
an introduction to this topic.

\section{Information Flow Policy}\label{sec:policy}

The {\selinux} security server makes decisions about system calls, for
instance whether a process should be allowed to write to a particular
file, or whether a process should be allowed to overlay its memory
with the binary image contained at a particular pathname, and continue
executing the result.  For each system call, {\selinux} specifies one
or more checks that must be satisfied in order for the call to be
allowed.  Each check is labeled by a pair consisting of a \emph{class}
and a \emph{permission}.  The class describes a kind of resource that
the access involves, such as \texttt{file}, \texttt{process}, or
\texttt{filesystem}.  The permission describes the action itself, such
as \texttt{read}, \texttt{write}, \texttt{mount}, or \texttt{execute}.
We will use the term \emph{resource} to cover any object in an
{\selinux} system; processes, files, sockets, etc.~are all regarded as
resources.  Each resource has a \emph{security context} which
summarizes its security relevant status.

In making a check, the security server receives as input two facts,
the \emph{security contexts} of the process and of another resource
involved in the system call.  A security context is a tuple consisting
of three components,%
%
\footnote{or four components, if the system is compiled with support
  for multi-level security as it can be, but normally is not.  For
  definiteness, we will assume MLS support is not compiled into the
  kernel in the remainder of this paper, although the approach we
  describe is equally applicable if it is.}
%
called a \emph{type}, a \emph{role}, and a \emph{user}.  The user is
similar in intent to the normal Unix notion of user, and represents
the person on behalf of whom the system is executing a process or
maintaining a resource.  The role, derived from the literature on
role-based access control, is an intermediate notion intended to
specify that collections of users should be permitted to execute
corresponding collections of programs.  The main purpose of the
\emph{user} component is to specify what roles that user is permitted;
the main purpose of the \emph{role} is to specify what types of
processes those users are permitted to execute.  The type
specifications do the remainder of the work.

A labeled-transition system is used to model the information flow
policy specified by {\selinux} policy file.  A security context is a
state in the transition system, and an event labels each transition.
We now formally define an information flow policy.  The derivation of
an information flow policy from an {\selinux} policy file is described
in Section~\ref{sec:derive}.

As stated above, security context is a type-role-user triple.  For a
given information flow policy, let $T$ be the set of names for types,
$R$ be the set of names for roles, and $U$ be the set of names for
users, so that the set of security contexts $S$ is~$T\times R\times
U$.

An event is a class-permission pair.  Let $C$ be the set of names for
classes, and $P$ be the set of names for permissions, so that the set
of events $G$ is $C\times P$.

Formally, an information flow policy is a 4-tuple $(S,G,\Delta,S_0)$, where
$S$ is a finite set of security contexts, $G$ is a finite set of
events, $S_0\subseteq S$ is the set of initial security contexts, and
$\Delta\subseteq S\times G\times S$ is the information flow transition
relation.  When $(s, g, s')\in \Delta$, the information flow policy allows
information to flow from an object labeled by $s$ to one labeled by
$s'$ as a result of event~$g$.

The set of information flow paths of length~$n$, $P^n$, is the subset
of $(S\times G)^n\times S$, such that
%
\begin{displaymath}
(s_0, g_0, s_1, g_1,\ldots,s_{n-1},g_{n-1},s_n)
\end{displaymath}
%
is in $P^n$ if and only if $s_0\in S_0$ and $(s_i,g_i,s_{i+1})\in \Delta$
for all~$i<n$.  Note that $P^0=S_0$.

A path is in the set of infinite information flow paths, $P^\infty$,
if and only if $s_0\in S_0$ and $(s_i,g_i,s_{i+1})\in \Delta$ for all~$i$.

\subsection{Logic of the Transition System} 

We use many-sorted first order logic with equality.  The sorts are
$T,R,U,C$, and $P$.  We assume that the language has a constant for
each defined value of these sorts, and include axioms stating that
every value of a particular sort is equal to one of the constants of
that sort.  No predicates other than equality are needed.  We are
interested in formulas in this language involving at most the free
variables $t,r,u,c,p,t',r',u'$, which we call \emph{information flow
  transition formulas}.  Here a lowercase variable ranges over
the sort whose name is the same letter in uppercase.  Primed variables
refer to the value in the next state, and unprimed variables refer to
the value in the current state.

A \emph{state formula}~$\sigma$ is a formula containing at most the
free variables $t,r,u$.  A \emph{event formula}~$\gamma$ is a formula
containing at most the free variables $c,p$.  We write $\delta$ for
general information flow transition formulas.


For our purposes, we need not distinguish between a set of tuples and
a formula true of exactly the same tuples.  Furthermore, within
formulas, we will write $t\in\{\tau_1,\ldots,\tau_n\}$ as a shorthand
for $t=\tau_1\lor\cdots\lor t=\tau_n$.


\section{Deriving a Policy}\label{sec:derive}

An {\selinux} configuration file defines the names for classes,
permissions, types, and users, and all but one name for the roles.
The role \texttt{object\_r} is an implicit part of a configuration.

The main component in a configuration file is the type, accounting for
at least 22,000 out of the 22,500 access control statements in the
example policy file contained in the distribution.  The type is used
to specify the detailed interactions permitted between processes and
other resources.  Each type specification determines some actions that
are allowed; in the {\selinux} configuration file they are introduced
by the keyword {\texttt{allow}}.  For a request to succeed, some
{\texttt{allow}} statement in the configuration file must authorize
it.  

The syntax of a type allow statement follows.
\[\texttt{allow }T_s\;T_t : C_a\;P_a ;\]
Each {\texttt{allow}} statement specifies a set of process (source)
types~$T_s$, a set of resource (target) types~$T_t$, a set of
classes~$C_a$, and a set of permissions~$P_a$.  If a process whose
type is in $T_s$ requests an action with a class-permission pair in
$C_a\times P_a$ against a resource with type in $T_t$, then that
request is authorized.  As an information flow transition relation
formula, an allow statement means:
\[ \begin{array}{@{}l}
\alpha_t\means{\texttt{allow }T_s\;T_t : C_a\;P_a ;} ={}\\
\qquad (t\in T_s\land t'\in T_t\setminus\{\texttt{self}\}\land c\in
C_a\land p\in P_a) \lor{} \\
\qquad(\texttt{self}\in T_t\land t\in T_s\land t=t'\land c\in
C_a\land p\in P_a).
\end{array}
\]
%
The special identifier \texttt{self} is not the name of a type, but is
instead used like a target type to indicate that the statement should
be applied between each source type and itself.  Thus, the formula
generated for an allow statement must be simplified so as to eliminate
references to \texttt{self}.

When a process changes security context, the role may change, but
only when permitted by another form of the allow statement.
\[\texttt{allow }R_c\;R_n;\]
The role allow statement permits a process whose current role is in~$R_c$ to
transition to one with a new role in~$R_n$.  As a formula, the statement
means:
\[ \begin{array}{l}
\alpha_r\means{\texttt{allow }R_c\;R_n;} ={}\\
\qquad
\begin{array}{l}
c=\texttt{process}\wedge
p=\texttt{transition} \Rightarrow {}\\
\qquad r \in R_c\land r'\in R_n.
\end{array}
\end{array}
\]

A role is declared with the following syntax.
\[\texttt{role }\rho\texttt{ types }T_r;\]
In addition to declaring the role name~$\rho$, the statement defines
the set of types with which the role is permitted to be associated.
As a formula, the statement means:
\[\beta_r\means{\texttt{role }\rho\texttt{ types }T_r;}
= r=\rho\land t\in T_r.\]

A user is declared with the following syntax.
\[\texttt{user }\mu\texttt{ roles }R_u;\]
In addition to declaring the user name~$\mu$, the statement defines the
set of roles the user is permitted to assume.  As a formula, the
statement means:
\[\beta_u\means{\texttt{user }\mu\texttt{ roles }R_u;}
= u=\mu\land r\in R_u.\]

Constraint definitions specify additional limits on transitions with
the following syntax.
\[\texttt{constraint }C_c\;P_c\;\delta;\]
The constraint expression~$\delta$ has a natural translation as a
formula as long as role operations are limited to equality testing,
the case we observe.  As a formula, the statement
means:\[\chi\means{\texttt{constraint }C_c\;P_c\;\delta;} = c\in
C_c\land p\in P_c\Rightarrow\delta.\]


%   Some system calls (\texttt{exec} for instance) require
%   several class-permission pairs to be authorized.

Since we abstract from auditing and other issues that do not affect
information-flow security goals, the configuration file defines five
relations of interest.  Each relation is built up by statements
contained in the same configuration file.
%
\begin{itemize}
 \item $\alpha_t$ is the formula built up by disjoining the meaning
       of every type {\texttt{allow}} statement.
 \item $\alpha_r$ is the formula built up by disjoining the meaning
       of every role {\texttt{allow}} statement.
 \item $\beta_r$ is the formula built up by disjoining the meaning of
       every {\texttt{role}} statement to the formula
       $r=\texttt{object\_r}\land t\notin T_p$, where~$T_p$ is the set
       of process types.
 \item $\beta_u$ is the formula built up by disjoining the meaning of
       every {\texttt{user}} statement to the atomic proposition
       $r=\texttt{object\_r}$.  As a result, $\beta_u\land
       r=\texttt{object\_r}$ holds for all user names.
 \item $\chi$ is the formula built up by conjoining the meaning
       of every {\texttt{constraint}} statement.
\end{itemize}

In what follows, we write~$\tilde\delta$ to mean the formula derived
from~$\delta$ by interchanging primed and unprimed variables.

Some events (file write, for instance) transfer information from
process to resource, while others (file read, for instance) transfer
it from resource to process.  Let $\psi$ be a class name, and $\pi$ be
a permission name.  {\selinux} has a file that describes how each
$(\psi,\pi)$ transfers information, whether like a read, like a write,
in both directions, or in neither.  From it, we extract descriptions
of two sets, $\gamma_w$ and $\gamma_r$.  When
event~$(\psi,\pi)\in\gamma_w$, it has write-like flow, while
$(\psi,\pi)\in\gamma_r$ means it has read-like flow.  The derivation
of the two sets of flow related events follows.

For class~$\psi$, the set of compatible permissions is declared in the
policy file with the following two syntactic forms.
%
\[
\begin{array}{c}
\texttt{common }\phi~\{~\pi^{+}~\}\\
\texttt{class }\psi~[~\texttt{inherits }\phi~]^{?}~\{~\pi^{+}~\}\\
\end{array}
\]
%
If the \texttt{class} statement does not include an \texttt{inherits}
phrase, the set of compatible permissions is just the ones listed
between the curly braces, otherwise, the permissions in the
\texttt{common} statement named~$\phi$ are also included.

In the {\selinux} file that describes the direction of information
flow, the relevant statements appear in the following two syntactic
forms.
%
\[
\begin{array}{c}
\texttt{common }\phi~\{~F^{+}~\}\\
\texttt{class }\psi~\{~F^{+}~\}
\end{array}
\]
where $F$ associates a flow direction with a permission~$\pi$.
\begin{eqnarray*}
F&::=&\pi : E.\\
E&::=&\texttt{none} \alts D \alts \{ D \}\alts \{ D , D \}.\\
D&::=&\texttt{read} \alts \texttt{write}.
\end{eqnarray*}
%

As a write-like flow formula, the \texttt{class} statement of a class
that was declared without an \texttt{inherits} phrase in the policy
file means:
\[
\begin{array}{c}
\gamma_w\means{\texttt{class }\psi~\{~F^{+}~\}} ={} \\
\qquad c=\psi\land p\in\{\pi_1,\ldots,\pi_n\}.
\end{array}
\]
where $\{\pi_1,\ldots,\pi_n\}$ is the set of permissions declared to
be write-like in the body of the \texttt{class} statement.  For a
class declared with an \texttt{inherits} phrase, the write-like
permissions in its associated \texttt{common} statement are also
included.  The formula~$\gamma_w$ is the disjunction of the write-like
meaning of every \texttt{class} statement in the file.

The direction-flow file contains only a simple approximation.  It does
not take into account indirect flows caused by error conditions or
variations in timing, and it does not consider flow into other system
resources besides the process requesting the event and the resource
against which the event is requested.  This is why our analysis avoids
the subtleties of covert channels.

Information flows from an entity with security context $(t, r, u)$ to
$(t',r',u')$ if an event $(c,p)$ has write-like flow and
\[
\alpha_t\wedge\alpha_r\wedge
\beta_r\wedge\beta_u\wedge\tilde\beta_r\wedge\tilde\beta_u\wedge
\chi.
\]

When event $(c,p)$ has read-like flow, information flows from an
entity with security context $(t, r, u)$ to $(t',r',u')$ if
\[
\tilde\alpha_t\wedge\tilde\alpha_r\wedge
\tilde\beta_r\wedge\tilde\beta_u\wedge\beta_r\wedge\beta_u\wedge
\tilde\chi.
\]

The information flow transition relation formula $\delta$ is the
disjunction of the previous two formulas.
\[
\begin{array}{l}
\beta_r\wedge\beta_u\wedge\tilde\beta_r\wedge\tilde\beta_u\\
{}\land
(\begin{array}[t]{@{}l}(\gamma_w\wedge\alpha_t\wedge\alpha_r\wedge\chi)
\\
{}\lor
(\gamma_r\wedge
\tilde\alpha_t\wedge\tilde\alpha_r\wedge \tilde\chi))
\end{array}
\end{array}
\]

The initial states of the information flow policy are the ones that
are compatible with $\beta_r$ and $\beta_u$ so that
%
  \[ \sigma=\beta_r\land\beta_u. \]
%

Inspecting $\delta$ and $\sigma$ leads to the conclusion that every
reachable state is an initial state.

\section{Information Flow Diagrams}

Some information flow policy goals stipulate which sequences of causal
interactions are permissible.  It is easy to visualize these causal
chains using something we call information flow diagrams.

There are four kinds of freedom in constructing the chains.  First, we
can define what security contexts appear at a stage
in the process; we refer to these sets by symbols such as $\sigma_i$.
Second, we may characterize what events may occur at a
particular stage; we refer to these sets by symbols such as
$\gamma_i$.  Third, we may be interested in the consequence of a
single event, or a sequence of iterated events.  We indicate these by
decorating $\gamma_i$ by a superscript $1$ or $+$, respectively.  Let
$\lambda_i$ be a label of one of the forms $\gamma_i^1$ or
$\gamma_i^+$.  Finally, we may specify exceptional security contexts,
$\sigma_e$, or exceptional events, $\gamma_e$, that
should be ignored by the assertion--a concept to be made precise
later.  Then we can notate an information flow policy goal in the form:
%
\begin{equation}
\sigma_0\stackrel{\lambda_0}{\longrightarrow}\sigma_1
\stackrel{\lambda_1}{\longrightarrow}\cdots
\stackrel{\lambda_{n-2}}{\longrightarrow}
\sigma_{n-1}
\stackrel{\lambda_{n-1}}{\longrightarrow}\sigma_n\quad[\sigma_e;\gamma_e]
\label{eqn:diagram}
\end{equation}
%
An assertion of an information flow policy in the above form is called
an \emph{information flow diagram}.

We interpret this information flow policy as an assertion about all
paths from $\sigma_0$ to $\sigma_n$.  It asserts that this path must
encounter the $\sigma_i$ in the order given, executing events from
$\lambda_i$ in each stage, and that there must be just one such event
if the decoration is 1 and may be more events if the decoration is
$+$.  Additionally, any path that visits any exceptional security
contexts in $\sigma_e$ before getting to $\sigma_n$, or gets there via
the exceptional events in $\gamma_e$, does not violate the assertion.

An information flow diagram prohibits paths that contain certain
prefixes.  An information flow policy satisfies the information flow
policy goal expressed as an information flow diagram if the
information flow policy allows no prohibited paths.  The paths
prohibited by an information flow diagram of length~$n$ all must meet
at least the following assertions:
%
\begin{equation}
\begin{array}{ll}
s_m\in\sigma_n,\quad&\mbox{for some $m$,}\\
s_j\in\sigma_0,\quad&\mbox{for some $j<m$,}\\
s_k\notin\sigma_e,\quad&\mbox{for all $j\leq k<m$, and}\\
g_k\notin\gamma_e,\quad&\mbox{for all $j\leq k<m$.}
\end{array}
\label{eqn:hypothesis}
\end{equation}

\subsection{Order Assertions}

One form of path prohibited by an information flow diagram is one that visits
states in the wrong order.  A path satisfying
Eqn.~\ref{eqn:hypothesis} is prohibited if there exists an~$i<n$ such
that the path visits a state in $\sigma_{i+1}$ without having
previously visited a state in~$\sigma_i$.  In other words, let
$s_m\in\sigma_n$ and $s_j\in\sigma_0$.  A path is prohibited if there
is some~$k$ with $j\leq k\leq m$, that satisfies: \begin{equation}
s_k\in\sigma_{i+1}\land s_\ell\notin\sigma_i\mbox{ for all
$j\leq\ell<k$.}  \label{eqn:order} \end{equation}

\subsection{Event Assertions}

The other form of path prohibited by an information flow diagram is one that
wanders from its bounds.  A path satisfying Eqn.~\ref{eqn:hypothesis} is
prohibited if having reached a state in $\sigma_i$, the path fails to
reach a state in $\sigma_{i+1}$ using events in $\gamma_i$.

Let $\Theta_{i,j}$ be the assertion that a path satisfying
Eqn.~\ref{eqn:hypothesis} properly reaches $\sigma_i$ at step~$j$.
The assertion $\Theta_{i,j}$ is false whenever $j>m$.
The assertion $\Theta_{0,j}$ is true when~$s_j\in\sigma_0$.
Assertion $\Theta_{i+1,j'}$ is true when
$$\Theta_{i,j}\land g_j\in\gamma_i
\land g_k\in\gamma_i
\land s_k\notin\sigma_{i+1}
\land s_{j'}\in\sigma_{i+1},$$
for all $k$ with $j< k<j'$.
When $\lambda_i=\gamma^1_i$, i.e, the single event case,
$j'=j+1$.

A path at step $j$ wanders at $\sigma_i$ in a single step event
($\lambda_i=\gamma^1_i$) if
\begin{equation}
\Theta_{i,j}\land(j\geq m\lor g_j\notin\gamma_i\lor
s_{j+1}\notin\sigma_{i+i}).
\label{eqn:follow single}
\end{equation}

A path at step $j$ wanders at $\sigma_i$ in a multiple step event
($\lambda_i=\gamma^+_i$) if $\Theta_{i,j}$ and
\begin{equation}
\begin{array}{ll}
s_\ell\notin\sigma_{i+1}\quad&\mbox{for all $j<\ell\leq m$, or}\\
g_k\notin\gamma_i\quad&\mbox{while $s_\ell\notin\sigma_{i+1}$,}
\end{array}
\label{eqn:follow multiple}
\end{equation}
for some $k$ and all $\ell$ such that $j<\ell\leq k+1\leq m$.

\section{Model Checking}

Model checking is used to automatically show that an information flow
policy satisfies an information flow policy goal stated as an
information flow diagram.  This section explains how an information
flow policy is stated in the formalisms used by model checkers.

Following~\cite{ClarkeEtAl01}, we derive a Kripke structure from the
first order formulas $\initstate$ and~$\transit$ that represent an
information flow policy $(S,G,\delta,\sigma)$.

There are six forms of atomic propositions--one form for each of the
six system variables, $t$, $r$, $u$, $c$, $p$, and $k$.  The first
five forms are identical to the ones defined at the end of
Section~\ref{sec:policy}.  The system variable $k$ ranges over boolean
values.  When $k$ is asserted to be false, the atomic proposition is
$\lnot k$, and when true, the atomic proposition is written simply as
$k$.  The boolean system variable~$k$ is used to construct a Kripke
structure with a transition relation that is total.  It asserts that a
state is okay.

The formula $\initstate$ is $k\Rightarrow\sigma$.  The formula
$\transit$ is $k'\Leftrightarrow k\land\delta$.

A Kripke structure can be derived from $\initstate$ and $\transit$ as
follows.  The set of states is $T\times R\times U\times C\times
P\times B$, where $B$ is the set of boolean values.

The formula $\initstate$ implies that the initial state of the Kripke
structure contains members of $\sigma$ when $k$ is true.  It has all
members of $S$ when $k$ is false.

The formula $\transit$ implies that the transition relation of the
Kripke structure is total.  Whenever $k$ is false, any transition is
allowed as long as $k'$ is false.  Whenever $k$ is true, the relation
allows a transition when $(s,g,s')\in \delta$ and $k'$ is true, and
allows a transition when $(s,g,s')\notin \delta$ and $k'$ is false.
Clearly, this transition relation is total.  Additionally,
$k'\Rightarrow k$, that is, $k$ is true in the next state only if it
is in the current state.

The labeling function of the Kripke structure is obvious from this
construction.

Inspecting $\initstate$ and $\transit$ leads to the conclusion that
every reachable state is an initial state.

\section{Diagrams as CTL Assertions}

We translate the semantics of an instance of an information flow
diagram into assertions in Computational Tree Logic
(CTL)~\cite[Ch.~3]{ClarkeEtAl01}.  Because all reachable states are
initial states, assertions of interest assume the initial state of a
path is in~$\sigma_0$.  Had the Kripke structure not had this
property, assertions would have had to be asserted globally using the
$\ctlag$ operator.

\subsection{Order Assertions}
The first set of assertions states that if we move to
$\sigma_n$ from $\sigma_0$, we visit all intermediate $\sigma_i$ in
the appropriate order:
\iffalse
%
\begin{equation}
\lnot(\sigma_0\land\ctle[\lnot\hat\sigma_i
\ctlu(\sigma_{i+1}\land\ctle[\lnot(\sigma_e\lor\gamma_e)\ctlu\sigma_n\land
k])]),
\label{eqn:order ctl}
\end{equation}
where $1\leq i<n$, and
$\hat\sigma_i=\sigma_i\lor\sigma_e\lor\gamma_e$.
%
\begin{equation}
\sigma_0\Rightarrow\lnot\ctle[\lnot\hat\sigma_i
\ctlu(\sigma_{i+1}\land\ctle[\lnot(\sigma_e\lor\gamma_e)\ctlu\sigma_n\land
k])],
\label{eqn:order ctl}
\end{equation}
where $1\leq i<n$, and
$\hat\sigma_i=\sigma_i\lor\sigma_e\lor\gamma_e$.
\fi
%
\begin{equation}
\sigma_0\Rightarrow\ctla[\hat\sigma_i
\ctlr(\sigma_{i+1}\Rightarrow\ctla[\sigma_e\lor\gamma_e
\ctlr\lnot(\sigma_n\land k)])],
\label{eqn:order ctl}
\end{equation}
where $1\leq i<n$, and
$\hat\sigma_i=\sigma_i\lor\sigma_e\lor\gamma_e$.

To understand these assertions, consider what happens when one fails.
When assertion~$i$ fails, the following is true:
%
\begin{displaymath}
\sigma_0\land\ctle[\lnot\hat\sigma_i
\ctlu(\sigma_{i+1}\land\ctle[\lnot(\sigma_e\lor\gamma_e)\ctlu\sigma_n\land
k])].
\end{displaymath}

In words, the assertion says that there is some path from an initial
state in $\sigma_0$, that reaches a part of $\sigma_{i+1}$
that eventually leads to $\sigma_n$ without visiting an exception, and
between $\sigma_0$ and $\sigma_{i+1}$ avoids security contents in
$\sigma_i\lor\sigma_e$, and events in $\gamma_e$.  The properties of
the transition relation ensure that the prefix of the path that ends
in a state denoted by $\sigma_n$ contains only states in which $k$ is
true.

\subsection{Event Assertions}

The second set of assertions states that a causal chain from
$\sigma_0$ to $\sigma_n$ uses acceptable events at each step.  It
uses events in $\gamma_0$ until a state in $\sigma_1$ is reached, and
then uses events in $\gamma_1$ until a state in $\sigma_2$ is reached,
and so forth.

The set of assertions is given by recurrence relations.
\begin{equation}
\lnot f^i_0,\qquad 0\leq i<n,
\label{eqn:follow ctl}
\end{equation}
where for $j<i$, let
$\hat\gamma_i=\gamma_i\land\lnot\sigma_e\land\lnot\gamma_e$ in
\begin{displaymath}
\begin{array}{ll}
f^i_j = \sigma_j\land\hat\gamma_j\land\ctlex f^i_{j+1},
&\mbox{if }\lambda_j=\gamma^1_j,\\
f^i_j = \sigma_j\land\hat\gamma_j\land\ctlex\ctle[\hat\gamma_j\ctlu f^i_{j+1}],
&\mbox{if }\lambda_j=\gamma^+_j,
\end{array}
\end{displaymath}
and
\begin{displaymath}
f^i_i=\sigma_i\land(\lnot\gamma_i\land
g\lor\hat\gamma_i\land\ctlex h_i),
\end{displaymath}
where
\begin{displaymath}
g=\ctle[\lnot(\sigma_e\lor\gamma_e)\ctlu\sigma_n\land k],
\end{displaymath}
and when $\lambda_i=\gamma^1_i$,
\begin{displaymath}
h_i=\lnot\sigma_{i+i}\land g,
\end{displaymath}
and when $\lambda_i=\gamma^+_i$,
\begin{displaymath}
h_i=\ctle[\lnot\hat\sigma_{i+1}\ctlu
\lnot\gamma_i\land\lnot\sigma_{i+1}\land g].
\end{displaymath}

To understand the assertions defined by Eqn.~\ref{eqn:follow ctl},
consider what happens when one fails.  When assertion~$i$ fails,
$f^i_0$ is true.  In words, this assertion says that there is some
path that goes through $\sigma_0,\ldots,\sigma_i$ as prescribed by the
information flow diagram, however, something goes wrong after this
point.  Assertion $f^i_i$ states that after reaching $\sigma_i$, and
while avoiding $\sigma_{i+1}$, the path finds a state that leads to
$\sigma_n$ without visiting an exception.  This state does not have a
security context in $\sigma_{i+1}$.

If the CTL assertions in Eqns.~\ref{eqn:order ctl} and~\ref{eqn:follow
ctl} hold, then the information flow policy expressed in a diagram of
the form shown in Eqn.~\ref{eqn:diagram} is true.  These general forms
make security goal statements simple to produce: appropriate contexts,
classes, and permissions can simply be substituted for the variables
in Eqn.~\ref{eqn:diagram} as appropriate.

\section{Diagrams as LTL Assertions}

We translate the semantics of an instance of an information flow diagram
into assertions in Linear Temporal Logic
(LTL)~\cite[Ch.~3]{ClarkeEtAl01}.

\subsection{Order Assertions}
The first assertion states that if we move to $\sigma_n$ from
$\sigma_0$ along a non-exceptional path, a security context in
$\sigma_i$ occurs before the first occurrence of a security context in
$\sigma_{i+1}$:
%
\begin{equation}
\sigma_0
\land(\lnot\sigma_e\land\lnot\gamma_e)\ltlu(\sigma_n\land k)
\Rightarrow\bigwedge^{n-1}_{i=1}
\sigma_i\ltlr\lnot\sigma_{i+1}.
\label{eqn:order ltl}
\end{equation}

The operator $\ltlr$ (``releases'') asserts that its right hand
operand is true and remains true until its left hand operator has been
true at least once.  Thus, this formula asserts that each set
$\sigma_{i+1}$ is not encountered until after $\sigma_i$ has been
encountered, along paths from $\sigma_0$ to $\sigma_n$.

Here is another way to state the same thing.
%
\begin{displaymath}
\sigma_0\Rightarrow\hat\sigma_i\ltlr
(\sigma_{i+1}\Rightarrow(\sigma_e\lor\gamma_e)\ltlr
\lnot(\sigma_n\land k))
\end{displaymath}
where $1\leq i<n$, and
$\hat\sigma_i=\sigma_i\lor\sigma_e\lor\gamma_e$.

\subsection{Event Assertions}

The second assertion states that a causal chain from
$\sigma_0$ to $\sigma_n$ uses acceptable events at each step.  It
uses events in $\gamma_0$ until a state in $\sigma_1$ is reached, and
then uses events in $\gamma_1$ until a state in $\sigma_2$ is reached,
and so forth:
%
\begin{equation}
\begin{array}{l}
\sigma_0
\land(\lnot\sigma_e\land\lnot\gamma_e)\ltlu(\sigma_n\land k)\\
\qquad\Rightarrow\gamma_0
\ltlo_0(\sigma_1\land\gamma_1\ltlo_1(\sigma_2\ldots)).
\end{array}
\label{eqn:follow ltl}
\end{equation}
where $\gamma_i\ltlo_i f = \gamma_i\land\ltlx f$ for a single step
event ($\lambda_i=\gamma^1_i$), and $\gamma_i\ltlo_i f =
\gamma_i\land\ltlx (\gamma_i\ltlu f)$ for a multiple step event
($\lambda_i=\gamma^+_i$).

\bibliography{slatspec}
\bibliographystyle{plain}

\end{document}