Unix Man page/Perldoc/Info page, English-Chinese Dictionary,
Chinese-English Dictionary
Unix Man page/Perldoc/Info page, English-Chinese Dictionary,
Chinese-English Dictionary
File: slat.info, Node: Top, Next: Introduction, Prev: (dir), Up: (dir)
SLAT User Manual
****************
This manual documents SLAT--the Security-Enhanced Linux Analysis Tools,
version 2.0.
Copyright (C) 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.
* Menu:
* Introduction:: What can SLAT do for you?
* SELinux Model:: A model for access control and information flow.
* Information Flow Goals:: Expressing policy goals.
* Invoking Slat Programs:: Validating information flow goals.
* Complete Example:: Complete example of validation usage.
* Index:: A concept index.
File: slat.info, Node: Introduction, Next: SELinux Model, Prev: Top, Up: Top
1 Introduction
**************
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:
* Locate system security configuration.
* Create information flow security goals.
* Analyze using SLAT.
* Examine output; for each goal, SLAT either validates it or
produces one or more counterexamples to its validity.
* When counterexamples exist, modify either security goals or policy
configuration (as appropriate) and iterate.
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/'.
File: slat.info, Node: SELinux Model, Next: Information Flow Goals, Prev: Introduction, Up: Top
2 SELinux Model
***************
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.
* Menu:
* The Information Flow Relation:: The Information Flow Abstraction.
* Labeled Transition Systems:: Representation of Relations.
File: slat.info, Node: The Information Flow Relation, Next: Labeled Transition Systems, Prev: SELinux Model, Up: SELinux Model
2.1 The Information Flow Relation
=================================
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.
File: slat.info, Node: Labeled Transition Systems, Prev: The Information Flow Relation, Up: SELinux Model
2.2 Labeled Transition Systems
==============================
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 (*note 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.
* Menu:
* LTS Form:: The Form of a Labeled Transition System.
* LTS Syntax:: The Details of the Syntax.
* LTS Operators:: Operator Precedence and Associativity.
File: slat.info, Node: LTS Form, Next: LTS Syntax, Prev: Labeled Transition Systems, Up: Labeled Transition Systems
2.2.1 LTS Form
--------------
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.
File: slat.info, Node: LTS Syntax, Next: LTS Operators, Prev: LTS Form, Up: Labeled Transition Systems
2.2.2 LTS Syntax
----------------
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; *note 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.
* An atom can be either a symbolic constant, a state component
variable, or an action component variable.
* The only atoms that can be followed by `'' are state component
variables.
* A set may not contain any variables.
* An `=', `!=', `:', or `!:' proposition must have a variable on its
left-hand-side.
* An `'`=', `!=', `:', or `!:' proposition with one variable must
mention symbolic constants consistent with the variable.
* An `=' or `!=' proposition with two variables must equate a state
component variable with its next state component variable.
* The `INIT' formula must not reference an action component variable
or a next state component variable--a variable that ends with `''.
* A `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.
* In this implementation, the state component variables are `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.
File: slat.info, Node: LTS Operators, Prev: LTS Syntax, Up: Labeled Transition Systems
2.2.3 Operator Precedence and Associativity
-------------------------------------------
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.
File: slat.info, Node: Information Flow Goals, Next: Invoking Slat Programs, Prev: SELinux Model, Up: Top
3 Information Flow Goals
************************
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.
* Menu:
* Formulas in Diagrams:: The syntax of formulas used in diagrams.
* Simple Diagrams:: Diagrams with single transition arrows.
* Iterated Actions:: Diagrams with multiple transition arrows.
* Exceptions:: Handling exceptional security contexts and actions.
* Diagram Syntax:: The Details of the Syntax.
* Checking Diagrams:: Model checking and validating diagrams.
File: slat.info, Node: Formulas in Diagrams, Next: Simple Diagrams, Prev: Information Flow Goals, Up: Information Flow Goals
3.1 Formulas in Diagrams
========================
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})
File: slat.info, Node: Simple Diagrams, Next: Iterated Actions, Prev: Formulas in Diagrams, Up: Information Flow Goals
3.2 Simple Diagrams
===================
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];
File: slat.info, Node: Iterated Actions, Next: Exceptions, Prev: Simple Diagrams, Up: Information Flow Goals
3.3 Iterated Actions
====================
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 | | | | |
|___________| |______________| |__________|
File: slat.info, Node: Exceptions, Next: Diagram Syntax, Prev: Iterated Actions, Up: Information Flow Goals
3.4 Exceptions
==============
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 ];
File: slat.info, Node: Diagram Syntax, Next: Checking Diagrams, Prev: Exceptions, Up: Information Flow Goals
3.5 Diagram Syntax
==================
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 (*note 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.
File: slat.info, Node: Checking Diagrams, Prev: Diagram Syntax, Up: Information Flow Goals
3.6 Checking Diagrams
=====================
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.
File: slat.info, Node: Invoking Slat Programs, Next: Complete Example, Prev: Information Flow Goals, Up: Top
4 Invoking Slat Programs
************************
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
File: slat.info, Node: Complete Example, Next: Index, Prev: Invoking Slat Programs, Up: Top
5 Complete Example
******************
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 |
|_____________________|
File: slat.info, Node: Index, Prev: Complete Example, Up: Top
Index
*****
[index]
* Menu:
* action formulas: Formulas in Diagrams. (line 6)
* action, class-permission pair: SELinux Model. (line 21)
* actions, exceptional: Exceptions. (line 6)
* actions, iterated: Iterated Actions. (line 6)
* atoms, syntax of: LTS Syntax. (line 15)
* class, resource kind: SELinux Model. (line 21)
* Computational Tree Logic: Checking Diagrams. (line 6)
* CTL: Checking Diagrams. (line 6)
* diagrams in SMV syntax: Invoking Slat Programs.
(line 44)
* exceptional actions: Exceptions. (line 6)
* exceptional security contexts: Exceptions. (line 6)
* flask concepts: Introduction. (line 45)
* formulas: Formulas in Diagrams. (line 6)
* formulas defining sets: Formulas in Diagrams. (line 6)
* information flow diagrams: Information Flow Goals.
(line 34)
* information flow relation: The Information Flow Relation.
(line 6)
* iterated actions: Iterated Actions. (line 6)
* k, variable: Checking Diagrams. (line 25)
* labeled transition systems: Labeled Transition Systems.
(line 6)
* LTS: Labeled Transition Systems.
(line 6)
* lts2smv, usage: Invoking Slat Programs.
(line 27)
* NuSMV <1>: Invoking Slat Programs.
(line 33)
* NuSMV: Introduction. (line 52)
* permission, resource operation kind: SELinux Model. (line 21)
* role, security context component: SELinux Model. (line 35)
* security context: SELinux Model. (line 35)
* security context formulas: Formulas in Diagrams. (line 6)
* security contexts, exceptional: Exceptions. (line 6)
* sets, formulas defining: Formulas in Diagrams. (line 6)
* sets, syntax of: LTS Syntax. (line 15)
* slat permission mapping: The Information Flow Relation.
(line 6)
* SMV, generation: Invoking Slat Programs.
(line 27)
* specification, labeled transition system: LTS Form. (line 30)
* syntax, arrow: Diagram Syntax. (line 6)
* syntax, atoms: LTS Syntax. (line 15)
* syntax, diagram: Diagram Syntax. (line 6)
* syntax, labeled transition system: LTS Form. (line 6)
* syntax, sets: LTS Syntax. (line 15)
* type, security context component: SELinux Model. (line 35)
* user, security context component: SELinux Model. (line 35)
* variable k: Checking Diagrams. (line 25)
|