Noninterference, Transitivity, and Channel-Control Security Policies
John Rushby
Technical Report CSL-92-02, Computer Science Laboratory, SRI
International; December 1992
Abstract
We consider noninterference formulations of security policies in which
the "interferes" relation is intransitive. Such policies provide a
formal basis for several real security concerns, such as channel
control, and assured pipelines. We show that the appropriate
formulation of noninterference for the intransitive case is that
developed by Haigh and Young for "multidomain security" (MDS). We
construct an "unwinding theorem" for intransitive polices and show
that it differs significantly from that of Haigh and Young. We argue
that their theorem is incorrect. An appendix presents a
mechanically-checked formal specification and verification of our
unwinding theorem.
We also consider the relationship between transitive and intransitive
formulations of security. We show that the standard formulations of
noninterference and unwinding correspond exactly to our intransitive
formulations, specialized to the transitive case. We show that
transitive polices are precisely the "multilevel security" (MLS)
polices, and that any MLS secure system satisfies the conditions of
the unwinding theorem.
In addition, we consider the relationship between noninterference
formulations of security and access control formulations, and we
identify the "reference monitor assumptions" that play a crucial role
in establishing the soundness of access control implementations.
Files
The version that used to be here was incorrectly dated and lacked the
appendices.
longer version with formal appendices
BibTeX Entry
@techreport{Rushby92:intransitive-noninterference,
TITLE = {Noninterference, Transitivity, and Channel-Control Security
Policies},
AUTHOR = {John Rushby},
INSTITUTION = {Computer Science Laboratory, SRI International},
YEAR = 1992,
NUMBER = {SRI-CSL-92-2},
ADDRESS = {Menlo Park, CA},
MONTH = dec
}
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page