Enforceable security policies.
A precise characterization is given for the class of security policies enforceable with mechanisms that work by monitoring system execution, and automata are introduced for specifying exactly that class of security policies. Techniques to enforce security policies specified by such automata are also discussed.
Introduction
A security policy defines execution that, for one reason or another, has been
deemed unacceptable. For example, a security policy might concern
access control, and restrict what operations principals can perform on
objects,
ffl information flow, and restrict what things principals can infer about
objects from observing other aspects of system behavior, or
ffl availability, and prohibit a principal from being denied use of a resource
as a result of execution by other principals.
Supported in part by ARPA/RADC grant F30602-96-1-0317 and AFOSR grant
F49620-94-1-0198. The views and conclusions contained herein are those of the author and
should not be interpreted as necessarily representing the official policies or endorsements,
either expressed or implied, of these organizations or the U.S. Government.
To date, general-purpose security policies, like those above, have attracted
most of the attention. But, application-dependent and special-purpose
security policies are increasingly important. A system to support
mobile code, like Java [5], might prevent information leakage by enforcing a
security policy that bars messages from being sent after files have been read.
To support electronic commerce, a security policy might prohibit executions
in which a customer pays for a service but the seller does not provide that
service. And finally, electronic storage and retrieval of intellectual property
is governed by complicated rights-management schemes that restrict not
only the use of stored materials but also the use of any derivatives [17].
The practicality of any security policy depends on whether that policy
is enforceable and at what cost. In this paper, we address those questions
for the class of enforcement mechanisms, which we call EM, that work by
monitoring a target system and terminating any execution that is about
to violate the security policy being enforced. Class EM includes security
kernels, reference monitors, and all other operating system and hardware-based
enforcement mechanisms that have appeared in the literature. Thus,
understanding what can and cannot be accomplished using mechanisms in
EM has value.
Excluded from EM are mechanisms that use more information than is
available from monitoring the execution of a target system. Therefore, compilers
and theorem-provers, which analyze a static representation of the
target system to deduce information about all of its possible executions, are
excluded from EM. The availability of information about all possible target
system executions gives power to an enforcement mechanism-just how
much power is an open question. Also excluded from EM are mechanisms
that modify a target system before executing it. Presumably the modified
target system would be "equivalent" to the original except that it satisfies
the security policy of interest; a definition for "equivalent" is needed in order
to analyze this class of mechanisms.
We proceed as follows. In x2, a precise characterization is given for security
policies that can be enforced using mechanisms in EM. An automata-based
formalism for specifying those security policies is the subject of x3.
Mechanisms in EM for enforcing security policies specified by automata
are described in x4. Next, x5 discusses some pragmatic issues related to
specifying and enforcing security policies as well as the application of our
enforcement mechanisms to safety-critical systems.
2 Characteristics of EM Enforcement Mechanisms
Formally, we represent executions by finite and infinite sequences, where \Psi
is the set of all possible such sequences. 1 Thus, a target system S defines
a subset \Sigma S of \Psi, and a security policy is a predicate on sets of executions.
Target system S satisfies security policy P if and only if P (\Sigma S ) equals true.
Notice that, for sets \Sigma and \Pi of executions, we do not require that if \Sigma
satisfies P and \Pi ae \Sigma holds, then \Pi satisfies P. Imposing such a requirement
on security policies would disqualify too many useful candidates. For
instance, the requirement would preclude information flow (as defined informally
in x1) from being considered a security policy-set \Psi of all executions
satisfies information flow, but a subset \Pi containing only those executions
in which the value of a variable x in each execution is correlated with the
value of y (say) does not. In particular, when an execution is known to be
in \Pi then the value of variable x reveals information about the value of y.
By definition, enforcement mechanisms in EM work by monitoring execution
of the target system. Thus, any security policy P that can be enforced
using a mechanism from EM must be equivalent to a predicate of the form
P is a predicate on executions. b
P formalizes the criteria used by the
enforcement mechanism for deciding to terminate an execution that would
otherwise violate the policy being enforced. In [1], a set of executions that
can be defined by checking each execution individually is called a property.
Using that terminology, we conclude from (1) that a security policy must
characterize sets that are properties in order for the policy to have an enforcement
mechanism in EM.
Not every security policy characterizes sets that are properties. Some
predicates on sets of executions cannot be put in form (1) because they
cannot be defined in terms of criteria that individual executions must each
satisfy in isolation. For example, the information flow policy discussed above
characterizes sets that are not properties (as is proved in [11]). Whether
information flows from x to y in a given execution depends, in part, on
what values y takes in other possible executions (and whether those values
are correlated with the value of x). A predicate to characterize such sets
of executions cannot be constructed only using predicates defined on single
executions.
1 The manner in which executions are represented is irrelevant here. Finite and infinite
sequences of atomic actions, of higher-level system steps, of program states, or of
state/action pairs are all plausible alternatives.
Enforcement mechanisms in EM cannot base decisions on possible future
execution, since that information is, by definition, not available to mechanisms
in EM. This further restricts what security policies can be enforced
by mechanisms from EM. In particular, consider security policy P of (1),
and suppose - is the prefix of some execution - 0 where b
enforcement mechanism for P must prohibit - even
though extension - 0 satisfies b
because otherwise execution of the target
system might terminate before - is extended into - 0 , and the enforcement
mechanism would then have failed to enforce P.
We can formalize this requirement as follows. For oe a finite or infinite
execution having i or more steps, and - a finite execution, let:
oe[::i] denote the prefix of oe involving its first i steps
- oe denote execution - followed by execution oe
and define \Pi \Gamma to be the set of all finite prefixes of elements in set \Pi. Then,
the above requirement concerning execution prefixes violating b
policy P defined by (1), is:
P(- oe))) (2)
Finally, note that any execution rejected by an enforcement mechanism
must be rejected after a finite period. This is formalized by:
policies satisfying (2) and (3) are satisfied by sets that are safety
properties [7], the class of properties that stipulate no "bad thing" happens
during an execution. Formally, a property S is defined [8] to be a safety
property if and only if for any finite or infinite execution oe,
oe
holds. This means that S is a safety property if and only if S is characterized
by a set of finite executions that are excluded and, therefore, the prefix of
no execution in S . Clearly, a security policy P satisfying (2) and (3) has
such a set of finite prefixes-the set of prefixes - 2 \Psi \Gamma such that : b
holds-so P is satisfied by sets that are safety properties according to (4).
Our analysis of enforcement mechanisms in EM has established:
Unenforceable Security Policy: If the sets of executions characterized
by a security policy P are not safety properties, then an enforcement
mechanism from EM does not exist for P.
Obviously, the contrapositive holds as well: all EM enforcement mechanisms
enforce safety properties. But, as discussed in x4, the converse-that all
safety properties have EM enforcement mechanisms-does not hold.
Revisiting the three application-independent security policies described
in x1, we find:
ffl Access control defines safety properties. The set of proscribed partial
executions contains those partial executions ending with an unacceptable
operation being invoked.
ffl Information flow does not define sets that are properties (as argued
above), so it does not define sets that are safety properties. Not being
safety properties, there are no enforcement mechanisms in EM for
exactly this policy. 2
ffl Availability defines sets that are properties but not safety properties.
In particular, any partial execution can be extended in a way that allows
a principal to access a resource, so availability lacks a defining set
of proscribed partial executions that every safety property must have.
Thus, there are no enforcement mechanisms in EM for availability-at
least as that policy is defined in x1. 3
3 Security Automata
Enforcement mechanisms in EM work by terminating any target-system
execution after seeing a finite prefix oe such that : b
P(oe) holds, for some
predicate b
defined by the policy being enforced. We established in x2 that
the set of executions satisfying b
also must be a safety property. Those
being the only constraints on b
P , we conclude that recognizers for sets of
2 Mechanisms from EM purporting to prevent information flow do so by enforcing a
security policy that implies, but is not equivalent to, the absence of information flow.
Given security policies P and Q for which P ) Q holds, a mechanism that enforces
does suffice for enforcing Q. And, there do exist security policies that both imply
restrictions on information flow and define sets that are safety properties. However, a
policy P that implies Q might rule out executions that do not violate Q, so using the
stronger policy is not without adverse consequences.
3 There are alternative formulations of availability that do characterize sets that are
safety properties. An example is "one principal cannot be denied use of a resource for
more than D steps as a result of execution by other principals". Here, the defining set of
partial executions contains intervals that exceed D steps and during which a principal is
denied use of a resource.
FileRead
not FileRead not Send

Figure

1: No Send after F ileRead
executions that are safety properties can serve as the basis for enforcement
mechanisms in EM.
A class of automata for recognizing safety properties is defined (but not
named) in [2]. We shall refer to these recognizers as security automata; they
are similar to ordinary non-deterministic finite-state automata [6]. Formally,
a security automaton is defined by:
- a (finite) set Q of automaton states,
- a set Q 0
' Q of initial automaton states,
- a (countable) set I of input symbols, and
- a transition function,
I is dictated by the security policy being enforced; the symbols in I might
correspond to system states, atomic actions, higher-level actions of the sys-
tem, or state/action pairs. In addition, the symbols of I might also have to
encode information about the past-for some safety properties, the transition
function will require that information.
To process a sequence s 1 of input symbols, the automaton starts
with its current state set equal to Q 0
and reads the sequence, one symbol at
a time. As each symbol s i is read, the automaton changes its current state
set Q 0 to the set Q 00 of automaton states, where
If ever Q 00 is empty, the input is rejected; otherwise the input is accepted.
Notice that this acceptance criterion means that a security automaton can
accept sequences that have infinite length as well as those having finite
length.
A(prin, obj, oper)

Figure

2: Access Control

Figure

1 depicts a security automaton for a security policy that prohibits
execution of Send operations after a F ileRead has been executed. The
automaton's states are represented by the two nodes labeled q nfr
(for "no
file read" ) and q fr (for "file read"). Initial states of the automaton are
represented in the figure by unlabeled incoming edges, so automaton state
is the only initial automaton state. In the figure, transition function
is specified in terms of edges labeled by transition predicates, which are
Boolean-valued effectively computable total functions with domain I. Let
ij denote the predicate that labels the edge from node q i to node q j . Then,
the security automaton, upon reading an input symbol s when Q 0 is the
current state set, changes its current state set to
In

Figure

transition predicate not FileRead is assumed to be satisfied
by system execution steps that are not file read operations, and transition
predicate not Send is assumed to be satisfied by system execution steps that
are not message-send operations. Since no transition is defined from q fr
for
input symbols corresponding to message-send execution steps, the security
automaton if Figure 1 rejects inputs in which a message is sent after a file
is read.
Another example of a security automaton is given in Figure 2. Different
instantiations for transition predicate A(prin; obj; oper) allow this automaton
to specify either discretionary access control [9] or mandatory access
control [3].
Discretionary Access Control. This policy prohibits operations according
to an access control matrix. Specifically, given access control matrix
M , a principal P rin is permitted by the policy to execute an
operation Oper involving object Obj only if Oper 2 M [P rin; Obj]
holds.
To specify this policy using the automaton of Figure 2, transition
predicate A(prin; obj; oper) would be instantiated by:
Mandatory Access Control. This policy prohibits execution of operations
according to a partially ordered set of security labels that are
associated with system objects. Information in objects assigned higher
labels is not permitted to be read and then stored into objects assigned
lower labels.
For example, a system's objects might be assigned labels from the set
ftopsecret; secret; sensitive; unclassifiedg
ordered according to:
topsecret - secret - sensitive - unclassified
Suppose two system operations are supported-read and write. A
mandatory access control policy might restrict execution of these operations
according to:
(i) a principal p with label -(p) is permitted to execute read(F ),
which reads a file F with label -(F ), only if -(p) -(F ) holds.
(ii) a principal p with label -(p) is permitted to execute write(F ),
which writes a file F with label -(F ), only if -(F ) -(p) holds.
To specify this policy using the automaton of Figure 2, transition
predicate A(prin; obj; oper) is instantiated by:
As a final illustration of security automata, we turn to electronic com-
merce. We might, for example, desire that a service-provider be prevented
from engaging in actions other than delivering the service for which a customer
has paid. This requirement is a security policy; it can be formalized in
terms of the following predicates, if executions are represented as sequences
of operations:
not pay(C)

Figure

3: Security automaton for fair transaction
customer C requests and pays for service
customer C is rendered service
The security policy of interest proscribes executions in which the service-provider
executes an operation that does not satisfy serve(C) after having
engaged in operation that satisfies pay(C). A security automaton for this
policy is given in Figure 3.
Notice, the security automaton of Figure 3 does not stipulate that payment
guarantees service. The security policy it specifies only limits what
the service-provider can do once a customer has made payment. In partic-
ular, the security policy that is specified allows a service-provider to stop
executing (i.e. stop producing input symbols) rather than rendering a paid-
for service. We do not impose the stronger security policy that service be
guaranteed after payment because that is not a safety property-there is
no defining set of proscribed partial executions-and therefore, according to
x2, it is not enforceable using a mechanism from EM.
4 Using Security Automata for Enforcement
Any security automaton can serve as the basis for an enforcement mechanism
in class EM, as follows. Each step the target system will next take
is represented by an input symbol and sent to an implementation of the
security automaton.
(i) If the automaton can make a transition on that input symbol, then
the target system is allowed to perform that step and the automaton
state is changed according to its transition predicates.
(ii) If the automaton cannot make a transition on that input symbol, then
the target system is terminated.
In fact, any security policy enforceable using a mechanism from EM can
be enforced using such a security-automaton implementation. This is because
all safety properties have specifications as security automata, and Unenforceable
Security Policy of x2 implies that EM enforcement mechanisms
enforce safety properties. Consequently, by understanding the limitations
of security-automata enforcement mechanisms, we can gain insight into the
limitations of all enforcement mechanisms in class EM.
Implicit in (ii) is the assumption that the target system can be terminated
by the enforcement mechanism. Specifically, we assume that the
enforcement mechanism has sufficient control over the target system to stop
further automaton input symbols from being produced. This control requirement
is subtle and makes certain security policies-even though they characterize
sets that are safety properties-unenforceable using mechanisms from
EM.
For example, consider the following variation on availability of x1:
Real-Time Availability: One principal cannot be denied use of a resource
for more than D seconds.
Sets satisfying Real-Time Availability are safety properties-the "bad thing"
is an interval of execution spanning more than D seconds during which some
principal is denied the resource. The input symbols of a security automaton
for Real-Time Availability must therefore encode time. However, the
passage of time cannot be stopped, so a target system with real-time clocks
cannot be prevented from continuing to produce input symbols. Real-Time
Availability simply cannot be enforced using one of our automata-based enforcement
mechanisms, because target systems lack the necessary controls.
And, since the other mechanisms in EM are no more powerful, we conclude
that Real-Time Availability cannot be enforced using any mechanism in EM.
Two mechanisms are involved in our security-automaton implementation
of an enforcement mechanism.
Automaton Input Read: A mechanism to determine that an input symbol
has been produced by the target system and then to forward that
symbol to the security automaton.
Automaton Transition: A mechanism to determine whether the security
automaton can make a transition on a given input and then to perform
that transition.
Their aggregate cost can be quite high. For example, when the automaton's
input symbols are the set of program states and its transition predicates
are arbitrary state predicates, a new input symbol is produced for each
machine-language instruction that the target system executes. The enforcement
mechanism must be invoked before every target-system instruction.
However, for security policies where the target system's production of
input symbols coincides with occurrences of hardware traps, our automata-based
enforcement mechanism can be supported quite cheaply by incorporating
it into the trap-handler. One example is implementing an enforcement
mechanism for access control policies on system-supported objects, like files.
Here, the target system's production of input symbols coincides with invocations
of system operations, hence the production of input symbols coincides
with occurrences of system-call traps.
A second example of exploiting hardware traps arises in implementing
memory protection. Memory protection implements discretionary access
control with operations read, write, and execute and an access control matrix
that tells how processes can access each region of memory. The security
automaton of Figure 2 specifies this security policy. Notice that this security
automaton expects an input symbol for each memory reference. But
most, if not all, of the these input symbols cause no change to the security
automaton's state. Input symbols that do not cause automaton state
transitions need not be forwarded to the automaton, and that justifies the
following optimization of Automaton Input Read:
Automaton Input Read Optimization: Input symbols are not forwarded
to the security automaton if the state of the automaton just after
the transition would be the same as it was before the transition.
Given this optimization, the production of automaton input symbols for
memory protection can be made to coincide with occurrences of traps.
The target system's memory-protection hardware-base/bounds registers
or page and segment tables-is initialized so that a trap occurs when an
input symbol should be forwarded to the memory protection automaton.
Memory references that do not cause traps never cause a state transition or
undefined transition by the automaton.
Inexpensive implementation of our automata-based enforcement mechanisms
is also possible when programs are executed by a software-implemented
virtual machine (sometimes known as a reference monitor). The virtual machine
instruction-processing cycle is augmented so that it produces input
symbols and makes automaton transitions, according to either an internal
or an externally specified security automaton. For example, the Java virtual
machine[10] could easily be augmented to implement the Automaton
Input Read and Automaton Transition mechanisms for input symbols that
correspond to method invocations.
Beyond Class EM Enforcement Mechanisms
The overhead of enforcement can sometimes be reduced by merging the
enforcement mechanism into the target system. One such scheme, which
has recently attracted attention, is software-based fault isolation (SFI), also
known as "sandboxing" [19, 16]. SFI implements memory protection, as
specified by a one-state automaton like that of Figure 2, but does so without
hardware assistance. Instead, a program is edited before it is executed, and
only such edited programs are run by the target system. (Usually, it is the
object code that is edited.) The edits insert instructions to check and/or
modify the values of operands, so that illegal memory references are never
attempted,
SFI is not in class EM because SFI involves modifying the target sys-
tem, and modifications are not permitted for enforcement mechanisms in
EM. But viewed in our framework, the inserted instructions for SFI can be
seen to implement Automaton Input Read by copying code for Automaton
Transition in-line before each target system instruction that produces an
input symbol. Notice that nothing prevents the SFI approach from being
used with multi-state automata, thereby enforcing any security policy that
can be specified as a security automaton. Moreover, a program optimizer
should be able to simplify the inserted code and eliminate useless portions 4
although this introduces a second type of program analysis to SFI and requires
putting further trust in automated program analysis tools.
Finally, there is no need for any run-time enforcement mechanism if
the target system can be analyzed and proved not to violate the security
policy of interest. This approach has been employed for a security policy like
what SFI was originally intended to address-a policy specified by one-state
security automata-in proof carrying code (PCC) [13]. With PCC, a proof
is supplied along with a program, and this proof comes in a form that can be
checked mechanically before running that program. The security policy will
not be violated if, before the program is executed, the accompanying proof is
checked and found to be correct. The original formulation of PCC required
that proofs be constructed by hand. This restriction can be relaxed. For
Ulfar Erlingsson of Cornell has implemented a system that does exactly this for the
Java virtual machine and for Intel x86 machine language.
certain security policies specified by one-state security automata, a compiler
can automatically produce PCC from programs written in high-level, type-safe
programming languages[12, 14].
To extend PCC for security policies that are specified by arbitrary security
automata, a method is needed to extract proof obligations for establishing
that a program satisfies the property given by such an automaton.
Such a method does exist-it is described in [2].
The utility of a formalism partly depends on the ease with which objects
of the formalism can be read and written. Users of the formalism must
be able to translate informal requirements into objects of the formalism.
With security automata, establishing the correspondence between transition
predicates and informal requirements on system behavior is crucial and can
require a detailed understanding of the target system. The automaton of

Figure

1, for example, only captures the informal requirement that messages
are not sent after a file is read if it is impossible to send a message unless
transition predicate Send is true and it is impossible to read a file unless
transition predicate F ileRead is true. There might be many ways to send
messages-some obvious and others buried deep within the bowels of the
target system. All must be identified and included in the definition of Send;
a similar obligation accompanies transition predicate F ileRead.
The general problem of establishing the correspondence between informal
requirements and some purported formalization of those requirements is not
new to software engineers. The usual solution is to analyze the formalization,
being alert to inconsistencies between the results of the analysis and the
informal requirements. We might use a formal logic to derive consequences
from the formalization; we might use partial evaluation to analyze what the
formalization implies about one or another scenario, a form of testing; or,
we might (manually or automatically) transform the formalization into a
prototype and observe its behavior in various scenarios.
Success with proving, testing, or prototyping as a way to gain confidence
in a formalization depends upon two things. The first is to decide
what aspects of a formalization to check, and this is largely independent of
the formalism. But the second, having the means to do those checks, not
only depends on the formalism but largely determines the usability of that
formalism. To do proving, we require a logic whose language includes the
formalism; to do testing, we require a means of evaluating a formalization
in one or another scenario; and to do prototyping, we must have some way
to transform a formalization into a computational form.
As it happens, a rich set of analytical tools does exist for security au-
tomata, because security automata are a class of Buchi automata [4], and
Buchi automata are widely used in computer-aided program verification
tools. Existing formal methods based either on model checking or on theorem
proving can be employed to analyze a security policy that has been
specified as a security automaton. And, testing or prototyping a security
policy that is specified by a security automaton is just a matter of running
the automaton.
Guidelines for Structuring Security Automata
Real system security policies are best given as collections of simpler policies,
a single large monolithic policy being difficult to comprehend. The system's
security policy is then the result of composing the simpler policies in the collection
by taking their conjunction. To employ such a separation of concerns
when security policies are specified by security automata, we must be able
to compose security automata in an analogous fashion. Given a collection of
security automata, we must be able to construct a single conjunction security
automaton for the conjunction of the security policies specified by the
automata in the collection. That construction is not difficult: An execution
is rejected by the conjunction security automaton if and only if it is rejected
by any automaton in the collection.
Beyond comprehensibility, there are other advantages to specifying system
security policies as collections of security automata. First, having a
collection allows different enforcement mechanisms to be used for the different
automata (hence the different security policies) in the collection. Second,
security policies specified by distinct automata can be enforced by distinct
system components, something that is attractive when all of some security
automaton's input symbols correspond to events at a single system compo-
nent. Benefits that accrue from having the source of all of an automaton's
input symbols be a single component include:
ffl Enforcement of a component's security policy involves trusting only
that component.
ffl The overhead of an enforcement mechanism is lower because communication
between components can be reduced.
For example, the security policy for a distributed system might be specified
by giving a separate security automaton for each system host. Then, each
host would itself implement Automaton Input Read and Automaton Transitions
mechanisms for only the security automata concerning that host.
The designer of a security automaton often must choose between encoding
security-relevant information in the target system's state and in an
automaton state. Larger automata are usually more complicated, hence
more difficult to understand, and often lead to more expensive enforcement
mechanisms. For example, our generalization of SFI involves modifying the
target system by inserting code and then employing a program optimizer
to simplify the result. The inserted code simulates the security automaton,
and the code for a smaller security automaton will be smaller, cheaper to
execute, and easier to optimize. Similarly, for our generalization of PCC,
proof obligations derived according to [2] are fewer and simpler if the security
automata is smaller.
However, we conjecture that the cost of executing a reference monitor
that implements Automaton Transition is probably insensitive to whether
security-relevant state information is stored in the target system or in automaton
states. This is because the predicates that must be evaluated in the
two implementations will differ only in whether a state component has been
associated with the security automaton or the target system, and the cost
of reading that state information and of evaluating the predicates should be
similar.
Application to Safety-Critical Systems
The idea that security kernels might have application in safety-critical systems
is eloquently justified in [15] and continues to interest researchers [18].
Safety-critical systems are concerned with enforcing properties that are
safety properties (in the sense of [8]), so it is natural to expect an enforcement
mechanism for safety properties to have application in this class of
systems. And, we see no impediments to using security automata or our
security-automata based enforcement mechanisms for enforcing safety properties
in safety-critical systems.
The justification given in [15] for using security kernels in safety-critical
systems involves a characterization of what types of properties can be enforced
by a security kernel. As do we in this paper, [15] concludes that safety
properties but not liveness properties are enforceable. However, the arguments
given in [15] are informal and are coupled to the semantics of kernel-supported
operations. The essential attributes of enforceability, which we
isolate and formalize by equations (1), (2), and (3), are neither identified
nor shown to imply that only safety properties can be enforced.
In addition, because [15] concerns kernelized systems, the notion of property
there is restricted to being sequences of kernel-provided functions. By
allowing security automata to have arbitrary sets of input symbols, our results
can be seen as generalizing those of [15]. And the generalization is a
useful one, because it applies to enforcement mechanisms that are not part of
a kernel. Thus, we can now extend the central thesis of [15], that kernelized
systems have application beyond implementing security policies, to justify
the use of enforcement mechanisms from EM when building safety-critical
systems.

Acknowledgments

I am grateful to Robbert van Renesse, Greg Morrisett, '
Ulfar Erlingsson,
Yaron Minsky, and Lidong Zhou for helpful feedback on the use and implementation
of security automata and for comments on previous drafts of
this paper. Helpful comments on an earlier draft of this paper were also
provided by Earl Boebert, Li Gong, Robert Grimm, Keith Marzullo, and
John Rushby. John McLean served as a valuable sounding board for these
ideas as I developed them. Feedback from Martin Abadi helped to sharpen
the formalism. And, the University of Tromso was a hospitable setting and
a compelling excuse for performing some of the work reported herein.



--R

Defining liveness.
Recognizing safety and liveness.
Secure computer systems: Mathematical foundations.

Java security: Present and near future.
Formal Languages and Their Relation to Automata.
Proving the correctness of multiprocess programs.
Logical Foundation.

The Java Virtual Machine Specification.
A general theory of composition for trace sets closed under selective interleaving functions.
From ML to typed assembly language.


Kernels for safety?
A tool for constructing safe extensible C
Letting Loose the Light: Igniting Commerce in Electronic Publication.
On the enforcement of software safety policies.
Efficient Software-Based Fault Isolation
--TR
A note on denial-of-service in operating systems
Distributed systems: methods and tools for specification. An advanced course
Verifying temporal properties without temporal logic
The DIAMOND security policy for object-oriented databases
Partial evaluation and automatic program generation
Efficient software-based fault isolation
Proof-carrying code
From system F to typed assembly language
The design and implementation of a certifying compiler
History-based access control for mobile code
SASI enforcement of security policies
Guarded commands, nondeterminacy and formal derivation of programs
Providing policy-neutral and transparent access control in extensible systems
Automata, Languages, and Machines
Java Virtual Machine Specification
Java Security
Authorization in Distributed Systems
A General Theory of Composition for Trace Sets Closed under Selective Interleaving Functions
A Logical Language for Expressing Authorizations

--CTR
James Ezick, Resolving and applying constraint queries on context-sensitive analyses, Proceedings of the ACM-SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, June 07-08, 2004, Washington DC, USA
Scott C.-H. Huang , Kia Makki , Niki Pissinou, On optimizing compatible security policies in wireless networks, EURASIP Journal on Wireless Communications and Networking, v.2006 n.2, p.71-71, April 2006
Alan Shieh , Dan Williams , Emin Gn Sirer , Fred B. Schneider, Nexus: a new operating system for trustworthy computing, Proceedings of the twentieth ACM symposium on Operating systems principles, October 23-26, 2005, Brighton, United Kingdom
Gary McGraw , Greg Morrisett, Attacking Malicious Code: A Report to the Infosec Research Council, IEEE Software, v.17 n.5, p.33-41, September 2000
Krzysztof M. Brzezinski , Norbert Malinski, Reference specification issues in on-line verification by passive testing, Proceedings of the 24th IASTED international conference on Parallel and distributed computing and networks, p.186-191, February 14-16, 2006, Innsbruck, Austria
Jacob Zimmermann , George Mohay, Distributed intrusion detection in clusters based on non-interference, Proceedings of the 2006 Australasian workshops on Grid computing and e-research, p.89-95, January 16-19, 2006, Hobart, Tasmania, Australia
Vir V. Phoha , Amit U. Nadgar , Asok Ray , Shashi Phoha, Supervisory Control of Software Systems, IEEE Transactions on Computers, v.53 n.9, p.1187-1199, September 2004
Dries Vanoverberghe , Frank Piessens, Supporting Security Monitor-Aware Development, Proceedings of the Third International Workshop on Software Engineering for Secure Systems, p.2, May 20-26, 2007
Massimo Bartoletti , Pierpaolo Degano , Gian Luigi Ferrari, Policy framings for access control, Proceedings of the 2005 workshop on Issues in the theory of security, p.5-11, January 10-11, 2005, Long Beach, California
R. Sekar , C. R. Ramakrishnan , I. V. Ramakrishnan , S. A. Smolka, Model-Carrying Code (MCC): a new paradigm for mobile-code security, Proceedings of the 2001 workshop on New security paradigms, September 10-13, 2001, Cloudcroft, New Mexico
Prasad Naldurg , Roy H. Campbell, Dynamic access control: preserving safety and trust for network defense operations, Proceedings of the eighth ACM symposium on Access control models and technologies, June 02-03, 2003, Como, Italy
J. J. Whitmore, A method for designing secure solutions, IBM Systems Journal, v.40 n.3, p.747-768, March 2001
Zaid Dwaikat , Francesco Parisi-Presicce, Risky trust: risk-based analysis of software systems, ACM SIGSOFT Software Engineering Notes, v.30 n.4, July 2005
Fabio Martinell , Ilaria Matteucci, Through Modeling to Synthesis of Security Automata, Electronic Notes in Theoretical Computer Science (ENTCS), 179, p.31-46, July, 2007
Arie Orlovsky , Danny Raz, Decentralized enforcement of security policies for distributed computational systems, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea
Shin Nakajima , Tetsuo Tamai, Formal specification and analysis of JAAS framework, Proceedings of the 2006 international workshop on Software engineering for secure systems, May 20-21, 2006, Shanghai, China
Dachuan Yu , Ajay Chander , Nayeem Islam , Igor Serikov, JavaScript instrumentation for browser security, ACM SIGPLAN Notices, v.42 n.1, January 2007
Lujo Bauer , Jay Ligatti , David Walker, Composing security policies with polymer, ACM SIGPLAN Notices, v.40 n.6, June 2005
Vijay V. Raghavan, Toward an integrative model of application-software security, Practicing software engineering in the 21st century, Idea Group Publishing, Hershey, PA,
Mark Reith , Jianwei Niu , William H. Winsborough, Engineering Trust Management into Software Models, Proceedings of the International Workshop on Modeling in Software Engineering, p.9, May 20-26, 2007
Franois Siewe , Antonio Cau , Hussein Zedan, A compositional framework for access control policies enforcement, Proceedings of the ACM workshop on Formal methods in security engineering, p.32-42, October 30, 2003, Washington, D.C.
Claudio Bettini , Sushil Jajodia , X. Sean Wang , Duminda Wijesekera, Provisions and obligations in policy management and security applications, Proceedings of the 28th international conference on Very Large Data Bases, p.502-513, August 20-23, 2002, Hong Kong, China
Galen C. Hunt , James R. Larus , David Tarditi , Ted Wobber, Broad new OS research: challenges and opportunities, Proceedings of the 10th conference on Hot Topics in Operating Systems, p.15-15, June 12-15, 2005, Santa Fe, NM
Douglas R. Smith, Requirement enforcement by transformation automata, Proceedings of the 6th workshop on Foundations of aspect-oriented languages, p.5-14, March 13-13, 2007, Vancouver, British Columbia, Canada
Frdric Besson , Thomas de Grenier de Latour , Thomas Jensen, Secure calling contexts for stack inspection, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.76-87, October 06-08, 2002, Pittsburgh, PA, USA
Panagiotis Manolios , Richard Trefler, A lattice-theoretic characterization of safety and liveness, Proceedings of the twenty-second annual symposium on Principles of distributed computing, p.325-333, July 13-16, 2003, Boston, Massachusetts
Joel Coburn , Srivaths Ravi , Anand Raghunathan , Srimat Chakradhar, SECA: security-enhanced communication architecture, Proceedings of the 2005 international conference on Compilers, architectures and synthesis for embedded systems, September 24-27, 2005, San Francisco, California, USA
David Wagner , Paolo Soto, Mimicry attacks on host-based intrusion detection systems, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA
Stephen McCamant , Michael D. Ernst, A simulation-based proof technique for dynamic information flow, Proceedings of the 2007 workshop on Programming languages and analysis for security, June 14-14, 2007, San Diego, California, USA
Fabio Martinelli , Ilaria Matteucci, An Approach for the Specification, Verification and Synthesis of Secure Systems, Electronic Notes in Theoretical Computer Science (ENTCS), 168, p.29-43, February, 2007
K. Altisen , F. Maraninchi , D. Stauch, Aspect-oriented programming for reactive systems: Larissa, a proposal in the synchronous framework, Science of Computer Programming, v.63 n.3, p.297-320, 15 December 2006
Anderson Santana de Oliveira, Rewriting-Based Access Control Policies, Electronic Notes in Theoretical Computer Science (ENTCS), v.171 n.4, p.59-72, July, 2007
Michael McDougall , Rajeev Alur , Carl A. Gunter, A model-based approach to integrating security policies for embedded devices, Proceedings of the 4th ACM international conference on Embedded software, September 27-29, 2004, Pisa, Italy
Martin Sulzmann , Rzvan Voicu, Language-Based Program Verification via Expressive Types, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.7, p.129-147, June, 2007
Anish Arora , Marvin Theimer, On modeling and tolerating incorrect software, Journal of High Speed Networks, v.14 n.2, p.109-134, April 2005
Christian Skalka, Trace effects and object orientation, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.139-150, July 11-13, 2005, Lisbon, Portugal
Arnab Ray, Security check: a formal yet practical framework for secure software architecture, Proceedings of the workshop on New security paradigms, August 18-21, 2003, Ascona, Switzerland
Patrick Cousot , Radhia Cousot, Systematic design of program transformation frameworks by abstract interpretation, ACM SIGPLAN Notices, v.37 n.1, p.178-190, Jan. 2002
Karl Krukow , Mogens Nielsen , Vladimiro Sassone, A framework for concrete reputation-systems with applications to history-based access control, Proceedings of the 12th ACM conference on Computer and communications security, November 07-11, 2005, Alexandria, VA, USA
Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Computability classes for enforcement mechanisms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.1, p.175-205, January 2006
Ian Welch , Robert J. Stroud, Using reflection as a mechanism for enforcing security policies on compiled code, Journal of Computer Security, v.10 n.4, p.399-432, December 2002
Tom Chothia , Dominic Duggan, Capability passing processes, Science of Computer Programming, v.66 n.3, p.184-204, May, 2007
James Rose , Nikhil Swamy , Michael Hicks, Dynamic inference of polymorphic lock types, Science of Computer Programming, v.58 n.3, p.366-383, December 2005
Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Certified In-lined Reference Monitoring on .NET, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada
Thomas Ball , Sriram K. Rajamani, The S
Ilaria Matteucci, Automated Synthesis of Enforcing Mechanisms for Security Properties in a Timed Setting, Electronic Notes in Theoretical Computer Science (ENTCS), 186, p.101-120, July, 2007
Trent Jaeger , Reiner Sailer , Yogesh Sreenivasan, Managing the risk of covert information flows in virtual machine systems, Proceedings of the 12th ACM symposium on Access control models and technologies, June 20-22, 2007, Sophia Antipolis, France
David Brumley , Dawn Song, Privtrans: automatically partitioning programs for privilege separation, Proceedings of the 13th conference on USENIX Security Symposium, p.5-5, August 09-13, 2004, San Diego, CA
Therrezinha Fernandes , Jules Desharnais, Describing data flow analysis techniques with Kleene algebra, Science of Computer Programming, v.65 n.2, p.173-194, March, 2007
F. Y. Huang , C. B. Jay , D. B. Skillicorn, Adaptiveness in well-typed Java bytecode verification, Proceedings of the 2006 conference of the Center for Advanced Studies on Collaborative research, October 16-19, 2006, Toronto, Ontario, Canada
Franois Pottier , Christian Skalka , Scott Smith, A systematic approach to static access control, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.344-382, March 2005
Shih-Chien Chou, Providing flexible access control to an information flow control model, Journal of Systems and Software, v.73 n.3, p.425-439, November-December 2004
R. Sekar , V.N. Venkatakrishnan , Samik Basu , Sandeep Bhatkar , Daniel C. DuVarney, Model-carrying code: a practical approach for safe execution of untrusted applications, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
Shih-Chien Chou , Chin-Yi Chang, An information flow control model for C applications based on access control lists, Journal of Systems and Software, v.78 n.1, p.84-100, October 2005
Ran Shaham , Eran Yahav , Elliot K. Kolodner , Mooly Sagiv, Establishing local temporal heap safety properties with applications to compile-time memory management, Science of Computer Programming, v.58 n.1-2, p.264-289, October 2005
David Basin , Ernst-Ruediger Olderog , Paul E. Sevinc, Specifying and analyzing security automata using CSP-OZ, Proceedings of the 2nd ACM symposium on Information, computer and communications security, March 20-22, 2007, Singapore
Charles E. Phillips, Jr. , T.C. Ting , Steven A. Demurjian, Information sharing and security in dynamic coalitions, Proceedings of the seventh ACM symposium on Access control models and technologies, June 03-04, 2002, Monterey, California, USA
Frdric Besson , Thomas De Grenier DeLatour , Thomas Jensen, Interfaces for stack inspection, Journal of Functional Programming, v.15 n.2, p.179-217, March 2005
Shih-Chien Chou, Embedding role-based access control model in object-oriented systems to protect privacy, Journal of Systems and Software, v.71 n.1-2, p.143-161, April 2004
Gianluigi Ferrari , Eugenio Moggi , Rosario Pugliese, MetaKlaim: a type safe multi-stage language for global computing, Mathematical Structures in Computer Science, v.14 n.3, p.367-395, June 2004
Steve Zdancewic , Lantian Zheng , Nathaniel Nystrom , Andrew C. Myers, Untrusted hosts and confidentiality: secure program partitioning, ACM SIGOPS Operating Systems Review, v.35 n.5, Dec. 2001
Philip W. L. Fong, Reasoning about safety properties in a JVM-like environment, Science of Computer Programming, v.67 n.2-3, p.278-300, July, 2007
Thomas Ball , Ella Bounimova , Byron Cook , Vladimir Levin , Jakob Lichtenberg , Con McGarvey , Bohus Ondrusek , Sriram K. Rajamani , Abdullah Ustuner, Thorough static analysis of device drivers, ACM SIGOPS Operating Systems Review, v.40 n.4, October 2006
Susan J. Chinburg , Ramesh Sharda , Mark Weiser, Establishing the business value of network security using analytical hierarchy process, Creating business value with information technology: challenges and solutions, Idea Group Publishing, Hershey, PA,
David Walker , Karl Crary , Greg Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.701-771, July 2000
Peter Thiemann, Program specialization for execution monitoring, Journal of Functional Programming, v.13 n.3, p.573-600, May
Robert Grimm , Brian N. Bershad, Separating access control policy, enforcement, and functionality in extensible systems, ACM Transactions on Computer Systems (TOCS), v.19 n.1, p.36-70, Feb. 2001
Yao-Wen Huang , Fang Yu , Christian Hang , Chung-Hung Tsai , Der-Tsai Lee , Sy-Yen Kuo, Securing web application code by static analysis and runtime protection, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA
security automata;security policies;safety properties;proof carrying code;SASI;EM security policies;inlined reference monitors