SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Noninterference, Transitivity, and Channel-Control Security Policies
 by Dr. John Rushby.

From Technical Report CSL-92-02.
December, 1992.


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.

BibTEX Entry
    AUTHOR = {John Rushby},
    TITLE = {Noninterference, Transitivity, and Channel-Control Security Policies},
    YEAR = {1992},
    MONTH = {dec},
    URL = {},
    BOOKTITLE = {Technical Report {CSL-92-02}}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy