Dynamic Intransitive Noninterference Revisited
This work addresses security policy enforcement in systems like operating systems, but it is incremental as it builds on existing static models.
The paper tackles the problem of dynamic information flow security policies by developing two semantic interpretations in an automaton-based model, generalizing static intransitive noninterference, and identifies conditions for their equivalence with sound and complete proof techniques.
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.