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

*UPDATED* 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