Noninterference, Transitivity, and Channel-Control Security Policies 1 论文

摘要

We consider noninterference formulations of security policies [7] in which the “interferes ” relation is intransitive. Such policies provide a formal basis for several real security concerns, such as channel control [17, 18], and assured pipelines [4]. We show that the appropriate formulation of noninterference for the intransitive case is that developed by Haigh and Young for “multidomain security ” (MDS) [9, 10]. We construct an “unwinding theorem ” [8] for intransitive polices and show that it differs significantly from that of Haigh and Young. We argue that their theorem is incorrect. A companion report [22] presents a mechanically-checked formal specification and verification of our unwinding theorem. We consider the relationship between transitive and intransitive formulations of security. We show that the standard formulations of noninterference and unwinding [7, 8] correspond exactly to our intransitive formulations, specialized to the transitive case. We show that transitive