This manual documents slat—the Security-Enhanced Linux Analysis Tools, version 2.0.
Copyright © 2003 The MITRE Corporation.
Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, this copyright notice and the title of the publication and its date appear, and notice in given that copying is by permission of The MITRE Corporation.
In January of 2001, the National Security Agency released a prototype version of a security-enhanced Linux system. Mandatory Access Control (MAC) security mechanisms were implemented, providing flexible support for a wide range of security policies. Both type enforcement and role-based access control components were incorporated into the access controls.
This document describes how to use the SELinux Analysis Tools (slat), which 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. We envision slat usage to be ongoing: whenever a system's policy configuration is modified, slat can be used to ensure continued enforcement of the pre-existing security goals.
The basic steps of slat usage are:
This manual assumes some knowledge of the SELinux system. In particular, we assume the reader is familiar with the following SELinux concepts: basic SELinux enforcement mechanism, policy file format, security contexts, and class, permission pairs. If you are unfamiliar with the basics of these concepts, please refer to “Configuring the SELinux Policy”, which is included in the SELinux distribution. The section titled “Flask Concepts” is particularly important.
After completing this overview, the manual explains the abstraction of SELinux access control used in slat analysis, and the source of the input on information flow. Next, we present the language used to describe information flow goals. Finally, we show how one uses slat to validate goals. The mathematical foundation of slat is described in another document included in the slat distribution.
Various slat programs are written in C and produce output that is known to work with the NuSMV model checker available at http://nusmv.irst.itc.it/.
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 complete.
Each check is labeled by a pair consisting of a class and a
permission. The class describes a kind of resource that the
access involves, such as file, process, or
filesystem. The permission describes the operation itself, such
as read, write, mount, or execute. We
call the pair an action. By a resource, we mean any
object in an SELinux system; processes, files, sockets, etc. are all
regarded as resources. Each resource has a security context which
summarizes its security relevant status.
In making a check, the security server receives as input two facts, the security contexts of the process and of another resource involved in the system call. A security context is a tuple consisting of three components, called a type, a role, and a 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 connect a collection of users with a corresponding collection of programs that they should be permitted to execute. Associated with the user component is a specification of the roles that user is permitted; the role then in turn specifies what types of processes those users are permitted to execute.
The most important component is the type, accounting for at least 22,000 out of the 22,500 access control statements in the sample policy file contained in one distribution. The type is used to specify the detailed interactions permitted between processes and other resources. For each system call, zero or more actions must be authorized; for each of these actions, the SELinux system will check that the type of the process is allowed to engage in this action against the type of some other resource involved in the system call. If any of these checks fails, then the system call will terminate before the kernel causes the corresponding change in system state.
For instance, in order to read a file, a process must be permitted to
engage in the file read action against it. However, the read
system call also causes an update to the attributes associated with
the file descriptor, indicating the current time as the last time of
file access. Thus, it must also be permitted to engage in the
fd setattr action.
Some actions (file write, for instance) transfer
information from process to resource, while others (file
read, for instance) transfer it from resource to process. The
slat permission mapping file, describes how each action transfers
information, whether like a read, like a write, in both directions, or
in neither. The slat program combines this information with
what it extracts from an SELinux policy file to produce an information
flow relation. For a given action, the information flow relation
specifies if the policy allows information to flow from the source
security context to the target security context.
The slat program encodes both an authorization relation and an information flow relation as a labeled transition system. A labeled transition system (lts) is a finite state machine with a label attached to each transition. Since most users will never need to look at the output of the slat program, first time readers can safely skip forward to the chapter on specifying policy goals (see Information Flow Goals).
To encode a relation, each security context is a state of the system, and each action is a label for transitions in the system. For an authorization relation, a transition from a source security context to a target security context with a given action as a label is part of the system if the authorization relation allows the action on the two contexts. For an information flow relation, a transition from a source security context to a target security context with a given action as a label is part of the system if the information flow relation says the action allows information to flow from the source to the target context.
The SELinux policy configuration file specifies that some combinations of user, role, and type values can never be used together. The initial state of the labeled transition system is a set of security contexts that excludes these combinations, and its transitions ensure the excluded states are never accessible.
This section concludes with a definition of the syntax used to describe labeled transition systems.
The form of a labeled transition system file is:
STATE t: set # Names of types
STATE r: set # Names of roles
STATE u: set # Names of users
ACTION c: set # Names of classes
ACTION p: set # Names of permissions
INIT
state # Initial state formula
TRANS
prop # Transition relation formula
SPEC
prop # A specification formula
SPEC
prop # Another specification formula
Each slat specification asserts that the transition formula implies the specification formula.
The syntax of the labeled transition system is given using Extended
bnf. Square brackets, [ and ], are used to group bnf
terminals and non-terminals, and are not part of the labeled
transition system syntax. The suffix * specifies zero or more
occurrences of its associated bnf term, the suffix + specifies
one or more occurrence, and the suffix ? specifies zero or one
occurrence of the term. Some of the non-terminals are also used to
define the syntax of diagrams used to state security policy goals;
see Diagram Syntax.
In the following, an atom is any sequence of characters that does not form a reserved word, such that the first character is in the set `a-zA-Z_$' and is followed by a possible empty sequence of characters belong to the set `a-zA-Z0-9_$'. Any string starting with the hash mark `#' and ending with a newline is a comment.
start ::= [ "STATE" atom ":" set ]+ [ "ACTION" atom ":" set ]*
"INIT" state "TRANS" prop [ "SPEC" prop ]*.
prop ::= "TRUE" | "FALSE"
| expr "=" expr | expr "!=" expr
| expr ":" set | expr "!:" set
| "!" prop | prop "&" prop | prop "|" prop
| prop "->" prop | prop "<->" prop | "(" prop ")".
state ::= prop -- restricted to state variables.
expr ::= atom | atom "'".
set ::= "{" [ atom [ "," atom ]+ ]? "}".
Additional syntactic rules follow.
' are state component
variables.
=, !=, :, or !: proposition must have a
variable on its left-hand-side.
=, !=, :, or !: proposition with
one variable must mention symbolic constants consistent with the
variable.
= or != proposition with two variables must equate a
state component variable with its next state component variable.
INIT formula must not reference an action component
variable or a next state component variable—a variable that ends with
'.
SPEC formula must be an implication in which the hypothesis
references no next state component variables and the conclusion
references no current state component variables.
t,
r, and u, and must be declared in that
order. Additionally, the action component variables are c and
p, and must be declared in that order.
The order of parsing precedence for operators from high to low is:
!, &, |, <->, ->.
All operators are left associative with the exception of implication `->', which is right associative.
The SELinux access control mechanisms provide strong and flexible means to achieve access control security goals such as confidentiality and integrity. Many security goals are naturally expressed in terms of information flow—generally, we wish to ensure that all paths through a system from some resource to another, go through a series of intermediate resources. Futhermore, we may also wish to specify the means by which one resource can transfer information to another.
slat analyzes paths in an SELinux system by analyzing the information flow relation derived from its policy configuration file and its multilevel security file. In this formalism, a security goal asserts that paths through the information flow relation from a starting security context to a final security context go through a chain of intermediate contexts. Additionally, it may specify the means by which a resource in one security context can affect another, in other words, it may restrict the transitions used by a path to ones labeled with designated class-permission pairs.
Security goals of this type are specified in a form that we call information flow diagrams, often shortened to diagrams. To aid in the analysis of such security goals, slat includes the program lts2smv. This command uses an information flow labeled transition system produced by the slat program, and a specification of a set of desired security goals to produce input for a model checker. When the output of lts2smv is given to a model checker, it produces a response about the satisfaction of the security goals. If the given policy does not satisfy the goals, it will also produce counterexamples.
In diagrams, simple formulas are used to specify sets of security
contexts and sets of actions. For security contexts, the only
variables that may occur in a formula are t, r, and
u. The variable t ranges over the types declared in the
SELinux policy configuration file, r over the roles, and
u over the users. For instance, the set of security contexts
that have user_t as their type component is given by the
following formula.
t = user_t
For actions, the only variables that may occur in a formula are
c, and p, where c ranges over the classes, and
p ranges over permisssions in the policy configuration file.
Formulas may be composed from other formulas using logical not
(!), and (&), and or (|). Parenthesis are used
for grouping. For instance, the singleton action of a file
write is given by the following formula.
c = file & p = write
The constant FALSE denotes the empty set, and TRUE
denotes the universal set.
Let x be one of the variables t, r, u,
c, or p, and i, j, and k be constants.
The following abreviations can be used in formulas.
x != i ==> !(x = i)
x : {i, j,..., k} ==> x = i | x = j | ... | x = k
x !: {i, j,..., k} ==> !(x : {i, j,..., k})
In the simplest form of diagram, the length of the chain it specifies
is the same as the number of actions in the diagram. Consider a
pictorial representation of a simple diagram of length n.
______ ______ ________ ______
| | a[0] | | a[1] a[n-2] | | a[n-1] | |
| s[0] | ===> | s[1] | ===> ... =====> | s[n-1] | =====> | s[n] |
|______| |______| |________| |______|
In this representation of a diagram, each box contains a security
context formula and each arrow is labeled with an action formula. The
diagram makes an assertion about all paths in the information flow
relation that contain a security context in s[0], and later,
contain a security context in s[n]. For the matching segment
of the path, the security context at the i-th transition must
be in s[i], and the action that labels the transition out must
be in a[i].
As text, the form used as input to the lts2smv program, the diagram above is written as follows.
[
s[0], a[0];
s[1], a[1];
...
s[n-1], a[n-1];
]
s[n];
The diagrams in the previous section specify, for each pair of
consecutive security contexts, that exactly one transition occurs.
Sometimes one wants to allow one or more transitions to occur as long
as each transition has the appropriate label. A multistep transition
is called an iterated action, and its action formula is
annotated in a diagram with a + suffix.
For example, if we would like to write down the assertion that flows
from some user contexts (where the context does not have any system
administrator privilege) to the type sshd_t always passes
through an intermediate security context with type sshd_tmp_t,
we write:
[
t=user_t & r=user_r & u!=jadmin, TRUE+;
t=sshd_tmp_t, c=process;
]
t=sshd_t;
Note the iterated actions are unrestricted due to the use of
TRUE, and the action formula c=process means that any
action with a class component of process is allowed. A
visualization of the diagram follows.
___________ ______________ __________
| | | | | |
| t=user_t& | TRUE+ | | c=process | |
| r=user_r& | ====> | t=sshd_tmp_t | ========> | t=sshd_t |
| u!=jadmin | | | | |
|___________| |______________| |__________|
For some security goals, one would like to designate some security
contexts, or some actions, as exceptional in the sense that any
path that uses them before it reaches the final security context is
deemed to meet the goal, no matter what happens afterward. If
s[n] is the final security context in the diagram,
s[e], the exceptional security contexts, and a[e] is
the exceptional actions, the textual representation of a diagram is:
[ ... ] s[n] [ s[e]; a[e] ];
For instance, suppose one knows that some contexts in
t=dpkt_t violate the goal expressed by a diagram. One can
check if other contexts violate the goal by making t=dpkt_t the
exceptional security contexts of the diagram.
When the exceptions are omitted from a diagram, it is treated as if the following was written.
[ ... ] s[n] [ FALSE; FALSE ];
The syntax of diagrams is given using Extended bnf. The specification
makes use of the conventions used to specify the syntax of labeled
transitions systems (see LTS Syntax), and also makes use of its
definition of the non-terminal prop.
start ::= diagram [ ";" diagram ]* ";"?.
diagram ::= "[" arrows? "]" state except?.
except ::= "[" state ";" action "]".
arrows ::= arrow [ ";" arrow ]* ";"?.
arrow ::= state "," action "+"?.
state ::= prop -- restricted to state variables.
action ::= prop -- restricted to action variables.
The program lts2smv converts a diagram into a set of
Computational Tree Logic (ctl) specifications that are validated
by a model checker. The details of the translation are beyond the
scope of this manual, however, the form of the translation needs to be
explained. For each diagram with n non-exceptional actions
specified, two types of ctl specifications are created, action
assertions and order assertions.
In total, there are n action assertions created. If a
counterexample is produced for the i-th action assertion, it
means there is a path to a final security context that matches the
security goal up to the i-th security context formula, but then
leaves via a prohibited action.
In total, there are n-1 order assertions created. If a
counterexample is produced for the i-th order assertion, it
means there is a path to a final security context that reaches a
security context in the i+1-th formula before it reaches a
security context in i-th formula.
One final note, the translation into smv model checker syntax
introduces a sixth variable k. The is variable is an artifact
of the translation and can safely be ignored.
Three programs are used to prepare input for a model checker–the programs apol2slat, slat, and lts2smv.
The apol2slat program translates an APOL style permission mapping file into a slat permission mapping file.
apol2slat apol_perm_mapping_ver18 > ver18.spm
where ver18.spm is the output file, and apol_perm_mapping_ver18 is the input.
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.
To generate an information flow labeled transition system, type:
$ slat -o flow.lts policy ver18.spm
where flow.lts is the output file, policy is the SELinux binary policy file, and ver18.spm is the slat permission mapping file.
To generate an smv model checker input file, type:
$ lts2smv -o diagram.smv flow.lts diagram.txt
where diagram.smv is the output file, flow.lts contains
the labeled transition system generated by slat, and
diagram.txt is a file containing one or more diagrams separated
by semicolons.
NuSMV can be used to check the information flow goal described by the diagrams using the command:
$ nice time NuSMV -f diagram.smv > diagram.log 2>&1
If NuSMV is not installed on your system, the package is available at http://nusmv.irst.itc.it/. Other model checkers that accept smv syntax may be substituted for NuSMV.
You can connect slat and lts2smv with a pipe via the command:
$ slat policy ver18.spm | lts2smv -o diagram.smv -- - diagram.txt
To see how a diagram translates into smv syntax without translating a labeled transition system, type:
$ lts2smv "" diagram.txt
We will now provide an example of slat usage. One goal for the
example SELinux policy included in the distribution is to restrict
access to raw disk data. The data is labeled with type
fixed_disk_device_t, and the type fsadm_t was created to
track which programs required access to the data. A reasonable security
goal, then, is to ensure that any information flowing into
fixed_disk_device_t has passed through the “gateway” type
fsadm_t first. This goal has the following intuitive picture:
_________ _________ _____________
| | | | | |
| start | ===> ... ===> | fsadm_t | ===> ... ===> | fixed_disk_ |
| context | | | | device_t |
|_________| |_________| |_____________|
Assume that this goal is specified in diagram format in the file disk.txt. With the following simple Makefile, to run slat one simply types make:
TARGETS = disk.log
POLICY = policy
LTS = ver18.lts
%.spm: %.apm
apol2slat $< > $@
%.lts: %.spm $(POLICY)
slat -o $@ $(POLICY) $<
%.smv: %.txt $(LTS)
lts2smv -o $@ $(LTS) $<
%.log: %.smv
nice time NuSMV -f $< > $@ 2>&1
all: $(TARGETS)
clean:
-rm $(LTS:.lts=.spm) $(LTS) $(TARGETS:.log=.smv) $(TARGETS)
.PRECIOUS: %.spm %.lts %.smv
The file disk.txt, containing the following diagram, asserts that
the only paths by which information flows from a standard user type into
the type fixed_disk_device_t contain the type fsadm_t as
an intermediary.
[
t=user_t & r=user_r & u!=jadmin, TRUE+;
t=fsadm_t, TRUE+;
]
t=fixed_disk_device_t;
The following is a transcript of the session:
$ make
apol2slat ver18.apm > ver18.spm
slat -o policy.lts policy ver18.spm
lts2smv -o disk.smv policy.lts disk.txt
nice time NuSMV -f disk.smv > disk.log 2>&1
$
The results of the NuSMV run are in the file disk.log. In this case, NuSMV finds a counterexample:
-- specification
!(t = user_t & r = user_r & u != jadmin_u
& E[t != fsadm_t U t = fixed_disk_device_t
& EF (k = TRUE & t = fixed_disk_device_t)])
is false
-- as demonstrated by the following execution sequence
-> State 1.1 <-
t = user_t
r = user_r
u = jdoe_u
c = netif_c
p = rawip_send_p
k = 1
-> State 1.2 <-
t = netif_ipsec2_t
r = object_r
p = udp_recv_p
-> State 1.3 <-
t = dpkg_t
r = system_r
u = system_u
c = fifo_file_c
p = append_p
-> State 1.4 <-
t = fixed_disk_device_t
r = object_r
u = jdoe_u
c = netif_c
p = accept_p
In this case, NuSMV found a counterexample to the assertion that
all paths which get to fixed_disk_device_t go through
fsadm_t first. To interpret the output of NuSMV, one can
easily construct a picture of the counterexample from the states
listed. A few notes on construction: Each state consists of a security
context (including the type t, the role r, and the user
u) and the next action (denoted by a class c, permission
p pair). If a variable does not appear in a state, it has not
changed from the previous state. The variable k is an internal
variable used by the model checker to indicate that the states are
valid, and can be ignored.
Given these guidelines, the counterexample given above corresponds to the existence of the following path in the system:
________ ________________ __________
| | | | | |
| user_t | netif_c | netif_ipsec2_t | netif_c | dpkg_t |
| user_r | rawip_send_p | object_r | udp_recv_p | system_r |
| jdoe_u | =========> | jdoe_u | =========> | system_u |
|________| |________________| |__________|
_____________________
| |
fifo_file_c | fixed_disk_device_t |
append_p | object_r |
=========> | jdoe_u |
|_____________________|
k, variable: Checking Diagramsk: Checking Diagrams