Providing Policy Control Over Object Operations in a Mach Based System
This paper provides an overview of the DTOS prototype and control
mechanisms. It begins by describing the basic elements of the Mach
kernel and the Mach access controls. It then describes the controls
added to the kernel under the DTOS program and interactions with the
security server. It concludes with analysis of some preliminary
performance figures.
Abstract. Full paper
available as a postscript file
(170K), or as a pdf file
(120K).
Developing and Using a Policy Neutral Access Control Policy
This paper describes the DTOS security policy flexibility. It
begins with a discussion of the basic architecture and the control
philosophy for DTOS. It describes the structure of the security
policy document, and discusses the range of policies supportable by
DTOS.
Abstract. Full paper
available as a postscript file
(120K), or as a pdf file (131K).
Defining Noninterference in the Temporal Logic of Actions
This paper is an output of the DTOS Composability Study. It
describes an approach for using Lamport's Temporal Logic of Actions
to specify noninterference properties. In addition to providing a
more intuitive definition of noninterference than previous attempts,
this approach also supports analysis of systems that do contain
covert channels to demonstrate limitations on their exploitations.
In relating the definition of noninterference given here to prior
definitions of noninterference, this paper also discusses ways in
which other definitions of noninterference can be formalized in TLA.
Finally, this paper discusses how prior work on specification
refinement and composition might be applied to the noninterference
problem within the framework provided by TLA.
Abstract. Full paper
available as a postscript file
(110K), or as a pdf file
(125K).
A Framework for Composition
This paper is also an output of the DTOS Composability Study. It
describes an interim version of the composability framework
developed as part of the study. It explains the advantages of the
new framework, and illustrates the use of the framework through a
simple example.
Abstract. Full paper
available as a postscript file
(130K), or as a pdf file
(157K).