The paper studies dynamic information flow security policies in an automaton-based model. Two semantic interpretations of such policies are developed, both of which generalize the notion of TA-security [van der Meyden ESORICS 2007] for static intransitive noninterference policies. One of the interpretations focuses on information flows permitted by policy edges, the other focuses on prohibitions implied by absence of policy edges. In general, the two interpretations differ, but necessary and sufficient conditions are identified for the two interpretations to be equivalent. Sound and complete proof techniques are developed for both interpretations. Two applications of the theory are presented. The first is a general result showing that access control mechanisms are able to enforce a dynamic information flow policy. The second is a simple capability system motivated by the Flume operating system.
Consider a situation with domains @math . Let @math be the policy @math . Intuitively, @math here is the policy authority, and @math states that all domains are permitted to know the state of the policy. In the initial state of the system, take the policy to be @math . Any actions performed by @math are, intuitively, permitted by this policy to be recorded in the state of @math , but should remain unknown to @math . Suppose that after some actions by @math , the policy agent changes the policy to @math . Now, @math is permitted to communicate with @math . According to our intuitions and formal definitions, @math may now send to @math the information it has about the actions that @math performed before the policy change. Such flows from @math to @math via @math are typical of the flows that intransitive policies are intended to permit @cite_4 .
@cite_4
2048500751
A noninterference formulation of MLS applicable to the Secure Ada® Target (SAT) Abstract Model is developed. An analogous formulation is developed to handle the SAT type enforcement policy. Unwinding theorems are presented for both MLS and Multidomain Security (MDS) and the SAT Abstract Model is shown to satisfy both MLS and MDS. Generalizations and extensions are also considered.